- PRIME_FACTORS_EXIST
-
|- ∀n.
0 < n ⇒ ∃b. FINITE_BAG b ∧ (∀m. m ⋲ b ⇒ prime m) ∧ (n = BAG_GEN_PROD b 1)
- UNIQUE_PRIME_FACTORS
-
|- ∀n b1 b2.
(FINITE_BAG b1 ∧ (∀m. m ⋲ b1 ⇒ prime m) ∧ (n = BAG_GEN_PROD b1 1)) ∧
FINITE_BAG b2 ∧ (∀m. m ⋲ b2 ⇒ prime m) ∧ (n = BAG_GEN_PROD b2 1) ⇒
(b1 = b2)
- PRIME_FACTORIZATION
-
|- ∀n.
0 < n ⇒
∀b.
FINITE_BAG b ∧ (∀x. x ⋲ b ⇒ prime x) ∧ (BAG_GEN_PROD b 1 = n) ⇒
(b = PRIME_FACTORS n)
- PRIME_FACTORS_1
-
|- PRIME_FACTORS 1 = {||}
- PRIME_FACTOR_DIVIDES
-
|- ∀x n. 0 < n ∧ x ⋲ PRIME_FACTORS n ⇒ divides x n
- DIVISOR_IN_PRIME_FACTORS
-
|- ∀p n. 0 < n ∧ prime p ∧ divides p n ⇒ p ⋲ PRIME_FACTORS n
- PRIME_FACTORS_MULT
-
|- ∀a b.
0 < a ∧ 0 < b ⇒
(PRIME_FACTORS (a * b) = PRIME_FACTORS a ⊎ PRIME_FACTORS b)
- FACTORS_prime
-
|- ∀p. prime p ⇒ (PRIME_FACTORS p = {|p|})
- PRIME_FACTORS_EXP
-
|- ∀p e. prime p ⇒ (PRIME_FACTORS (p ** e) p = e)