Theory gcdset

⊢ ∀s. big_gcd s = ITSET gcd s 0

⊢ ∀s. big_lcm s = ITSET lcm s 1

⊢ ∀n. coprimes n = {j | j ∈ natural n ∧ coprime j n}

⊢ ∀s. gcdset s =
      if s = ∅ ∨ s = {0} then 0
      else
        MAX_SET
          ({n | n ≤ MIN_SET (s DELETE 0)} ∩ {d | ∀e. e ∈ s ⇒ d divides e})

⊢ big_gcd ∅ = 0

⊢ ∀s. FINITE s ⇒ ∀x. big_gcd (x INSERT s) = gcd x (big_gcd s)

⊢ ∀s. FINITE s ⇒ ∀x. x ∈ s ⇒ big_gcd s divides x

⊢ ∀s. FINITE s ⇒ ∀m. (∀x. x ∈ s ⇒ m divides x) ⇒ m divides big_gcd s

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∀k. big_gcd (IMAGE ($* k) s) = k * big_gcd s

⊢ ∀s. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ 0 < x) ⇒ 0 < big_gcd s

⊢ ∀s x. FINITE s ∧ x ∉ s ⇒ big_gcd (x INSERT s) = gcd x (big_gcd s)

⊢ ∀x. big_gcd {x} = x

⊢ ∀x y. big_gcd {x; y} = gcd x y

⊢ big_lcm ∅ = 1

⊢ ∀s. FINITE s ⇒ ∀x. big_lcm (x INSERT s) = lcm x (big_lcm s)

⊢ ∀s. FINITE s ⇒ ∀x. x ∈ s ⇒ x divides big_lcm s

⊢ ∀s. FINITE s ⇒ ∀m. (∀x. x ∈ s ⇒ x divides m) ⇒ big_lcm s divides m

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∀k. big_lcm (IMAGE ($* k) s) = k * big_lcm s

⊢ ∀s. FINITE s ⇒ (∀x. x ∈ s ⇒ 0 < x) ⇒ 0 < big_lcm s

⊢ ∀s x. FINITE s ∧ x ∉ s ⇒ big_lcm (x INSERT s) = lcm x (big_lcm s)

⊢ ∀x. big_lcm {x} = x

⊢ ∀x y. big_lcm {x; y} = lcm x y

⊢ coprimes 0 = ∅

⊢ coprimes 1 = {1}

⊢ ∀n. coprimes n = natural n ∩ {j | coprime j n}

⊢ ∀n j. j ∈ coprimes n ⇔ 0 < j ∧ j ≤ n ∧ coprime j n

⊢ ∀n. 1 < n ⇒ ∀j. j ∈ coprimes n ⇔ j < n ∧ coprime j n

⊢ ∀n. 1 < n ⇒ ∀j. j ∈ coprimes n ⇒ j < n

⊢ ∀n. coprimes n = ∅ ⇔ n = 0

⊢ ∀n. FINITE (coprimes n)

⊢ ∀n. 0 < n ⇒ 1 ∈ coprimes n

⊢ ∀n. 1 < n ⇒ n − 1 ∈ coprimes n

⊢ ∀n. 1 < n ⇒ MAX_SET (coprimes n) = n − 1

⊢ ∀n. 0 ∉ coprimes n

⊢ ∀n. coprimes n ⊆ natural n

⊢ ∀n. n ∈ coprimes n ⇔ n = 1

⊢ ∀n. 1 < n ⇒ n ∉ coprimes n

⊢ gcdset ∅ = 0

⊢ gcdset (x INSERT s) = gcd x (gcdset s)

⊢ ∀e. e ∈ s ⇒ gcdset s divides e

⊢ (∀e. e ∈ s ⇒ g divides e) ⇒ g divides gcdset s

⊢ natural 0 = ∅

⊢ natural 1 = {1}

⊢ ∀n. CARD (natural n) = n

⊢ ∀n a b. 0 < n ∧ 0 < a ∧ b ∈ natural n ∧ a divides b ⇒ b DIV a ∈ natural n

⊢ ∀n a b.
    0 < n ∧ a divides n ∧ b ∈ natural n ∧ a divides b ⇒
    b DIV a ∈ natural (n DIV a)

⊢ ∀n a b. 0 < n ∧ a ∈ natural n ∧ b divides a ⇒ b ∈ natural n

⊢ ∀n j. j ∈ natural n ⇔ 0 < j ∧ j ≤ n

⊢ ∀n. FINITE (natural n)

⊢ ∀n. 0 < n ⇒ 1 ∈ natural n

⊢ ∀n. 0 < n ⇒ n ∈ natural n

⊢ ∀n. 0 ∉ natural n

⊢ ∀n. natural n = {j | 0 < j ∧ j ≤ n}

⊢ ∀n. natural (SUC n) = SUC n INSERT natural n