Theory "divides"

Parents     while   numeral

Signature

Constant Type
PRIMES :num -> num
divides :num -> num -> bool
prime :num -> bool

Definitions

PRIMES_def
⊢ (PRIMES 0 = 2) ∧ ∀n. PRIMES (SUC n) = LEAST p. prime p ∧ PRIMES n < p
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)


Theorems

ALL_DIVIDES_0
⊢ ∀a. divides a 0
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_ANTISYM
⊢ ∀a b. divides a b ∧ divides b a ⇒ (a = b)
DIVIDES_FACT
⊢ ∀b. 0 < b ⇒ divides b (FACT b)
DIVIDES_LE
⊢ ∀a b. 0 < b ∧ divides a b ⇒ a ≤ b
DIVIDES_LEQ_OR_ZERO
⊢ ∀m n. divides m n ⇒ m ≤ n ∨ (n = 0)
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_ONE
⊢ ∀x. divides x 1 ⇔ (x = 1)
DIVIDES_REFL
⊢ ∀a. divides a a
DIVIDES_SUB
⊢ ∀a b c. divides a b ∧ divides a c ⇒ divides a (b − c)
DIVIDES_TRANS
⊢ ∀a b c. divides a b ∧ divides b c ⇒ divides a c
EUCLID
⊢ ∀n. ∃p. n < p ∧ prime p
EUCLID_PRIMES
⊢ ∀n. ∃i. n < PRIMES i
INDEX_LESS_PRIMES
⊢ ∀n. n < PRIMES n
INFINITE_PRIMES
⊢ ∀n. PRIMES n < PRIMES (SUC n)
LEQ_DIVIDES_FACT
⊢ ∀m n. 0 < m ∧ m ≤ n ⇒ divides m (FACT n)
LT_PRIMES
⊢ ∀m n. m < n ⇒ PRIMES m < PRIMES n
NEXT_LARGER_PRIME
⊢ ∀n. ∃i. n < PRIMES i ∧ ∀j. j < i ⇒ PRIMES j ≤ n
NOT_LT_DIVIDES
⊢ ∀a b. 0 < b ∧ b < a ⇒ ¬divides a b
NOT_PRIME_0
⊢ ¬prime 0
NOT_PRIME_1
⊢ ¬prime 1
ONE_DIVIDES_ALL
⊢ ∀a. divides 1 a
ONE_LT_PRIME
⊢ ∀p. prime p ⇒ 1 < p
ONE_LT_PRIMES
⊢ ∀n. 1 < PRIMES n
PRIMES_11
⊢ ∀m n. (PRIMES m = PRIMES n) ⇒ (m = 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_2
⊢ prime 2
PRIME_3
⊢ prime 3
PRIME_FACTOR
⊢ ∀n. n ≠ 1 ⇒ ∃p. prime p ∧ divides p n
PRIME_INDEX
⊢ ∀p. prime p ⇔ ∃i. p = PRIMES i
PRIME_POS
⊢ ∀p. prime p ⇒ 0 < p
ZERO_DIVIDES
⊢ divides 0 m ⇔ (m = 0)
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
primePRIMES
⊢ ∀n. prime (PRIMES n)
prime_divides_only_self
⊢ ∀m n. prime m ∧ prime n ∧ divides m n ⇒ (m = n)