Theory "primeFactor"

Signature

Definitions

PRIME_FACTORS_def

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

Theorems

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_FACTORS_MULT

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

PRIME_FACTORS_EXP

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

PRIME_FACTORS_EXIST

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

PRIME_FACTORS_1

⊢ PRIME_FACTORS 1 = {||}

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_FACTOR_DIVIDES

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

FACTORS_prime

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

DIVISOR_IN_PRIME_FACTORS

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