Theory "divides"

Signature

Definitions

divides_def

|- ∀a b. divides a b ⇔ ∃q. b = q * a

prime_def

|- ∀a. prime a ⇔ a ≠ 1 ∧ ∀b. divides b a ⇒ (b = a) ∨ (b = 1)

PRIMES_def

|- (PRIMES 0 = 2) ∧ ∀n. PRIMES (SUC n) = LEAST p. prime p ∧ PRIMES n < p

Theorems

ALL_DIVIDES_0

|- ∀a. divides a 0

ZERO_DIVIDES

|- divides 0 m ⇔ (m = 0)

DIVIDES_REFL

|- ∀a. divides a a

DIVIDES_TRANS

|- ∀a b c. divides a b ∧ divides b c ⇒ divides a c

ONE_DIVIDES_ALL

|- ∀a. divides 1 a

DIVIDES_ONE

|- ∀x. divides x 1 ⇔ (x = 1)

DIVIDES_ADD_1

|- ∀a b c. divides a b ∧ divides a c ⇒ divides a (b + c)

DIVIDES_ADD_2

|- ∀a b c. divides a b ∧ divides a (b + c) ⇒ divides a c

DIVIDES_SUB

|- ∀a b c. divides a b ∧ divides a c ⇒ divides a (b − c)

DIVIDES_LE

|- ∀a b. 0 < b ∧ divides a b ⇒ a ≤ b

DIVIDES_LEQ_OR_ZERO

|- ∀m n. divides m n ⇒ m ≤ n ∨ (n = 0)

NOT_LT_DIVIDES

|- ∀a b. 0 < b ∧ b < a ⇒ ¬divides a b

DIVIDES_ANTISYM

|- ∀a b. divides a b ∧ divides b a ⇒ (a = b)

DIVIDES_MULT

|- ∀a b c. divides a b ⇒ divides a (b * c)

DIVIDES_MULT_LEFT

|- ∀n m. divides (n * m) m ⇔ (m = 0) ∨ (n = 1)

DIVIDES_FACT

|- ∀b. 0 < b ⇒ divides b (FACT b)

LEQ_DIVIDES_FACT

|- ∀m n. 0 < m ∧ m ≤ n ⇒ divides m (FACT n)

NOT_PRIME_0

|- ¬prime 0

NOT_PRIME_1

|- ¬prime 1

PRIME_2

|- prime 2

PRIME_3

|- prime 3

PRIME_POS

|- ∀p. prime p ⇒ 0 < p

ONE_LT_PRIME

|- ∀p. prime p ⇒ 1 < p

prime_divides_only_self

|- ∀m n. prime m ∧ prime n ∧ divides m n ⇒ (m = n)

PRIME_FACTOR

|- ∀n. n ≠ 1 ⇒ ∃p. prime p ∧ divides p n

EUCLID

|- ∀n. ∃p. n < p ∧ prime p

primePRIMES

|- ∀n. prime (PRIMES n)

INFINITE_PRIMES

|- ∀n. PRIMES n < PRIMES (SUC n)

LT_PRIMES

|- ∀m n. m < n ⇒ PRIMES m < PRIMES n

PRIMES_11

|- ∀m n. (PRIMES m = PRIMES n) ⇒ (m = n)

INDEX_LESS_PRIMES

|- ∀n. n < PRIMES n

EUCLID_PRIMES

|- ∀n. ∃i. n < PRIMES i

NEXT_LARGER_PRIME

|- ∀n. ∃i. n < PRIMES i ∧ ∀j. j < i ⇒ PRIMES j ≤ n

PRIMES_NO_GAP

|- ∀n p. PRIMES n < p ∧ p < PRIMES (SUC n) ∧ prime p ⇒ F

PRIMES_ONTO

|- ∀p. prime p ⇒ ∃i. PRIMES i = p

PRIME_INDEX

|- ∀p. prime p ⇔ ∃i. p = PRIMES i

ONE_LT_PRIMES

|- ∀n. 1 < PRIMES n

ZERO_LT_PRIMES

|- ∀n. 0 < PRIMES n

compute_divides

|- ∀a b.
     divides a b ⇔
     if a = 0 then b = 0
     else if a = 1 then T
     else if b = 0 then T
     else b MOD a = 0