Theory primeFactor

⊢ ∀n. 0 < n ⇒
      FINITE_BAG (PRIME_FACTORS n) ∧ (∀m. m ⋲ PRIME_FACTORS n ⇒ prime m) ∧
      n = BAG_GEN_PROD (PRIME_FACTORS n) 1

⊢ ∀p n. 0 < n ∧ prime p ∧ divides p n ⇒ p ⋲ PRIME_FACTORS n

⊢ ∀p. prime p ⇒ PRIME_FACTORS p = {|p|}

⊢ ∀b n.
    FINITE_BAG b ∧ BAG_GEN_PROD b 1 = n ∧ (∀x. x ⋲ b ⇒ 2 ≤ x) ⇒
    BAG_CARD b ≤ BAG_CARD (PRIME_FACTORS n)

⊢ ∀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 = {||}

⊢ ∀n. 0 < n ⇒
      ∃b. FINITE_BAG b ∧ (∀m. m ⋲ b ⇒ prime m) ∧ n = BAG_GEN_PROD b 1

⊢ ∀p e. prime p ⇒ PRIME_FACTORS (p ** e) p = e

⊢ ∀a b.
    0 < a ∧ 0 < b ⇒
    PRIME_FACTORS (a * b) = PRIME_FACTORS a ⊎ PRIME_FACTORS b

⊢ ∀x n. 0 < n ∧ x ⋲ PRIME_FACTORS n ⇒ divides x n

⊢ ∀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