Theory divides

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

⊢ ∀a b. a divides b ⇔ ∃q. b = q * a

⊢ ∀a. prime a ⇔ a ≠ 1 ∧ ∀b. b divides a ⇒ b = a ∨ b = 1

⊢ ∀n a b. a MOD n + b < n ⇒ (a + b) DIV n = a DIV n

⊢ ∀a. a divides 0

⊢ ∀a b c. a divides b ∧ a divides c ⇒ a divides b + c

⊢ ∀a b c. a divides b ∧ a divides b + c ⇒ a divides c

⊢ ∀a b. a divides b ∧ b divides a ⇒ a = b

⊢ ∀a b c. a divides b ⇒ c * a divides c * b

⊢ ∀p n. 0 < p ∧ p divides n ⇒ p * (n DIV p) = n

⊢ ∀n. 0 < n ⇒ ∀m. n divides m ⇔ m = m DIV n * n

⊢ ∀n. 0 < n ⇒ ∀m. n divides m ⇔ m = n * (m DIV n)

⊢ ∀m. EVEN m ⇒ ∀n. m divides n ⇒ EVEN n

⊢ ∀b. 0 < b ⇒ b divides FACT b

⊢ ∀a b. 0 < b ∧ a divides b ⇒ a ≤ b

⊢ ∀m n. m divides n ⇒ m ≤ n ∨ n = 0

⊢ ∀p n. 0 < p ⇒ (p divides n ⇔ n MOD p = 0)

⊢ ∀a b c. a divides b ⇒ a divides b * c

⊢ ∀m n. n divides m ⇒ ∀k. n divides k * m

⊢ ∀a b c. c ≠ 0 ⇒ (c * a divides c * b ⇔ a divides b)

⊢ ∀n m. n * m divides m ⇔ m = 0 ∨ n = 1

⊢ ∀a b c. c ≠ 0 ⇒ (a * c divides b * c ⇔ a divides b)

⊢ ∀n. ODD n ⇒ ∀m. m divides n ⇒ ODD m

⊢ ∀x. x divides 1 ⇔ x = 1

⊢ ∀a b c d. a divides c ∧ b divides d ⇒ a * b divides c * d

⊢ ∀a. a divides a

⊢ ∀a b c. a divides b ∧ a divides c ⇒ a divides b − c

⊢ ∀a b c. a divides b ∧ b divides c ⇒ a divides c

⊢ ∀x y z. 0 < z ⇒ (x DIV z = y DIV z ⇔ x − x MOD z = y − y MOD z)

⊢ ∀m n. 0 < n ⇒ (m DIV n = 0 ⇔ m < n)

⊢ ∀n. 0 < n ⇒ ∀k m. m MOD n = 0 ⇒ (k * n = m ⇔ k = m DIV n)

⊢ ∀x y z. 0 < y ∧ x ≤ y * z ⇒ x DIV y ≤ z

⊢ ∀x y. 0 < x ∧ 0 < y ∧ x ≤ y ⇒ ∀n. n DIV y ≤ n DIV x

⊢ ∀m n. 0 < m ⇒ (n DIV m = 0 ∧ n MOD m = 0 ⇔ n = 0)

⊢ ∀n. 0 < n ⇒ ∀q. n divides q ⇔ q DIV n * n = q

⊢ ∀n. 0 < n ⇒ ∀q. q DIV n * n ≤ q

⊢ ∀m n. 0 < m ∧ m ≤ n ⇒ 0 < n DIV m

⊢ ∀n. 0 < n ⇒ ∀x y. x * n = y ⇒ x = y DIV n

⊢ ∀n. 0 < n ⇒ ∀x y. n * x = y ⇒ x = y DIV n

⊢ ∀n. ∃p. n < p ∧ prime p

⊢ ∀n. ∃i. n < PRIMES i

⊢ ∀n. EVEN n ⇔ 2 divides n

⊢ a ** b divides a ** c ⇔ b ≤ c ∨ a = 0 ∧ 0 < c ∨ a = 0 ∧ b = 0 ∨ a = 1

⊢ ∀a b n. 0 < n ∧ a ** n divides b ⇒ a divides b

⊢ FACT 0 = 1

⊢ FACT 1 = 1

⊢ FACT 2 = 2

⊢ ∀n. 0 < n ⇒ FACT (n − 1) = FACT n DIV n

⊢ ∀n. FACT n = 1 ⇔ n ≤ 1

⊢ ∀n. FACT n = n ⇔ n = 1 ∨ n = 2

⊢ ∀n. 0 < n ⇒ n ≤ FACT n

⊢ ∀n. n < PRIMES n

⊢ ∀n. PRIMES n < PRIMES (SUC n)

⊢ ∀m n. 0 < m ∧ m ≤ n ⇒ m divides FACT n

⊢ ∀n. 0 < n ⇒ ∀k m. m MOD n = 0 ⇒ (m ≤ n * k ⇔ m DIV n ≤ k)

⊢ ∀m n. m < n ⇒ PRIMES m < PRIMES n

⊢ ∀n. 0 < n ⇒ ∀k m. m MOD n = 0 ⇒ (k * n < m ⇔ k < m DIV n)

⊢ ∀n. ∃i. n < PRIMES i ∧ ∀j. j < i ⇒ PRIMES j ≤ n

⊢ ∀a b. 0 < b ∧ b < a ⇒ ¬(a divides b)

⊢ ¬prime 0

⊢ ¬prime 1

⊢ ∀n. ODD n ⇔ ¬(2 divides n)

⊢ ∀n. 1 < n ⇒ 1 DIV n = 0

⊢ ∀a. 1 divides a

⊢ ∀p. prime p ⇒ 1 < p

⊢ ∀n. 1 < PRIMES n

⊢ ∀m n. PRIMES m = PRIMES n ⇒ m = n

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

⊢ ∀p. prime p ⇒ ∃i. PRIMES i = p

⊢ prime 2

⊢ prime 3

⊢ ∀n. n ≠ 1 ⇒ ∃p. prime p ∧ p divides n

⊢ ∀p. prime p ⇔ ∃i. p = PRIMES i

⊢ ∀p. prime p ⇒ 0 < p

⊢ ∀m n. 0 < n ∧ n ≤ m ⇒ (m − n) DIV n = m DIV n − 1

⊢ 0 divides m ⇔ m = 0

⊢ ∀n. 0 < PRIMES n

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

⊢ ∀m n. 0 < n ∧ m divides n ⇒ n DIV (n DIV m) = m

⊢ ∀n. 0 < n ⇒ ∀a b. a divides b ⇒ a divides b ** n

⊢ ∀a b c. c divides a ∧ c divides b ⇒ ∀h k. c divides h * a + k * b

⊢ ∀a b c.
    c divides a ∧ c divides b ⇒ ∀h k d. h * a = k * b + d ⇒ c divides d

⊢ ∀m n. 0 < n ∧ m divides n ⇒ 0 < m ∧ m ≤ n

⊢ ∀m n. 0 < n ∧ m divides n ⇒ 0 < m

⊢ ∀m n. n divides m * n ∧ n divides n * m

⊢ ∀n. prime (PRIMES n)

⊢ ∀n m.
    prime (n * m) ⇔ (n ≤ m ⇒ n = 1 ∧ prime m) ∧ (m ≤ n ⇒ m = 1 ∧ prime n)

⊢ ∀n. ∃p. prime p ∧ n < p

⊢ ∀m n. prime m ∧ prime n ∧ m divides n ⇒ m = n