Package natural-divides-gcd-thm: Properties of natural number greatest common divisor

Information

namenatural-divides-gcd-thm
version1.0
descriptionProperties of natural number greatest common divisor
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2014-11-17
checksum101c8bc67156b3739811f4df283dfb46b0363064
requiresbase
natural-divides-def
natural-divides-gcd-def
natural-divides-thm
showData.Bool
Number.Natural

Files

Theorems

a. gcd 0 a = a

a. gcd a 0 = a

a. gcd a a = a

a. gcd a 1 = 1

a. gcd 1 a = 1

a b. gcd a b = gcd b a

a b. gcd a b = a divides a b

a b. gcd b a = a divides a b

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

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

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

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

a b c. divides b a divides (gcd b c) a

a b c. divides b a divides (gcd c b) a

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

a b. a b gcd a (b - a) = gcd a b

a b. b a gcd (a - b) b = gcd a b

a b. gcd a b = 0 a = 0 b = 0

a b s t. divides (gcd a b) (distance (s * a) (t * b))

a b. s t. distance (s * a) (t * b) = gcd a b

a b c. divides c (gcd a b) divides c a divides c b

a b c. divides (gcd a (b * c)) (gcd a b * gcd a c)

a b c. gcd (a * b) (a * c) = a * gcd b c

a b c. gcd (b * a) (c * a) = gcd b c * a

a b. gcd a b = 1 gcd (a * a) b = 1

a b. gcd b a = 1 gcd b (a * a) = 1

a b. gcd b (a * a) = 1 gcd b a = 1

a b. gcd (a * a) b = 1 gcd a b = 1

a b c. gcd b (a * c) = 1 gcd b c = 1

a b c. gcd b (c * a) = 1 gcd b c = 1

a b c. gcd (a * b) c = 1 gcd b c = 1

a b c. gcd (b * a) c = 1 gcd b c = 1

a b c. gcd a b = 1 gcd a (b * c) = gcd a c

a b c. gcd a b = 1 gcd a (c * b) = gcd a c

a b c. gcd b a = 1 gcd (b * c) a = gcd c a

a b c. gcd b a = 1 gcd (c * b) a = gcd c a

a b. ¬(a = 0) s t. t * b + gcd a b = s * a

a b. ¬(a = 0) s t. t * b + gcd b a = s * a

a b s t. distance (s * a) (t * b) = 1 gcd a b = 1

a b. (c. divides c a divides c b c = 1) gcd a b = 1

a b.
    gcd a b = if a = 0 then b else if a b then gcd a (b - a) else gcd b a

a b c. gcd b c = 1 divides b a divides c a divides (b * c) a

a b c. gcd a (b * c) = 1 gcd a b = 1 gcd a c = 1

a b c. gcd (b * c) a = 1 gcd b a = 1 gcd c a = 1

a b c. gcd a b = 1 gcd a c = 1 gcd a (b * c) = 1

a b c. gcd b a = 1 gcd c a = 1 gcd (b * c) a = 1

a b g.
    divides g a divides g b
    (c. divides c a divides c b divides c g) gcd a b = g

p.
    p 0 0 (a b. gcd a b = 1 p a b)
    (c a b. ¬(c = 0) p a b p (c * a) (c * b)) a b. p a b

External Type Operators

External Constants

Assumptions

¬

t. t t

a. divides a 0

a. divides a a

p. p

t. t ¬t

a. divides 1 a

(¬) = λp. p

t. (x. t) t

() = λp. p = λx.

t. t

t. t t

t. t t

t. t t t

t. t

t. t t

t. t

t. t t

t. t

t. t t t

n. 0 * n = 0

m. m * 0 = 0

n. distance 0 n = n

n. distance n n = 0

t. (t ) ¬t

m. m * 1 = m

m. 1 * m = m

m n. m m + n

a b. divides (gcd a b) a

a b. divides (gcd a b) b

() = λp q. p q p

a. divides 0 a a = 0

x y. x = y y = x

a b. (a b) a b

m n. m * n = n * m

m n. m + n = n + m

m n. distance m n = distance n m

a b. a = b divides a b

m n. m + n - m = n

a. divides a 1 a = 1

m. m = 0 n. m = suc n

() = λp q. (λf. f p q) = λf. f

() = λp. q. (x. p x q) q

t1 t2. ¬t1 ¬t2 t2 t1

m n. suc m * n = m * n + n

a b c. divides a c divides a (b * c)

a b. divides a b c. c * a = b

() = λp q. r. (p r) (q r) r

m n. n m m - n + n = m

a b. divides a b divides b a a = b

p. (x y. p x y) y x. p x y

x y z. x = y y = z x = z

m n p. m * (n * p) = m * n * p

m n p. m + (n + p) = m + n + p

p m n. m + p = n + p m = n

p m n. distance (m + p) (n + p) = distance m n

a b c. divides a b divides b c divides a c

m n. m * n = 0 m = 0 n = 0

m n. distance (distance m n) (distance m (n + 1)) = 1

m n p. m * (n + p) = m * n + m * p

m n p. m * distance n p = distance (m * n) (m * p)

m n p. (m + n) * p = m * p + n * p

p m n. distance m n * p = distance (m * p) (n * p)

a b c. divides a b divides a c divides a (b + c)

a b c. divides c a divides c b divides c (gcd a b)

a b c. divides (a * b) (a * c) a = 0 divides b c

a b c. divides (b * a) (c * a) a = 0 divides b c

m n p. distance m n = p m + p = n n + p = m

a b c. c b divides a b divides a c divides a (b - c)

p c x y. p (if c then x else y) (c p x) (¬c p y)

p.
    (n. p 0 n) (m n. n < m p n m p m n)
    (m n. p m n p m (n + m)) m n. p m n