Theory gcd

⊢ ∀a b c.
    is_gcd a b c ⇔
    c divides a ∧ c divides b ∧ ∀d. d divides a ∧ d divides b ⇒ d divides c

⊢ ∀m n. lcm m n = if m = 0 ∨ n = 0 then 0 else m * n DIV gcd m n

⊢ ∀m n.
    (EVEN m ∧ EVEN n ⇒ gcd m n = 2 * gcd (m DIV 2) (n DIV 2)) ∧
    (EVEN m ∧ ODD n ⇒ gcd m n = gcd (m DIV 2) n)

⊢ ∀a b n. prime a ∧ 0 < n ⇒ (a divides b ⇔ a divides b ** n)

⊢ ∀p x y. prime p ⇒ (x * y MOD p = 0 ⇔ x MOD p = 0 ∨ y MOD p = 0)

⊢ ∀n m.
    n ≠ 0 ∧ m ≠ 0 ⇒ ∃p q. n = p * gcd n m ∧ m = q * gcd n m ∧ coprime p q

⊢ ∀p n. prime p ∧ n < p ⇒ FACT n MOD p ≠ 0

⊢ ∀x. gcd 0 x = x ∧ gcd x 0 = x

⊢ ∀a. gcd 0 a = a

⊢ ∀a. gcd a 0 = a

⊢ coprime 1 x ∧ coprime x 1

⊢ ∀a b. gcd (a + b) a = gcd a b

⊢ (∀a b. gcd (a + b) a = gcd a b) ∧ ∀a b. gcd (b + a) a = gcd a b

⊢ ∀a b. gcd a (a + b) = gcd a b

⊢ (∀a b. gcd a (a + b) = gcd a b) ∧ ∀a b. gcd a (b + a) = gcd a b

⊢ ∀a b c. gcd a (gcd b c) = gcd (gcd a b) c

⊢ ∀a b c. gcd a (gcd b c) = gcd b (gcd a c)

⊢ ∀m n k. coprime m k ⇒ gcd m (k * n) = gcd m n

⊢ gcd a b = gcd b a

⊢ ∀m n k. gcd (k * m) (k * n) = k * gcd m n

⊢ ∀m n. 0 < n ∧ 0 < m ⇒ 0 < gcd n m ∧ n MOD gcd n m = 0 ∧ m MOD gcd n m = 0

⊢ ∀a b. gcd a b = if a = 0 then b else gcd (b MOD a) a

⊢ ∀n m. gcd n m = 0 ⇔ n = 0 ∧ m = 0

⊢ ∀a b c. gcd a (b * a + c) = gcd a c

⊢ ∀m n. gcd n (gcd n m) = gcd n m

⊢ ∀a b. is_gcd a b (gcd a b)

⊢ ∀a b.
    gcd a b divides a ∧ gcd a b divides b ∧
    ∀d. d divides a ∧ d divides b ⇒ d divides gcd a b

⊢ ∀m n. gcd m n * lcm m n = m * n

⊢ ∀j k. 0 < j ⇒ ∃p q. p * j = q * k + gcd j k

⊢ ∀m n. 0 < m ⇒ gcd m n = gcd m (n MOD m)

⊢ ∀m n. 0 < m ⇒ gcd n m = gcd (n MOD m) m

⊢ ∀m n. 0 < n ∧ m MOD n = 0 ⇒ gcd m n = n

⊢ ∀m n. gcd (m * n) n = n

⊢ ∀n x. 1 < n ∧ coprime n x ⇒ ∃k. k * x MOD n = 1 ∧ coprime n k

⊢ ∀m n. 0 < m ∨ 0 < n ⇒ 0 < gcd m n

⊢ ∀a b c.
    c = gcd a b ⇔
    c divides a ∧ c divides b ∧ ∀x. x divides a ∧ x divides b ⇒ x divides c

⊢ ∀a b c. gcd (b * a + c) a = gcd a c

⊢ ∀m n k. coprime m k ⇒ gcd m (k * n) = gcd m n

⊢ ∀a. gcd a a = a

⊢ ∀a b. b ≤ a ⇒ gcd (a − b) b = gcd a b

⊢ ∀a b. a ≤ b ⇒ gcd a (b − a) = gcd a b

⊢ ∀P. (∀y. P 0 y) ∧ (∀x y. P x y ⇒ P y x) ∧ (∀x. P x x) ∧
      (∀x y. 0 < x ∧ 0 < y ∧ P x y ⇒ P x (x + y)) ⇒
      ∀m n. P m n

⊢ ∀a b. gcd a b = gcd b a

⊢ ∀a. is_gcd 0 a a

⊢ ∀a. is_gcd a 0 a

⊢ ∀a b c. b ≤ a ∧ is_gcd (a − b) b c ⇒ is_gcd a b c

⊢ ∀a b c. a ≤ b ∧ is_gcd a (b − a) c ⇒ is_gcd a b c

⊢ ∀a. is_gcd a a a

⊢ ∀a b c. is_gcd a b c ⇔ is_gcd b a c

⊢ ∀a b c d. is_gcd a b c ∧ is_gcd a b d ⇒ c = d

⊢ lcm 0 x = 0 ∧ lcm x 0 = 0

⊢ lcm 1 x = x ∧ lcm x 1 = x

⊢ ∀a b c. lcm a (lcm b c) = lcm (lcm a b) c

⊢ ∀a b c. lcm a (lcm b c) = lcm b (lcm a c)

⊢ lcm a b = lcm b a

⊢ ∀a b. coprime a b ⇒ ∀c. lcm (a * c) (b * c) = a * b * c

⊢ ∀m n k. lcm (k * m) (k * n) = k * lcm m n

⊢ ∀m n. coprime m n ⇒ lcm m n = m * n

⊢ ∀n a b. a divides n ∧ b divides n ⇒ lcm a b divides n

⊢ ∀m n. m divides lcm m n ∧ n divides lcm m n

⊢ ∀m n. lcm m n = 0 ⇔ m = 0 ∨ n = 0

⊢ ∀m n p. m divides p ∧ n divides p ⇒ lcm m n divides p

⊢ m divides lcm m n ∧ n divides lcm m n ∧
  ∀p. m divides p ∧ n divides p ⇒ lcm m n divides p

⊢ 0 < m ∧ 0 < n ⇒ m ≤ lcm m n ∧ m ≤ lcm n m

⊢ 0 < m ∧ 0 < n ⇒ ∀p. 0 < p ∧ p < lcm m n ⇒ ¬(m divides p) ∨ ¬(n divides p)

⊢ ∀m n. 0 < m ∧ 0 < n ⇒ 0 < lcm m n

⊢ ∀a b c.
    c = lcm a b ⇔
    a divides c ∧ b divides c ∧ ∀x. a divides x ∧ b divides x ⇒ c divides x

⊢ ∀a. lcm a a = a

⊢ ∀a b. lcm a b = lcm b a

⊢ ∀n m. n ≠ 0 ⇒ ∃p q. p * n = q * m + gcd m n

⊢ ∀a b c. coprime a b ∧ b divides a * c ⇒ b divides c

⊢ ∀n a b. 0 < n ∧ b ≤ a ⇒ ((a − b) MOD n = 0 ⇔ a MOD n = b MOD n)

⊢ ∀n a b. 0 < n ∧ a MOD n = b MOD n ⇒ (a − b) MOD n = 0

⊢ ∀n a b. 0 < n ∧ b ≤ a ⇒ (a MOD n = b MOD n ⇔ ∃c. a = b + c * n)

⊢ ∀n. 1 < n ⇒ ∀x. coprime n x ⇒ 0 < x ∧ 0 < x MOD n

⊢ ∀n x y. 0 < n ⇒ (x + y) MOD n = (x + y MOD n) MOD n

⊢ ∀n x. 0 < n ∧ coprime n x ⇒ coprime n (x MOD n)

⊢ ∀p k. prime p ∧ k < p ⇒ ¬(p divides FACT k)

⊢ ∀p b. prime p ⇒ p divides b ∨ coprime p b

⊢ ∀p b. prime p ⇒ p divides b ∨ is_gcd p b 1

⊢ ∀n x y. coprime n x ∧ coprime n y ⇒ coprime n (x * y)

⊢ ∀p a b. prime p ∧ p divides a * b ⇒ p divides a ∨ p divides b

⊢ ∀n. (coprime 0 n ⇔ n = 1) ∧ (coprime n 0 ⇔ n = 1)

⊢ ∀n. coprime 0 n ⇔ n = 1

⊢ ∀n. coprime n 0 ⇔ n = 1

⊢ ∀n. 0 < n ⇒ coprime n (n − 1)

⊢ ∀n. coprime n (n + 1)

⊢ ∀m n. coprime m n ⇔ ∀p. prime p ⇒ ¬(p divides m ∧ p divides n)

⊢ ∀m n.
    0 < m ∧ 0 < n ⇒
    (coprime m n ⇔
     ∀p. prime p ∧ p ≤ m ∧ p ≤ n ⇒ ¬(p divides m ∧ p divides n))

⊢ ∀a b c. coprime a b ∧ c divides a ∧ c divides b ⇒ c = 1

⊢ ∀c m. coprime c m ⇒ ∀n. coprime (c ** n) m

⊢ ∀a b. coprime a b ⇒ ∀n. coprime a (b ** n)

⊢ ∀m n. m divides n ⇒ ∀k. coprime n k ⇒ coprime m k

⊢ ∀n k. 1 < n ∧ coprime n k ⇒ ∀p. 1 < p ∧ p divides n ⇒ ¬(p divides k)

⊢ ∀n k. coprime k n ∧ 1 < n ⇒ 0 < k

⊢ ∀m n. 0 < m ∧ coprime m n ⇒ coprime m (n MOD m)

⊢ ∀m n. 0 < m ⇒ (coprime m n ⇔ coprime m (n MOD m))

⊢ ∀n k. coprime k n ∧ n ≠ 1 ⇒ k ≠ 0

⊢ ∀n p. 1 < n ∧ prime p ∧ p divides n ⇒ ∀k. coprime n k ⇒ coprime p k

⊢ ∀x y z. coprime x z ∧ coprime y z ⇒ coprime (x * y) z

⊢ ∀x y z. coprime x z ⇒ (coprime y z ⇔ coprime (x * y) z)

⊢ ∀x y z. coprime z x ∧ coprime z y ⇒ coprime z (x * y)

⊢ ∀n a b. a divides n ∧ b divides n ∧ coprime a b ⇒ a * b divides n

⊢ ∀x y. coprime x y ⇔ coprime y x

⊢ ∀n m k. coprime n m ⇒ (n divides m * k ⇔ n divides k)

⊢ ∀m n. n divides m ⇔ gcd n m = n

⊢ ∀m n. n divides m ⇔ lcm n m = m

⊢ ∀m n. 0 < m ∧ n divides m ⇒ coprime n (PRE m)

⊢ ∀m n. n divides m ⇒ coprime n (SUC m)

⊢ ∀m n. n ≠ 0 ⇒ gcd m n ≤ n

⊢ (∀y. gcd 0 y = y) ∧ (∀x. gcd <..num comp'n..> 0 = <..num comp'n..> ) ∧
  (∀x. gcd <..num comp'n..> 0 = <..num comp'n..> ) ∧
  (∀y x.
     gcd <..num comp'n..> <..num comp'n..> =
     if <..num comp'n..> − 1 ≤ <..num comp'n..> − 1 then
       gcd (<..num comp'n..> − 1 − (<..num comp'n..> − 1)) <..num comp'n..>
     else
       gcd <..num comp'n..> (<..num comp'n..> − 1 − (<..num comp'n..> − 1))) ∧
  (∀y x.
     gcd <..num comp'n..> <..num comp'n..> =
     if <..num comp'n..> − 1 ≤ <..num comp'n..> then
       gcd (<..num comp'n..> − (<..num comp'n..> − 1)) <..num comp'n..>
     else gcd <..num comp'n..> (<..num comp'n..> − 1 − <..num comp'n..> )) ∧
  (∀y x.
     gcd <..num comp'n..> <..num comp'n..> =
     if <..num comp'n..> ≤ <..num comp'n..> − 1 then
       gcd (<..num comp'n..> − 1 − <..num comp'n..> ) <..num comp'n..>
     else gcd <..num comp'n..> (<..num comp'n..> − (<..num comp'n..> − 1))) ∧
  ∀y x.
    gcd <..num comp'n..> <..num comp'n..> =
    if <..num comp'n..> ≤ <..num comp'n..> then
      gcd (<..num comp'n..> − <..num comp'n..> ) <..num comp'n..>
    else gcd <..num comp'n..> (<..num comp'n..> − <..num comp'n..> )

⊢ ∀m n p. coprime p n ⇒ gcd (p * m) n = gcd m n

⊢ (∀y. gcd 0 y = y) ∧ (∀x. gcd (SUC x) 0 = SUC x) ∧
  ∀y x.
    gcd (SUC x) (SUC y) =
    if y ≤ x then gcd (x − y) (SUC y) else gcd (SUC x) (y − x)

⊢ ∀P. (∀y. P 0 y) ∧ (∀x. P (SUC x) 0) ∧
      (∀x y.
         (¬(y ≤ x) ⇒ P (SUC x) (y − x)) ∧ (y ≤ x ⇒ P (x − y) (SUC y)) ⇒
         P (SUC x) (SUC y)) ⇒
      ∀v v1. P v v1

⊢ ∀n p. prime p ∧ gcd p n ≠ 1 ⇒ p divides n

⊢ ∀n p. prime p ∧ ¬(p divides n) ⇒ coprime p n

⊢ ∀p q. prime p ∧ prime q ∧ p ≠ q ⇒ coprime p q