- IS_GCD_UNIQUE
-
|- ∀a b c d. is_gcd a b c ∧ is_gcd a b d ⇒ (c = d)
- IS_GCD_REF
-
|- ∀a. is_gcd a a a
- IS_GCD_SYM
-
|- ∀a b c. is_gcd a b c ⇔ is_gcd b a c
- IS_GCD_0R
-
|- ∀a. is_gcd a 0 a
- IS_GCD_0L
-
|- ∀a. is_gcd 0 a a
- PRIME_IS_GCD
-
|- ∀p b. prime p ⇒ divides p b ∨ is_gcd p b 1
- IS_GCD_MINUS_L
-
|- ∀a b c. b ≤ a ∧ is_gcd (a − b) b c ⇒ is_gcd a b c
- IS_GCD_MINUS_R
-
|- ∀a b c. a ≤ b ∧ is_gcd a (b − a) c ⇒ is_gcd a b c
- gcd_ind
-
|- ∀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
- gcd_def
-
|- (∀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)
- gcd_def_compute
-
|- (∀y. gcd 0 y = y) ∧ (∀x. gcd (NUMERAL (BIT1 x)) 0 = NUMERAL (BIT1 x)) ∧
(∀x. gcd (NUMERAL (BIT2 x)) 0 = NUMERAL (BIT2 x)) ∧
(∀y x.
gcd (NUMERAL (BIT1 x)) (NUMERAL (BIT1 y)) =
if NUMERAL (BIT1 y) − 1 ≤ NUMERAL (BIT1 x) − 1 then
gcd (NUMERAL (BIT1 x) − 1 − (NUMERAL (BIT1 y) − 1)) (NUMERAL (BIT1 y))
else
gcd (NUMERAL (BIT1 x))
(NUMERAL (BIT1 y) − 1 − (NUMERAL (BIT1 x) − 1))) ∧
(∀y x.
gcd (NUMERAL (BIT2 x)) (NUMERAL (BIT1 y)) =
if NUMERAL (BIT1 y) − 1 ≤ NUMERAL (BIT1 x) then
gcd (NUMERAL (BIT1 x) − (NUMERAL (BIT1 y) − 1)) (NUMERAL (BIT1 y))
else gcd (NUMERAL (BIT2 x)) (NUMERAL (BIT1 y) − 1 − NUMERAL (BIT1 x))) ∧
(∀y x.
gcd (NUMERAL (BIT1 x)) (NUMERAL (BIT2 y)) =
if NUMERAL (BIT1 y) ≤ NUMERAL (BIT1 x) − 1 then
gcd (NUMERAL (BIT1 x) − 1 − NUMERAL (BIT1 y)) (NUMERAL (BIT2 y))
else
gcd (NUMERAL (BIT1 x)) (NUMERAL (BIT1 y) − (NUMERAL (BIT1 x) − 1))) ∧
∀y x.
gcd (NUMERAL (BIT2 x)) (NUMERAL (BIT2 y)) =
if NUMERAL (BIT1 y) ≤ NUMERAL (BIT1 x) then
gcd (NUMERAL (BIT1 x) − NUMERAL (BIT1 y)) (NUMERAL (BIT2 y))
else gcd (NUMERAL (BIT2 x)) (NUMERAL (BIT1 y) − NUMERAL (BIT1 x))
- GCD_IS_GCD
-
|- ∀a b. is_gcd a b (gcd a b)
- GCD_REF
-
|- ∀a. gcd a a = a
- GCD_SYM
-
|- ∀a b. gcd a b = gcd b a
- GCD_0R
-
|- ∀a. gcd a 0 = a
- GCD_0L
-
|- ∀a. gcd 0 a = a
- GCD_ADD_R
-
|- ∀a b. gcd a (a + b) = gcd a b
- GCD_ADD_R_THM
-
|- (∀a b. gcd a (a + b) = gcd a b) ∧ ∀a b. gcd a (b + a) = gcd a b
- GCD_ADD_L
-
|- ∀a b. gcd (a + b) a = gcd a b
- GCD_ADD_L_THM
-
|- (∀a b. gcd (a + b) a = gcd a b) ∧ ∀a b. gcd (b + a) a = gcd a b
- GCD_EQ_0
-
|- ∀n m. (gcd n m = 0) ⇔ (n = 0) ∧ (m = 0)
- GCD_1
-
|- (gcd 1 x = 1) ∧ (gcd x 1 = 1)
- PRIME_GCD
-
|- ∀p b. prime p ⇒ divides p b ∨ (gcd p b = 1)
- L_EUCLIDES
-
|- ∀a b c. (gcd a b = 1) ∧ divides b (a * c) ⇒ divides b c
- P_EUCLIDES
-
|- ∀p a b. prime p ∧ divides p (a * b) ⇒ divides p a ∨ divides p b
- FACTOR_OUT_GCD
-
|- ∀n m.
n ≠ 0 ∧ m ≠ 0 ⇒
∃p q. (n = p * gcd n m) ∧ (m = q * gcd n m) ∧ (gcd p q = 1)
- GCD_SUCfree_ind
-
|- ∀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
- LINEAR_GCD
-
|- ∀n m. n ≠ 0 ⇒ ∃p q. p * n = q * m + gcd m n
- GCD_EFFICIENTLY
-
|- ∀a b. gcd a b = if a = 0 then b else gcd (b MOD a) a
- LCM_IS_LEAST_COMMON_MULTIPLE
-
|- divides m (lcm m n) ∧ divides n (lcm m n) ∧
∀p. divides m p ∧ divides n p ⇒ divides (lcm m n) p
- LCM_0
-
|- (lcm 0 x = 0) ∧ (lcm x 0 = 0)
- LCM_1
-
|- (lcm 1 x = x) ∧ (lcm x 1 = x)
- LCM_COMM
-
|- lcm a b = lcm b a
- LCM_LE
-
|- 0 < m ∧ 0 < n ⇒ m ≤ lcm m n ∧ m ≤ lcm n m
- LCM_LEAST
-
|- 0 < m ∧ 0 < n ⇒ ∀p. 0 < p ∧ p < lcm m n ⇒ ¬divides m p ∨ ¬divides n p
- GCD_COMMON_FACTOR
-
|- ∀m n k. gcd (k * m) (k * n) = k * gcd m n
- GCD_CANCEL_MULT
-
|- ∀m n k. (gcd m k = 1) ⇒ (gcd m (k * n) = gcd m n)
- BINARY_GCD
-
|- ∀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))