This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| gcd-zero | ⊦ gcd(0, 0) = 0 | An Axiom |
| divides | ⊦ i | j ↔ (∃ i0. i * i0 = j) | An Axiom |
| gcd-div1 | ⊦ gcd(i, j) | i | An Axiom |
| gcd-div2 | ⊦ gcd(i, j) | j | An Axiom |
| gcd-max | ⊦ i0 | i ∧ i0 | j ∧ (i ≠ 0 ∨ j ≠ 0) → i0 ≤ gcd(i, j) | An Axiom |
| prime-def | ⊦ prime(j) ↔ 2 ≤ j ∧ (∀ i. 1 < i ∧ i < j → ¬ i | j) | An Axiom |
| max_prime_divisor-def | ⊦ j | i ∧ prime(j) ∧ j < i ∧ (∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i) → max_prime_divisor(i) = j | An Axiom |
| abs-gcd-not-less | ⊦ j ≠ 0 → (¬ abs(i) < gcd(i, j) ↔ i ≠ 0) | A User Theorem |
| abs-not-less | ⊦ j ≠ 0 → ¬ abs(j) < gcd(i, j) | A User Theorem |
| case-10 | 2 ≤ i, i < 10 ⊦ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i = 6 ∨ i = 7 ∨ i = 8 ∨ i = 9 | A User Theorem |
| case-20 | 10 ≤ i, i < 20 ⊦ i = 10 ∨ i = 11 ∨ i = 12 ∨ i = 13 ∨ i = 14 ∨ i = 15 ∨ i = 16 ∨ i = 17 ∨ i = 18 ∨ i = 19 | A User Theorem |
| case-30 | 20 ≤ i, i < 30 ⊦ i = 20 ∨ i = 21 ∨ i = 22 ∨ i = 23 ∨ i = 24 ∨ i = 25 ∨ i = 26 ∨ i = 27 ∨ i = 28 ∨ i = 29 | A User Theorem |
| case-40 | 30 ≤ i, i < 40 ⊦ i = 30 ∨ i = 31 ∨ i = 32 ∨ i = 33 ∨ i = 34 ∨ i = 35 ∨ i = 36 ∨ i = 37 ∨ i = 38 ∨ i = 39 | A User Theorem |
| coprime-divides | ⊦ gcd(i, j) = 1 ∧ i * i0 = j * j0 → i | j0 | A User Theorem |
| coprime-divides-01 | ⊦ gcd(i, j) = 1 ∧ i | j * j0 → i | j0 | A User Theorem |
| coprime-divides-02 | ⊦ gcd(i, j) = 1 ∧ ¬ i | j0 → ¬ i | j * j0 | A User Theorem |
| coprime-divides-03 | ⊦ gcd(i, j) = 1 ∧ ¬ i | j0 → ¬ i | j0 * j | A User Theorem |
| coprime-divides-04 | ⊦ gcd(i, j) = 1 ∧ ¬ i | j0 → i * i0 ≠ j * j0 | A User Theorem |
| coprime-mod-zero | ⊦ i0 % j ≠ 0 ∧ gcd(i, j) = 1 ∧ j ≠ 0 → (i * i0) % j ≠ 0 | A User Theorem |
| coprime-pot | ⊦ gcd(i, j) = 1 ∧ 1 < i ∧ 0 < j0 ∧ j ≠ 0 → i * i0 ≠ j ^ j0 | A User Theorem |
| div-abs | ⊦ i | abs(i) * j | A User Theorem |
| div-abs-01 | ⊦ i | abs(j) → i | j | A User Theorem |
| div-abs-02 | ⊦ i | abs(j) ↔ i | j | A User Theorem |
| div-abs-03 | ⊦ i | abs(i) | A User Theorem |
| div-abs-04 | ⊦ abs(i) | i | A User Theorem |
| div-div | ⊦ i | j ∧ j | i ∧ i ≤ 0 ∧ j ≤ 0 → (i ≠ j ↔ false) | A User Theorem |
| div-div-01 | ⊦ i | j ∧ j | i ∧ 0 ≤ i ∧ 0 ≤ j → (i ≠ j ↔ false) | A User Theorem |
| div-eq | ⊦ j | i ∧ j ≠ 0 → (i / j = i0 ↔ i = i0 * j) | A User Theorem |
| div-eq-one | ⊦ i | j ∧ i ≠ 0 → (j / i = 1 ↔ j = i) | A User Theorem |
| div-gcd-is-neg | ⊦ i0 < 0 → i0 / gcd(i, i0) ≤ 0 | A User Theorem |
| div-gcd-is-neg-01 | ⊦ i0 < 0 → ¬ 0 < i0 / gcd(i, i0) | A User Theorem |
| div-gcd-is-neg-01-01 | ⊦ i0 < 0 → ¬ 0 ≤ i0 / gcd(i, i0) | A User Theorem |
| div-gcd-neg-not-zero | ⊦ i0 < 0 → i0 / gcd(i, i0) ≠ 0 | A User Theorem |
| div-gcd-not-neg | ⊦ 0 < i → ¬ i / gcd(i, i0) ≤ 0 | A User Theorem |
| div-gcd-one | ⊦ i / gcd(i, 1) = i | A User Theorem |
| div-gcd-zero | ⊦ i ≠ 0 → i / gcd(i, i0) ≠ 0 | A User Theorem |
| div-mod | ⊦ 0 < j ∧ 0 ≤ i ∧ 0 ≤ i0 → (j | i - i0 ↔ i % j = i0 % j) | A User Theorem |
| div-mod-01 | ⊦ 0 < j ∧ 0 ≤ i0 ∧ i0 ≤ i → (j | i - i0 ↔ i % j = i0 % j) | A User Theorem |
| div-mod-zero | ⊦ j | i ∧ i ≠ 0 → i % j = 0 | A User Theorem |
| div-mod-zero-01 | ⊦ i % j = 0 ∧ j ≠ 0 → j | i | A User Theorem |
| div-mult | ⊦ i | i * j | A User Theorem |
| div-mult-01 | ⊦ i ≠ 0 → (i * i0 | i * i1 ↔ i0 | i1) | A User Theorem |
| div-mult-div | ⊦ 0 < j ∧ 1 < i → ¬ i * j | j | A User Theorem |
| div-mult-shift | ⊦ j | i ∧ j ≠ 0 → i / j * j0 = (i * j0) / j | A User Theorem |
| div-neg | ⊦ i | ~ j ↔ i | j | A User Theorem |
| div-not-ls | ⊦ i < j ∧ 0 < i → ¬ j | i | A User Theorem |
| div-one | ⊦ 1 | i | A User Theorem |
| div-one-neg-pos | ⊦ 0 < i → (i | ~1 ↔ i = 1) | A User Theorem |
| div-one-one | ⊦ i | 1 ↔ i = 1 ∨ i = ~1 | A User Theorem |
| div-one-one-neg | ⊦ i | ~1 ↔ i = 1 ∨ i = ~1 | A User Theorem |
| div-one-pos | ⊦ 0 < i → (i | 1 ↔ i = 1) | A User Theorem |
| div-zero | ⊦ i | i | A User Theorem |
| div-zero-01 | ⊦ i | 0 | A User Theorem |
| div-zero-zero | ⊦ 0 | i ↔ i = 0 | A User Theorem |
| divides-abs | ⊦ abs(i) | abs(j) ↔ i | j | A User Theorem |
| divides-abs-01 | ⊦ abs(i) | j ↔ i | j | A User Theorem |
| divides-abs-02 | ⊦ i | abs(j) * j0 ↔ i | j * j0 | A User Theorem |
| divides-add | ⊦ i | j → (i | j + j0 ↔ i | j0) | A User Theorem |
| divides-minus | ⊦ j | i - i0 ↔ j | i0 - i | A User Theorem |
| divides-mod | ⊦ i ≠ 0 → (i | j ↔ j % i = 0) | A User Theorem |
| divides-mone | ⊦ ~1 | j | A User Theorem |
| divides-mult | ⊦ j ≠ 0 → (i * j | j * i0 ↔ i | i0) | A User Theorem |
| divides-mult-01 | ⊦ i | j → i | j * j0 | A User Theorem |
| divides-mult-02 | ⊦ i | j ∧ i0 | j0 → i * i0 | j * j0 | A User Theorem |
| divides-mult-add | ⊦ i | i * j + j0 ↔ i | j0 | A User Theorem |
| divides-mult-sub | ⊦ i | i * j - j0 ↔ i | j0 | A User Theorem |
| divides-neg | ⊦ ~ i | j ↔ i | j | A User Theorem |
| divides-pot-prime | ⊦ prime(i) ∧ 0 < j0 ∧ j ≠ 0 → (i | j ^ j0 ↔ i | j) | A User Theorem |
| divides-prime | ⊦ prime(j) → (i | j ↔ abs(i) = j ∨ abs(i) = 1) | A User Theorem |
| exgcd-div | ⊦ ∃ i0. i / gcd(i, j) = i0 ∧ gcd(i, j) * i0 = i | A User Theorem |
| gcd-abs | ⊦ abs(gcd(i, j)) = gcd(i, j) | A User Theorem |
| gcd-abs-rew | ⊦ gcd(i, abs(j)) = gcd(i, j) | A User Theorem |
| gcd-abs-rew-01 | ⊦ gcd(abs(i), j) = gcd(i, j) | A User Theorem |
| gcd-abs-rew-02 | ⊦ gcd(i, j) = gcd(abs(i), abs(j)) | A User Theorem |
| gcd-add | ⊦ 0 < i ∧ 0 < j → gcd(i + j, j) = gcd(i, j) | A User Theorem |
| gcd-com | ⊦ gcd(i, j) = gcd(j, i) | A User Theorem |
| gcd-conq-one | 0 ≤ j, 0 ≤ i, gcd(i, j) = 1 ⊦ ∃ i0. 0 ≤ i0 ∧ j | i * i0 - 1 | A User Theorem |
| gcd-conq-one-01 | gcd(i, j) = 1 ⊦ ∃ i0. j | i * i0 - 1 | A User Theorem |
| gcd-div-eq | ⊦ i ≠ 0 → (i / gcd(i, j) = i0 ↔ i = i0 * gcd(i, j)) | A User Theorem |
| gcd-div-gcd | ⊦ i ≠ 0 → gcd(i / gcd(i, j), j / gcd(i, j)) = 1 | A User Theorem |
| gcd-div-gcd-pos | 0 < i, 0 < j ⊦ gcd(i / gcd(i, j), j / gcd(i, j)) = 1 | A User Theorem |
| gcd-div-mult | ⊦ i ≠ 0 ∧ j ≠ 0 → i / gcd(i, j) * gcd(i, j) = i | A User Theorem |
| gcd-div-mult-shift | ⊦ i ≠ 0 → i / gcd(i, j) * j0 = (i * j0) / gcd(i, j) | A User Theorem |
| gcd-div-rest | ⊦ abs(j0) < gcd(i, j) → (i = i1 * gcd(i, j) + j0 ↔ i = i1 * gcd(i, j) ∧ j0 = 0) | A User Theorem |
| gcd-div-shift | ⊦ i0 ≠ 0 → (i0 * j) / gcd(i0, j0) = i0 / gcd(i0, j0) * j | A User Theorem |
| gcd-divides | ⊦ gcd(i, j) | i * i0 | A User Theorem |
| gcd-divides-01 | ⊦ j0 | gcd(i, j) → j0 | j | A User Theorem |
| gcd-divides-both | ⊦ j | gcd(i, i0) → j | i ∧ j | i0 | A User Theorem |
| gcd-divides-both-h | 0 ≤ i, i < j, j0 | gcd(i, j) ⊦ j0 | j ∧ j0 | i | A User Theorem |
| gcd-ge-one | ⊦ i ≠ 0 → 1 ≤ gcd(i, j) | A User Theorem |
| gcd-less | ⊦ i1 | i ∧ i1 | j ∧ 0 ≠ i → i1 ≤ gcd(i, j) | A User Theorem |
| gcd-less-eq-zero | ⊦ gcd(i, j) ≤ 0 ↔ gcd(i, j) = 0 | A User Theorem |
| gcd-max-prop | i0 | i, i0 | j ⊦ i0 | gcd(i, j) | A User Theorem |
| gcd-mod-one | 1 < j, 1 < i, gcd(i, j) = 1 ⊦ ∃ i0. (i * i0) % j = 1 | A User Theorem |
| gcd-mod-one-01 | 1 < j, 1 < i, gcd(i, j) = 1 ⊦ ∃ i0. (i * i0) % j = 1 ∧ 0 < i0 | A User Theorem |
| gcd-mult | ⊦ gcd(i * i1, j * i1) = gcd(i, j) * abs(i1) | A User Theorem |
| gcd-mult-01 | ⊦ gcd(i, i * j) = abs(i) | A User Theorem |
| gcd-mult-pos | ⊦ 0 < i1 ∧ 0 < i ∧ 0 ≤ j → gcd(i * i1, j * i1) = gcd(i, j) * i1 | A User Theorem |
| gcd-mult-pos-01 | ⊦ 0 < i1 ∧ 0 < i ∧ 0 ≤ j → gcd(i1 * i, i1 * j) = gcd(i, j) * i1 | A User Theorem |
| gcd-neg | ⊦ gcd(~ i, j) = gcd(i, j) | A User Theorem |
| gcd-negone-eq | ⊦ ~1 = j2 / gcd(i2, j2) → gcd(i2, j2) = ~ j2 | A User Theorem |
| gcd-nls | ⊦ i ≠ 0 → ¬ abs(i) < gcd(i, j) | A User Theorem |
| gcd-nls-01 | ⊦ i ≠ 0 → ¬ abs(i) < gcd(abs(i), j) | A User Theorem |
| gcd-nls-zero | ⊦ 0 < i → ¬ i / gcd(i, j) < 0 | A User Theorem |
| gcd-one | ⊦ gcd(i, j) = 1 ↔ ¬(∃ i1. i1 > 1 ∧ i1 | i ∧ i1 | j) | A User Theorem |
| gcd-one-01 | ⊦ gcd(i, 1) = 1 | A User Theorem |
| gcd-one-eq | ⊦ j2 / gcd(i2, j2) = 1 → gcd(i2, j2) = j2 | A User Theorem |
| gcd-one-eq-01 | ⊦ i ≠ 0 → (abs(i) / gcd(i, j) = 1 ↔ gcd(i, j) = abs(i)) | A User Theorem |
| gcd-one-eq-02 | ⊦ j ≠ 0 → (abs(i) / gcd(i, j) = 1 ↔ gcd(i, j) = abs(i)) | A User Theorem |
| gcd-one-prime | ⊦ prime(i) ∧ ¬ i | j → gcd(i, j) = 1 | A User Theorem |
| gcd-pos | ⊦ 0 ≤ gcd(i, j) | A User Theorem |
| gcd-prime | ⊦ prime(j) ∧ 1 < i ∧ i < j → gcd(i, j) = 1 | A User Theorem |
| gcd-primes | ⊦ prime(i) ∧ prime(j) ∧ i ≠ j → gcd(i, j) = 1 | A User Theorem |
| gcd-rec | ⊦ j ≠ 0 → gcd(i, j) = gcd(abs(j), abs(i) % abs(j)) | A User Theorem |
| gcd-rec-pos | ⊦ 0 < j ∧ 0 ≤ i → gcd(i, j) = gcd(j, i % j) | A User Theorem |
| gcd-rec-sub | ⊦ 0 < i ∧ i < j → gcd(i, j) = gcd(i, j - i) | A User Theorem |
| gcd-rec-sub-01 | ⊦ gcd(i, j) = gcd(i, j - i) | A User Theorem |
| gcd-rec-sub-02 | ⊦ 0 < i ∧ i < j → gcd(i, j) = gcd(j, j - i) | A User Theorem |
| gcd-rec-sub-03 | ⊦ gcd(i, j) = gcd(j, j - i) | A User Theorem |
| gcd-same | ⊦ i ≠ 0 → gcd(i, i) = abs(i) | A User Theorem |
| gcd-same-01 | ⊦ 0 < j → gcd(j, j) = j | A User Theorem |
| gcd-same-02 | ⊦ gcd(abs(i), abs(i)) = abs(i) | A User Theorem |
| gcd-zero-02 | ⊦ ¬ gcd(i, j) < 0 | A User Theorem |
| gcd-zero-03 | ⊦ i ≠ 0 → gcd(i, 0) = abs(i) | A User Theorem |
| gcd-zero-04 | ⊦ gcd(i, 0) = abs(i) | A User Theorem |
| gcd-zero-05 | ⊦ gcd(i0, j0) + gcd(i, j) = 0 ↔ gcd(i0, j0) = 0 ∧ gcd(i, j) = 0 | A User Theorem |
| gcd-zero-zero | ⊦ gcd(i, j) = 0 ↔ i = 0 ∧ j = 0 | A User Theorem |
| gcdex | ⊦ ∃ i0, j0. gcd(i, j) = i * i0 + j * j0 | A User Theorem |
| gcdex-not-unique | gcd(i, j) = i * i0 + j * j0 ⊦ ∀ i1. gcd(i, j) = i * (i0 - i1 * j) + j * (j0 + i1 * i) | A User Theorem |
| gcdex-pos | j ≠ 0 ⊦ ∃ i0, j0. gcd(i, j) = i * i0 + j * j0 ∧ 0 ≤ i0 | A User Theorem |
| gcdex-smallest-pos | j ≠ 0 ⊦ ∃ i0, j0. gcd(i, j) = i * i0 + j * j0 ∧ 0 ≤ i0 ∧ (∀ i1. 0 ≤ i1 ∧ i1 < i0 → ¬(∃ j1. gcd(i, j) = i * i1 + j * j1)) | A User Theorem |
| gcdhex | 0 ≤ i, 0 ≤ j, j ≤ i ⊦ ∃ i0, j0. gcd(i, j) = i * i0 + j * j0 | A User Theorem |
| isSquare-mult | ⊦ isSquare(j * i * i) ↔ isSquare(j) ∨ i = 0 | A User Theorem |
| isSquare-mult-aux | j0 * j0 = j * i * i, 0 < j0, 0 < j, 0 < i ⊦ i = 0, isSquare(j) | A User Theorem |
| max_prime_divisor-abs | ⊦ ¬ prime(i) ∧ 2 ≤ i → abs(i / max_prime_divisor(i)) = i / max_prime_divisor(i) | A User Theorem |
| max_prime_divisor-abs-01 | ⊦ ¬ prime(i) ∧ 2 ≤ i → abs(max_prime_divisor(i)) = max_prime_divisor(i) | A User Theorem |
| max_prime_divisor-divides | ⊦ ¬ prime(i) ∧ 2 ≤ i → max_prime_divisor(i) | i | A User Theorem |
| max_prime_divisor-divides-01 | ⊦ ¬ prime(i) ∧ 2 ≤ i → i % max_prime_divisor(i) = 0 | A User Theorem |
| max_prime_divisor-divides-02 | ⊦ ¬ j | i ∧ prime(j) ∧ ¬ prime(i) ∧ 2 ≤ i → ¬ j | i / max_prime_divisor(i) | A User Theorem |
| max_prime_divisor-divides-03 | ⊦ ¬ prime(i) ∧ 2 ≤ i ∧ prime(j) ∧ j | i ∧ j ≠ max_prime_divisor(i) → j | i / max_prime_divisor(i) | A User Theorem |
| max_prime_divisor-ge2 | ⊦ ¬ prime(i) ∧ 2 ≤ i → 2 ≤ i / max_prime_divisor(i) | A User Theorem |
| max_prime_divisor-nle | ⊦ ¬ prime(i) ∧ 2 ≤ i → ¬ i ≤ max_prime_divisor(i) | A User Theorem |
| max_prime_divisor-nle-01 | ⊦ ¬ prime(i) ∧ 2 ≤ i → ¬ i ≤ i / max_prime_divisor(i) | A User Theorem |
| max_prime_divisor-nle-zero | ⊦ ¬ prime(i) ∧ 2 ≤ i → ¬ max_prime_divisor(i) ≤ 0 | A User Theorem |
| max_prime_divisor-nle-zero-01 | ⊦ ¬ prime(i) ∧ 2 ≤ i → ¬ i / max_prime_divisor(i) ≤ 0 | A User Theorem |
| max_prime_divisor-nls | ⊦ ¬ prime(i) ∧ 2 ≤ i → ¬ i < i / max_prime_divisor(i) | A User Theorem |
| max_prime_divisor-nls-01 | ⊦ ¬ prime(i) ∧ 2 ≤ i → ¬ i < max_prime_divisor(i) | A User Theorem |
| max_prime_divisor-nls-02 | ⊦ ¬ prime(i / max_prime_divisor(i)) ∧ ¬ prime(i) ∧ 2 ≤ i → ¬ max_prime_divisor(i) < max_prime_divisor(i / max_prime_divisor(i)) | A User Theorem |
| max_prime_divisor-nls-03 | ⊦ prime(i / max_prime_divisor(i)) ∧ ¬ prime(i) ∧ 2 ≤ i → ¬ max_prime_divisor(i) < i / max_prime_divisor(i) | A User Theorem |
| max_prime_divisor-nls-zero | ⊦ ¬ prime(i) ∧ 2 ≤ i → ¬ max_prime_divisor(i) < 0 | A User Theorem |
| max_prime_divisor-not-zero | ⊦ ¬ prime(i) ∧ 2 ≤ i → max_prime_divisor(i) ≠ 0 | A User Theorem |
| max_prime_divisor-prime | ⊦ ¬ prime(i) ∧ 2 ≤ i → prime(max_prime_divisor(i)) | A User Theorem |
| mod-gcd | ⊦ i ≠ 0 → i % gcd(i, j) = 0 | A User Theorem |
| mod-gcd-01 | ⊦ j ≠ 0 → i % gcd(i, j) = 0 | A User Theorem |
| mod-square-10 | ⊦ (i * i) % 10 = 0 ↔ i % 10 = 0 | A User Theorem |
| not-less-gcd | ⊦ 0 < i → ¬ i < gcd(i, j) | A User Theorem |
| num-gcd-pos | ⊦ 0 < j ∧ j < i → gcd((* i), (* j)) = gcd(j, i % j) | A User Theorem |
| pot-isSquare | ⊦ 0 < i ∧ 0 < j → (isSquare(i ^ j) ↔ isSquare(i) ∨ even(j)) | A User Theorem |
| prime-11 | ⊦ prime(11) | A User Theorem |
| prime-1259 | ⊦ prime(1259) | A User Theorem |
| prime-13 | ⊦ prime(13) | A User Theorem |
| prime-163 | ⊦ prime(163) | A User Theorem |
| prime-23 | ⊦ prime(23) | A User Theorem |
| prime-29 | ⊦ prime(29) | A User Theorem |
| prime-317 | ⊦ prime(317) | A User Theorem |
| prime-43 | ⊦ prime(43) | A User Theorem |
| prime-5 | ⊦ prime(5) | A User Theorem |
| prime-631 | ⊦ prime(631) | A User Theorem |
| prime-7 | ⊦ prime(7) | A User Theorem |
| prime-83 | ⊦ prime(83) | A User Theorem |
| prime-abs | ⊦ prime(j) → abs(j) = j | A User Theorem |
| prime-def-mod | ⊦ 1 < j → (prime(j) ↔ (∀ i. 1 < i ∧ i * i ≤ j → j % i ≠ 0)) | A User Theorem |
| prime-def-prime | ⊦ 1 < i → (prime(i) ↔ (∀ j. prime(j) ∧ j * j ≤ i → ¬ j | i)) | A User Theorem |
| prime-divides | ⊦ prime(i) → (i | j * j0 ↔ i | j ∨ i | j0) | A User Theorem |
| prime-divides-01 | ⊦ prime(i) ∧ j0 | j ∧ j0 < i ∧ i | j ∧ 0 < j0 → i | j / j0 | A User Theorem |
| prime-divides-one | ⊦ prime(i) → ¬ i | 1 | A User Theorem |
| prime-ex-max | ⊦ ¬ prime(i) ∧ 2 ≤ i → (∃ j. prime(j) ∧ j | i ∧ j < i ∧ (∀ j0. j < j0 ∧ j0 < i ∧ prime(j0) → ¬ j0 | i)) | A User Theorem |
| prime-le-2 | ⊦ prime(i) → (i ≤ 2 ↔ i = 2) | A User Theorem |
| prime-mult-eq | ⊦ prime(i) ∧ ¬ i | j → i * i0 ≠ j | A User Theorem |
| prime-mult-not | ⊦ 1 < i ∧ 1 < j → ¬ prime(i * j) | A User Theorem |
| prime-not-four | ⊦ ¬ prime(4) | A User Theorem |
| prime-not-neg | ⊦ j < 0 → ¬ prime(j) | A User Theorem |
| prime-not-neg-01 | ⊦ j ≤ 0 → ¬ prime(j) | A User Theorem |
| prime-not-odd | ⊦ ¬ odd(j) → (prime(j) ↔ j = 2) | A User Theorem |
| prime-odd | ⊦ prime(j) ∧ j ≠ 2 → j % 2 = 1 | A User Theorem |
| prime-odd-01 | ⊦ prime(j) ∧ j ≠ 2 → (j - 1) % 2 = 0 | A User Theorem |
| prime-one | ⊦ i ≤ 1 → ¬ prime(i) | A User Theorem |
| prime-small | ⊦ j < 2 → ¬ prime(j) | A User Theorem |
| prime-three | ⊦ prime(3) | A User Theorem |
| prime-two | ⊦ prime(2 * j) ↔ j = 1 | A User Theorem |
| prime-two-01 | ⊦ prime(2) | A User Theorem |
| square-neq-any | j ≠ 0 ∨ j0 ≠ 0, j * j = i * j0 * j0 ⊦ ∃ i0. i = i0 * i0 | A User Theorem |
| square-neq-any-pos | 0 < i, j ≠ 0 ∨ j0 ≠ 0, j * j = i * j0 * j0 ⊦ ∃ i0. i = i0 * i0 | A User Theorem |
| square-neq-any-pos-01 | 0 < i, 0 < j, 0 < j0, j * j = i * j0 * j0 ⊦ ∃ i0. i = i0 * i0 | A User Theorem |
| square-neq-any-pos-02 | 0 < i, 0 < j, 0 < j0, gcd(j, j0) = 1, j * j = i * j0 * j0 ⊦ ∃ i0. i = i0 * i0 | A User Theorem |
| square-neq-pos | ⊦ prime(i) ∧ 0 < j ∧ 0 ≤ j0 → j * j ≠ i * j0 * j0 | A User Theorem |
| square-neq-pos-h | ⊦ prime(i) ∧ gcd(j, j0) = 1 ∧ 0 < j ∧ 0 ≤ j0 → j * j ≠ i * j0 * j0 | A User Theorem |
| square-neq-prime | ⊦ prime(i) ∧ (j ≠ 0 ∨ j0 ≠ 0) → j * j ≠ i * j0 * j0 | A User Theorem |
| square-prime-eq | ⊦ prime(j) ∧ ¬ j | i → i * i ≠ j * j0 | A User Theorem |