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