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: |
|---|---|---|
| Mod-def | ⊦ j ≠ 0 → i = i / j * j + i % j | An Axiom |
| Div-right | ⊦ j ≠ 0 → i / ~ j = ~(i / j) | An Axiom |
| Div-left | ⊦ j ≠ 0 → ~ i / j = ~(i / j) | An Axiom |
| Div-def | ⊦ 0 ≤ i ∧ 0 < j → i / j * j ≤ i ∧ i < (i / j)+1 * j | An Axiom |
| abs | j ≠ 0 ⊦ abs(i / j) = abs(i) / abs(j) | A User Theorem |
| abs-01 | j ≠ 0 ⊦ abs(i / abs(j)) = abs(i / j) | A User Theorem |
| abs-02 | j ≠ 0 ⊦ abs(abs(i) / j) = abs(i / j) | A User Theorem |
| abs-03 | 0 ≠ j ⊦ abs(i) / j * abs(i) / j = i / j * i / j | A User Theorem |
| abs-div10-le | ⊦ abs(i) ≤ abs(i) / 10 ↔ i = 0 | A User Theorem |
| abs-intro | ⊦ 0 ≤ i ∧ 0 < j ∨ i < 0 ∧ j < 0 → i / j = abs(i) / abs(j) | A User Theorem |
| abs-shift | ⊦ j ≠ 0 → abs(i % j) = abs(i) % abs(j) | A User Theorem |
| abs-shift-01 | ⊦ j ≠ 0 → abs(i % j) = abs(i) % j | A User Theorem |
| add-div-mult | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → (i / j + i0 / j) + (i % j + i0 % j) / j = (i + i0) / j | A User Theorem |
| div-abs | ⊦ i ≠ 0 → i / abs(i) ≠ 0 | A User Theorem |
| div-add-both | ⊦ i % j = 0 ∧ i0 % j = 0 ∧ 0 ≠ j → (i + i0) / j = i / j + i0 / j | A User Theorem |
| div-add-neg | ⊦ i0 % j = 0 ∧ i < 0 ∧ i0 < 0 ∧ 0 < j → (i + i0) / j = i / j + i0 / j | A User Theorem |
| div-add-nosucc | ⊦ 1 < j ∧ 0 ≤ i ∧ i % j = 0 → (i + (j - 1)) / j = i / j | A User Theorem |
| div-add-nosucc-neg | ⊦ 1 < j ∧ i < 0 ∧ i % j = 0 → (i - (j - 1)) / j = i / j | A User Theorem |
| div-add-pos | ⊦ i0 % j = 0 ∧ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → (i + i0) / j = i / j + i0 / j | A User Theorem |
| div-add-rew | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → (i + i0) / j = i / j + i0 / j + (i % j + i0 % j) / j | A User Theorem |
| div-add-succ | ⊦ 1 < j ∧ 0 < i ∧ i % j ≠ 0 → (i + (j - 1)) / j = i / j + 1 | A User Theorem |
| div-add-succ-neg | ⊦ 1 < j ∧ i < 0 ∧ i % j ≠ 0 → (i - (j - 1)) / j = i / j - 1 | A User Theorem |
| div-add1-negneg | ⊦ i % j = 0 ∧ i < 0 ∧ i0 < 0 ∧ 0 < j → (i + i0) / j = i / j + i0 / j | A User Theorem |
| div-add1-negpos-neg | ⊦ i % j = 0 ∧ i + i0 < 0 ∧ i0 % j = 0 ∧ i < 0 ∧ 0 ≤ i0 ∧ 0 < j → (i + i0) / j = i / j + i0 / j | A User Theorem |
| div-add1-negpos-neg-01 | ⊦ i % j = 0 ∧ i + i0 < 0 ∧ i0 % j ≠ 0 ∧ i < 0 ∧ 0 ≤ i0 ∧ 0 < j → (i + i0) / j = i / j + i0 / j + 1 | A User Theorem |
| div-add1-negpos-neg-02 | ⊦ i % j = 0 ∧ i + i0 < 0 ∧ i < 0 ∧ 0 ≤ i0 ∧ 0 < j → (i + i0) / j = i / j + (i0 + (j - 1)) / j | A User Theorem |
| div-add1-negpos-pos | ⊦ i % j = 0 ∧ 0 ≤ i + i0 ∧ i < 0 ∧ 0 ≤ i0 ∧ 0 < j → (i + i0) / j = i / j + i0 / j | A User Theorem |
| div-add1-posneg-neg | ⊦ i % j = 0 ∧ i + i0 < 0 ∧ 0 ≤ i ∧ i0 < 0 ∧ 0 < j → (i + i0) / j = i / j + i0 / j | A User Theorem |
| div-add1-posneg-pos | ⊦ i % j = 0 ∧ 0 ≤ i + i0 ∧ i0 % j = 0 ∧ 0 ≤ i ∧ i0 < 0 ∧ 0 < j → (i + i0) / j = i / j + i0 / j | A User Theorem |
| div-add1-posneg-pos-01 | ⊦ i % j = 0 ∧ 0 ≤ i + i0 ∧ i0 % j ≠ 0 ∧ 0 ≤ i ∧ i0 < 0 ∧ 0 < j → (i + i0) / j = i / j + i0 / j - 1 | A User Theorem |
| div-add1-posneg-pos-02 | ⊦ i % j = 0 ∧ 0 ≤ i + i0 ∧ 0 ≤ i ∧ i0 < 0 ∧ 0 < j → (i + i0) / j = i / j + (i0 - (j - 1)) / j | A User Theorem |
| div-add1-pospos | ⊦ i % j = 0 ∧ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → (i + i0) / j = i / j + i0 / j | A User Theorem |
| div-addthree-rew | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 ≤ i1 ∧ 0 < j → (i + i0 + i1) / j = i / j + i0 / j + i1 / j + (i % j + i0 % j + i1 % j) / j | A User Theorem |
| div-am-rew | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j ∧ 0 ≤ i1 → (i + i0 * i1) / j = (i + i0 * i1 % j) / j + i0 * i1 / j | A User Theorem |
| div-div | ⊦ j ≠ 0 ∧ j0 ≠ 0 → (i / j) / j0 = i / (j * j0) | A User Theorem |
| div-div-intro | ⊦ j ≠ 0 ∧ j0 ≠ 0 → i / (j * j0) = (i / j) / j0 | A User Theorem |
| div-div-num | j ≠ 0, j0 ≠ 0 ⊦ (i / (* j)) / (* j0) = i / (j * j0) | A User Theorem |
| div-div-pos | ⊦ 0 ≤ i ∧ 0 < j ∧ 0 < j0 → (i / j) / j0 = i / (j * j0) | A User Theorem |
| div-div-pred | ⊦ i < 0 → ((i - 1) / 2 - 1) / 2 = (i - 3) / 4 | A User Theorem |
| div-div-pred-01 | ⊦ i < 0 → ((i - 3) / 4 - 1) / 2 = (i - 7) / 8 | A User Theorem |
| div-div-switch | ⊦ j ≠ 0 ∧ i ≠ 0 ∧ i % j = 0 → i1 / i / j = (i1 * j) / i | A User Theorem |
| div-elim | ⊦ 0 < j ∧ 0 < i → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ 0 ≤ j0 ∧ j0 < j) | A User Theorem |
| div-elim-divides | ⊦ 0 ≠ j ∧ i % j = 0 → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ j0 = 0) | A User Theorem |
| div-elim-negneg | ⊦ j < 0 ∧ i < 0 → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ j0 ≤ 0 ∧ j < j0 ∧ 0 ≤ i0) | A User Theorem |
| div-elim-negpos | ⊦ 0 < j ∧ i < 0 → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ j0 ≤ 0 ∧ abs(j0) < j ∧ i0 ≤ 0) | A User Theorem |
| div-elim-pos | ⊦ 0 < j ∧ 0 ≤ i → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ 0 ≤ j0 ∧ j0 < j) | A User Theorem |
| div-elim-posneg | ⊦ j < 0 ∧ 0 ≤ i → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ 0 ≤ j0 ∧ j0 < abs(j) ∧ i0 ≤ 0) | A User Theorem |
| div-elim-pospos | ⊦ 0 < j ∧ 0 ≤ i → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ 0 ≤ j0 ∧ j0 < j ∧ 0 ≤ i0) | A User Theorem |
| div-elim1 | ⊦ j < 0 ∧ 0 ≤ i → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ 0 ≤ j0 ∧ j0 < abs(j)) | A User Theorem |
| div-elim2 | ⊦ 0 < j ∧ i < 0 → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ j0 ≤ 0 ∧ abs(j0) < j) | A User Theorem |
| div-elim3 | ⊦ j < 0 ∧ i < 0 → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ j0 ≤ 0 ∧ j < j0) | A User Theorem |
| div-eq-same | ⊦ 0 ≠ j → (j * i / j = i ↔ i % j = 0) | A User Theorem |
| div-eq-same-01 | j ≠ 0 ⊦ i / j = i ↔ i = 0 ∨ j = 1 | A User Theorem |
| div-eq-zero | ⊦ 0 < i ∧ 0 < j → (i / j = 0 ↔ i < j) | A User Theorem |
| div-eq-zero-01 | ⊦ 0 ≠ j → (i / j = 0 ↔ abs(i) < abs(j)) | A User Theorem |
| div-est-denom-pos | ⊦ ¬ i0 ≤ i / j ∧ j ≤ j0 ∧ 0 ≤ i ∧ 0 < j → ¬ i0 ≤ i / j0 | A User Theorem |
| div-est-nle-pos | ⊦ ¬ i0 * j ≤ i ∧ 0 ≤ i ∧ 0 < j → ¬ i0 ≤ i / j | A User Theorem |
| div-est-nls | ⊦ ¬ i < i0 ∧ 0 ≤ i0 ∧ 0 < j → ¬ i / j < i0 / j | A User Theorem |
| div-est-num | ⊦ ¬ i / j < j0 ∧ i ≤ i0 ∧ 0 < j → ¬ i0 / j < j0 | A User Theorem |
| div-le-modnotzero | ⊦ i % j ≠ 0 ∧ 0 < j ∧ 0 ≤ i → (i0 ≤ i / j ↔ i0 * j < i) | A User Theorem |
| div-le-modnotzero-01 | ⊦ 0 ≤ i ∧ 0 < j → (i / j ≤ i0 ↔ ¬ i0 * j ≤ i ∨ i0 = i / j) | A User Theorem |
| div-le-modzero | ⊦ i % j = 0 ∧ 0 < j → (i0 ≤ i / j ↔ i0 * j ≤ i) | A User Theorem |
| div-le-modzero-01 | ⊦ i % j = 0 ∧ 0 ≤ i ∧ 0 < j → (i / j ≤ i0 ↔ ¬ i0 * j < i) | A User Theorem |
| div-le-pos | ⊦ j0 ≤ i / j ∧ i ≤ i0 ∧ 0 < j → j0 ≤ i0 / j | A User Theorem |
| div-le-same | ⊦ 0 < i ∧ 0 < j → (i ≤ i / j ↔ j = 1) | A User Theorem |
| div-le-same-neg | ⊦ i < 0 ∧ 0 < j → (i / j ≤ i ↔ i = 0 ∨ j = 1) | A User Theorem |
| div-lezero | ⊦ 0 < j → (i / j ≤ 0 ↔ i < j) | A User Theorem |
| div-ls | j0 ≤ i / j, i < i0, i0 % j = 0, 0 < j, 0 ≤ i ⊦ j0 < i0 / j | A User Theorem |
| div-ls-01 | i < i0, i0 % j = 0, 0 < j, 0 ≤ i ⊦ i / j < i0 / j | A User Theorem |
| div-ls-02 | 0 < j0, 0 ≤ i, i ≤ j, i / j0 ≠ j / j0 ⊦ i / j0 < j / j0 | A User Theorem |
| div-ls-modnotzero | ⊦ 0 ≤ i ∧ 0 < j → (i0 < i / j ↔ i0 * j ≤ i ∧ i0 ≠ i / j) | A User Theorem |
| div-ls-modzero | ⊦ i % j = 0 ∧ 0 ≤ i ∧ 0 < j → (i0 < i / j ↔ i0 * j < i) | A User Theorem |
| div-ls-mone | 0 < j ⊦ i / (* j) < ~1 ↔ i + 2 * j ≤ 0 | A User Theorem |
| div-ls-pos-better | ⊦ 0 < j ∧ 0 ≤ i → (i / j < j0 ↔ i < j * j0) | A User Theorem |
| div-ls-pos-mon | i < i0 / j, i0 ≤ i1, 0 ≤ i0, 0 < j ⊦ i < i1 / j | A User Theorem |
| div-ls-same | ⊦ 0 < j → (i < i / j ↔ i < 0 ∧ 1 < j) | A User Theorem |
| div-ls-zero | 0 < j ⊦ i / (* j) < 0 ↔ i + j ≤ 0 | A User Theorem |
| div-minus-onediff | ⊦ i % j ≠ 0 ∧ j0 = j - 1 ∧ i < 0 ∧ 0 < j → (i - j0) / j = i / j - 1 | A User Theorem |
| div-minus-onediff-01 | ⊦ i % j = 0 ∧ j0 = j - 1 ∧ i < 0 ∧ 0 < j → (i - j0) / j = i / j | A User Theorem |
| div-minus255-256 | ⊦ i % 256 ≠ 0 ∧ i < 0 → (i - 255) / 256 = i / 256 - 1 | A User Theorem |
| div-minus255-256-01 | ⊦ i % 256 = 0 ∧ i < 0 → (i - 255) / 256 = i / 256 | A User Theorem |
| div-mone | ⊦ j + 1 = 0 → i / j = ~ i | A User Theorem |
| div-mone-01 | ⊦ i / ~1 = ~ i | A User Theorem |
| div-mult | j ≠ 0 ⊦ (j * i) / j = i | A User Theorem |
| div-mult-01 | j ≠ 0, i0 ≠ 0 ⊦ (i * i0) / (j * i0) = i / j | A User Theorem |
| div-mult-02 | 0 < j, 0 < i0, 0 ≤ i ⊦ (i * i0) / (j * i0) = i / j | A User Theorem |
| div-mult-03 | j ≠ 0 ⊦ (i * j) / j = i | A User Theorem |
| div-mult-le | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → i * i0 / j ≤ (i * i0) / j | A User Theorem |
| div-mult-le-01 | ⊦ 0 ≤ i ∧ 0 < j → (i ≤ j * i / j ↔ i % j = 0) | A User Theorem |
| div-mult-ls | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → ¬ (i * i0) / j < i * i0 / j | A User Theorem |
| div-mult-ls-pos | ⊦ i % j ≠ 0 ∧ 0 ≤ i ∧ 0 < j → i / j * j < i | A User Theorem |
| div-mult-neg | ⊦ 0 < j ∧ i ≤ 0 ∧ i0 ≤ 0 ∧ abs(i0) < j → (j * i + i0) / j = i | A User Theorem |
| div-mult-nle-est | 0 < i, 0 ≤ j ⊦ ¬ j / i ≤ i0 → ¬ j ≤ i * i0 | A User Theorem |
| div-mult-nls-est | 0 < i, 0 ≤ j ⊦ ¬ j / i < i0 → ¬ j < i * i0 | A User Theorem |
| div-mult-nls-est-01 | 0 < i, 0 ≤ j ⊦ ¬ i0 ≤ j / i → ¬ i * i0 < j | A User Theorem |
| div-mult-nls-zero | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → ¬ (i * i0) / j < 0 | A User Theorem |
| div-mult-num | j ≠ 0, j0 % j = 0 ⊦ (i * (* j0)) / (* j) = i * j0 / j | A User Theorem |
| div-mult-num-01 | j % j0 = 0, j ≠ 0, j0 ≠ 0 ⊦ (i * (* j0)) / (* j) = i / j / j0 | A User Theorem |
| div-mult-pos | ⊦ 0 < j ∧ 0 ≤ i ∧ 0 ≤ i0 ∧ i0 < j → (j * i + i0) / j = i | A User Theorem |
| div-mult-pos-01 | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → (i + i0 * j) / j = i / j + i0 | A User Theorem |
| div-mult-pos-02 | ⊦ 0 < j ∧ 0 ≤ i ∧ 0 ≤ i0 ∧ i0 < j → (i * j + i0) / j = i | A User Theorem |
| div-mult-pos-03 | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → (i + j * i0) / j = i / j + i0 | A User Theorem |
| div-mult-pos-rew | ⊦ 0 < j ∧ 0 ≤ i ∧ 0 ≤ i0 → i / j + i0 = (i + i0 * j) / j | A User Theorem |
| div-mult-rew | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → (i * i0) / j = i / j * i0 + (i % j * i0) / j | A User Theorem |
| div-mult-rew-01 | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → i / j * i0 = (i * i0) / j - (i % j * i0) / j | A User Theorem |
| div-mult-shift-holds | ⊦ i % j * i0 < j ∧ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → (i * i0) / j = i / j * i0 | A User Theorem |
| div-mult-three | ⊦ 2 < i → 0 < (2 * i) / 3 | A User Theorem |
| div-mult-three-nls | ⊦ 2 ≤ j → ¬ (j * j * j) / 3 < j | A User Theorem |
| div-mult-two-nls | ⊦ 0 ≤ i ∧ 0 < j → ¬ (2 * i) / j < 2 * i / j | A User Theorem |
| div-mult-two-nls-01 | ⊦ 0 ≤ i ∧ 0 < j → ¬ 1 + 2 * i / j < (2 * i) / j | A User Theorem |
| div-nearer-zero | j ≠ 0 ⊦ abs(i / j * j) ≤ abs(i) | A User Theorem |
| div-ngr-zero | ⊦ i < 0 ∧ 0 < j → (0 ≤ i / j ↔ abs(i) < j) | A User Theorem |
| div-nle | ⊦ 0 < j ∧ i < i0 ∧ 0 ≤ i → ¬ i0 ≤ i / j | A User Theorem |
| div-nls | ⊦ ¬ i0 < i ∧ 0 ≤ i ∧ 0 < j → ¬ i0 < i / j | A User Theorem |
| div-nls-01 | ⊦ ¬ i0 < abs(i) ∧ i ≤ 0 ∧ j < 0 → ¬ i0 < i / j | A User Theorem |
| div-rec | 0 < j, j ≤ i ⊦ i / j = (i - j) / j + 1 | A User Theorem |
| div-rec-01 | j < 0, i ≤ j ⊦ i / j = (i - j) / j + 1 | A User Theorem |
| div-same | i ≠ 0 ⊦ i / i = 1 | A User Theorem |
| div-shift-two | i0 = (i / 2) / j * 2, j ≠ 0, 0 ≤ i, 0 ≤ j ⊦ i / j = i0 + (i - j * i0 < j ⊃ 0;1) | A User Theorem |
| div-sub | j ≠ 0 ⊦ (j - i * j) / j = 1 - i | A User Theorem |
| div-sub-01 | j ≠ 0, i % j = 0, i0 % j = 0 ⊦ i / j - i0 / j = (i - i0) / j | A User Theorem |
| div-sum-ls | ⊦ 0 ≤ i ∧ 0 ≤ i1 ∧ 0 < i + i1 ∧ 0 < j1 ∧ 0 < j2 ∧ 0 < j ∧ j1 < j ∧ j2 < j → (i * j1 + i1 * j2) / j < i + i1 | A User Theorem |
| div-sum-ls-01 | ⊦ 0 < i ∧ 0 < i1 ∧ 0 < j1 ∧ 0 < j2 ∧ 0 < j ∧ j1 < j ∧ j2 < j → (i * j1 + i1 * j2) / j < i + i1 | A User Theorem |
| div-two | ⊦ 0 ≤ i → (2 * i + 1) / 2 = i | A User Theorem |
| div-two-01 | j ≠ 0 ⊦ (2 * i) / (2 * j) = i / j | A User Theorem |
| div-two-intro | ⊦ j % 2 = 0 ∧ j ≠ 0 → i / j = (i / 2) / j / 2 | A User Theorem |
| div-two-zero | ⊦ 0 < i → (i / 2 = 0 ↔ i = 1) | A User Theorem |
| div-two-zero-01 | ⊦ 0 ≤ i / 2 ↔ ~1 ≤ i | A User Theorem |
| div-twoodd | 0 ≤ i, 0 < j ⊦ (2 * i + 1) / (2 * j) = i / j | A User Theorem |
| div-twoodd-01 | ⊦ i < 0 ∧ i % 2 = 0 → (i - 1) / 2 = i / 2 | A User Theorem |
| div-twoodd-02 | 0 ≤ i, j < 0 ⊦ (2 * i + 1) / (2 * j) = i / j | A User Theorem |
| div-twoodd-03 | i < 0, 0 < j ⊦ (2 * i - 1) / (2 * j) = i / j | A User Theorem |
| div-twoodd-04 | i < 0, j < 0 ⊦ (2 * i - 1) / (2 * j) = i / j | A User Theorem |
| div-twoodd-05 | i < 0, 0 < j ⊦ (2 * i + 1) / (2 * j) = (i + 1) / j | A User Theorem |
| div-twoodd-06 | 0 ≤ i, j ≠ 0 ⊦ (2 * i + 1) / (2 * j) = i / j | A User Theorem |
| div-twoodd-07 | i < 0, j < 0 ⊦ (2 * i + 1) / (2 * j) = (i + 1) / j | A User Theorem |
| div-zero | 0 < j, 0 ≤ i, i < j ⊦ i / j = 0 | A User Theorem |
| div-zero-01 | 0 < j, i < 0, abs(i) < j ⊦ i / j = 0 | A User Theorem |
| div-zero-02 | abs(i) < abs(j) ⊦ i / j = 0 | A User Theorem |
| div-zero-03 | 0 < j ⊦ 0 ≤ i ∧ i < j → i / (* j) = 0 | A User Theorem |
| div-zero-04 | 0 < j ⊦ 0 < i ∧ i < j → i / (* j) = 0 | A User Theorem |
| div-zero-05 | ⊦ i < j ∧ 0 < j ∧ 0 ≤ i → i / j = 0 | A User Theorem |
| div-zero-06 | ⊦ i < j ∧ 0 < j ∧ 0 < i → i / j = 0 | A User Theorem |
| div-zero-ngr | ⊦ i < 0 ∧ 0 < j → ¬ 0 < i / j | A User Theorem |
| div-zero-ngr-01 | ⊦ 0 ≤ i ∧ j < 0 → ¬ 0 < i / j | A User Theorem |
| div-zero-nls | ⊦ 0 ≤ i ∧ 0 < j → ¬ i / j < 0 | A User Theorem |
| div-zero-nls-01 | ⊦ j ≠ 0 → ¬ abs(i) / abs(j) < 0 | A User Theorem |
| div2-add-neg | ⊦ j % 2 = 0 ∧ i ≤ 0 ∧ abs(i) ≤ j → (i + j) / 2 = (i - 1) / 2 + j / 2 | A User Theorem |
| div2-neg | ⊦ i / 2 < 0 → i < 0 | A User Theorem |
| div2-neg-01 | ⊦ j < 0 → ¬ j / 2 ≤ j | A User Theorem |
| div2-neg-odd | ⊦ j < 0 → (j * 2 - 1) / 2 = j | A User Theorem |
| div2-nle | ⊦ 0 < i → ¬ i ≤ i / 2 | A User Theorem |
| div2-nle-01 | ⊦ 1 < i → ¬ i / 2 ≤ 0 | A User Theorem |
| div2-nle-02 | ⊦ 0 ≤ i ∧ i < j → ¬ j ≤ (i + j) / 2 | A User Theorem |
| div2-nls | ⊦ i ≤ j → ¬ j < (i + j) / 2 | A User Theorem |
| div2-nls-01 | ⊦ i < j → ¬ j < (i + j) / 2 | A User Theorem |
| div2-nls-02 | ⊦ i ≤ j → ¬ (i + j) / 2 < i | A User Theorem |
| div2-nls-03 | ⊦ i < j → ¬ (i + j) / 2 < i | A User Theorem |
| div2-notzero | ⊦ j < 0 → (j - 1) / 2 ≠ 0 | A User Theorem |
| div2-odd | i % 2 = 0, 0 ≤ i ⊦ (i + 1) / 2 = i / 2 | A User Theorem |
| div2-odd-01 | ⊦ i < 0 → (1 - i * 2) / 2 = ~ i | A User Theorem |
| div2-one | ⊦ 1 / 2 = 0 | A User Theorem |
| div2-zero | ⊦ i / 2 = 0 ↔ i = 0 ∨ i = 1 ∨ i = ~ 1 | A User Theorem |
| div2one | ⊦ i % 2 = 1 ∧ 0 < i → i / 2 * 2 + 1 = i | A User Theorem |
| div2one-01 | ⊦ i % 2 = 1 → (1 + i / 2) * 2 = i + 1 | A User Theorem |
| div2zero | ⊦ i % 2 ≠ 1 ∧ 0 < i → i / 2 * 2 = i | A User Theorem |
| div53 | ⊦ (1 + 1 + 1 + 1 + 1) / (1 + 1 + 1) = 1 | A User Theorem |
| diveq-neg | i0 * j + j0 < 0, i0 < 0, j0 ≤ 0, abs(j0) < j ⊦ (i0 * j + j0) / j = i0 | A User Theorem |
| diveq-pos | 0 ≤ i0 * j + j0, 0 ≤ j0, j0 < j ⊦ (i0 * j + j0) / j = i0 | A User Theorem |
| divmod-rew | j ≠ 0 ⊦ i / j * j + i % j = i | A User Theorem |
| divmult | j ≠ 0 ⊦ i % j = 0 → i / j * j = i | A User Theorem |
| estimate-01 | 0 < i, 0 < i0, 0 < j, j < i, j0 < i0 ⊦ j0 < (i * i0) / j | A User Theorem |
| even-add | ⊦ (i + j) % 2 = 0 ↔ i % 2 = 0 ∧ j % 2 = 0 ∨ i % 2 ≠ 0 ∧ j % 2 ≠ 0 | A User Theorem |
| even-mult | ⊦ (i * j) % 2 = 0 ↔ i % 2 = 0 ∨ j % 2 = 0 | A User Theorem |
| even-not | ⊦ (2 * i + 1) % 2 ≠ 0 | A User Theorem |
| even-not-ex | ⊦ i % 2 ≠ 0 ↔ (∃ i0. i = 2 * i0 + 1) | A User Theorem |
| even-or-succ-even | 0 ≤ i ⊦ i % 2 = 0 ∨ (i + 1) % 2 = 0 | A User Theorem |
| exeven | i % 2 = 0 ⊦ ∃ j. i = 2 * j | A User Theorem |
| exodd | i % 2 = 1, 0 ≤ i ⊦ ∃ j. 0 ≤ j ∧ i = 2 * j + 1 | A User Theorem |
| is-div | ⊦ 0 ≤ i0 ∧ 0 ≤ i ∧ 0 < j ∧ i0 * j ≤ i ∧ i < (i0 + 1) * j → i0 = i / j | A User Theorem |
| le-abs-numerator | j ≠ 0 ⊦ ~ abs(i) ≤ i / j ∧ i / j ≤ abs(i) | A User Theorem |
| le-norest | ⊦ i % j = 0 ∧ i0 % j = 0 ∧ 0 ≤ i ∧ 0 < j ∧ 0 ≤ i0 → (i / j ≤ i0 / j ↔ i ≤ i0) | A User Theorem |
| leone-two | ⊦ i / 2 ≤ 1 ↔ i ≤ 1 + 1 + 1 | A User Theorem |
| less-mult-div | ⊦ 0 < i ∧ 0 < i1 ∧ 0 < j ∧ i1 < j → i * i1 / j < i | A User Theorem |
| less-mult-div-01 | ⊦ 0 < i ∧ 0 < j ∧ 0 < j1 ∧ i1 < j → (i * i1) / j < i | A User Theorem |
| less-mult-div-02 | ⊦ 0 < i ∧ 0 < j ∧ i1 < j → (i * i1) / j < i | A User Theorem |
| letwo | ⊦ 1 < i → ¬ i ≤ i / 2 | A User Theorem |
| letwozero | ⊦ i < 0 → (0 ≤ i / 2 ↔ i = ~1) | A User Theorem |
| ls | 0 ≤ i0, 0 < i, 0 < j, i0 / i < i0 / j ⊦ j < i | A User Theorem |
| ls-01 | i0 ≠ 0, j0 ≠ 0, 0 ≤ i, 0 ≤ i0, i ≤ j, i0 ≤ j0 ⊦ i / j0 ≤ j / i0 | A User Theorem |
| ls-02 | 0 < i0, i / i0 < j / i0 ⊦ i < j | A User Theorem |
| ls-03 | 0 < j0, 0 ≤ i, i ≤ j ⊦ i / j0 ≤ j / j0 | A User Theorem |
| ls-even | ⊦ i % 2 = 0 ∧ j % 2 = 0 ∧ 0 ≤ i ∧ 0 ≤ j → (i / 2 < j / 2 ↔ i < j) | A User Theorem |
| ls-even-01 | ⊦ i % 2 = 0 ∧ j % 2 = 0 → (i / 2 < j / 2 ↔ i < j) | A User Theorem |
| ls-same-pos | ⊦ 0 ≤ i ∧ 0 < j → i / j * j ≤ i | A User Theorem |
| ls-same-pos-01 | ⊦ 0 ≤ i ∧ 0 < j → i < (i / j + 1) * j | A User Theorem |
| ls-same-pos-02 | ⊦ 0 ≤ i ∧ 0 < j → ¬ i < i / j * j | A User Theorem |
| ls-succ | ⊦ 0 < i ∧ 0 < j → i / (j + 1) ≤ i / j | A User Theorem |
| lsf | ⊦ i / i0 < j / i0 ∧ 0 < i0 → i < j | A User Theorem |
| lsf-01 | ⊦ i0 / i < i0 / j ∧ 0 ≤ i0 ∧ 0 < i ∧ 0 < j → j < i | A User Theorem |
| lsf-02 | ⊦ i / j < i / i0 ∧ 0 < j ∧ 0 < i0 ∧ i < 0 → j < i0 | A User Theorem |
| lsfc | 0 ≤ i0, 0 < i, 0 < j ⊦ i0 / i < i0 / j → j < i | A User Theorem |
| lsfc-01 | 0 < i0 ⊦ i / i0 < j / i0 → i < j | A User Theorem |
| lsfc-02 | 0 < i0 ⊦ i / i0 + j / i0 < 0 → i + j < 0 | A User Theorem |
| lstwozero | ⊦ i < 0 → ¬ 0 < i / 2 | A User Theorem |
| minus-add | j0 ≠ 0 ⊦ (i - j) / j0 + (j - i) / j0 = 0 | A User Theorem |
| mod-abs | ⊦ j ≠ 0 → i % abs(j) = i % j | A User Theorem |
| mod-abs-intro | ⊦ j ≠ 0 → i % j = i % abs(j) | A User Theorem |
| mod-add | ⊦ 0 < i ∧ 0 ≤ j → (i + j) % i = j % i | A User Theorem |
| mod-add-01 | ⊦ 0 < i ∧ j < 0 ∧ i ≤ abs(j) → (i + j) % i = j % i | A User Theorem |
| mod-add-both-zero | ⊦ i % j = 0 ∧ i0 % j = 0 ∧ 0 ≠ j → (i + i0) % j = 0 | A User Theorem |
| mod-add-neg | ⊦ i0 % j = 0 ∧ i < 0 ∧ i0 < 0 ∧ 0 < j → (i + i0) % j = i % j | A User Theorem |
| mod-add-pos | ⊦ i0 % j = 0 ∧ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → (i + i0) % j = i % j | A User Theorem |
| mod-add-zero | ⊦ 0 ≤ i ∧ 0 < j ∧ 0 ≤ i1 ∧ i % j + j * i1 = 0 → i1 = 0 | A User Theorem |
| mod-add1-negneg | ⊦ i % j = 0 ∧ i < 0 ∧ i0 < 0 ∧ 0 < j → (i + i0) % j = i0 % j | A User Theorem |
| mod-add1-negpos-neg | ⊦ i % j = 0 ∧ i + i0 < 0 ∧ i < 0 ∧ 0 ≤ i0 ∧ i0 % j ≠ 0 ∧ 0 < j → (i + i0) % j = i0 % j - j | A User Theorem |
| mod-add1-negpos-pos | ⊦ i % j = 0 ∧ 0 ≤ i + i0 ∧ i < 0 ∧ 0 ≤ i0 ∧ 0 < j → (i + i0) % j = i0 % j | A User Theorem |
| mod-add1-posneg-neg | ⊦ i % j = 0 ∧ i + i0 < 0 ∧ 0 ≤ i ∧ i0 < 0 ∧ 0 < j → (i + i0) % j = i0 % j | A User Theorem |
| mod-add1-posneg-pos | ⊦ i % j = 0 ∧ 0 ≤ i + i0 ∧ 0 ≤ i ∧ i0 < 0 ∧ i0 % j ≠ 0 ∧ 0 < j → (i + i0) % j = i0 % j + j | A User Theorem |
| mod-add1-pospos | ⊦ i % j = 0 ∧ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → (i + i0) % j = i0 % j | A User Theorem |
| mod-by6 | ⊦ 0 ≤ i → (i * (i + 1) * (2 * i + 1)) % 6 = 0 | A User Theorem |
| mod-div-ls | 0 ≤ i0, i0 < i1, 0 < j, 0 ≤ i ⊦ (i0 + i1 * i % j) / j < i1 | A User Theorem |
| mod-div-zero | ⊦ j ≠ 0 → (i % j) / j = 0 | A User Theorem |
| mod-four | ⊦ 1 % (1 + 1 + 1 + 1) = 1 | A User Theorem |
| mod-gez | ⊦ j ≠ 0 → (0 ≤ i % j ↔ 0 ≤ i ∨ i % j = 0) | A User Theorem |
| mod-grz | ⊦ 0 < j ∧ i < 0 → ¬ 0 < i % j | A User Theorem |
| mod-grz-01 | ⊦ i < 0 ∧ j ≠ 0 → ¬ 0 < i % j | A User Theorem |
| mod-grz-02 | ⊦ i < 0 ∧ j < 0 → ¬ 0 < i % j | A User Theorem |
| mod-le | ⊦ j ≤ j0 + 1 ∧ 0 ≤ i ∧ 0 < j → i % j ≤ j0 | A User Theorem |
| mod-le-01 | ⊦ j ≤ j0 ∧ 0 ≤ i ∧ 0 < j → i % j ≤ j0 | A User Theorem |
| mod-le-num | j < j0, 0 < j ⊦ i % (* j) ≤ (* j0) | A User Theorem |
| mod-les | ⊦ 0 < j → ¬ j ≤ i % j | A User Theorem |
| mod-less | ⊦ j > 0 → i % j < j | A User Theorem |
| mod-less-01 | ⊦ 0 < j → i % j < j | A User Theorem |
| mod-lezero | ⊦ 0 < j → ¬ j + i % j ≤ 0 | A User Theorem |
| mod-ls-same | ⊦ 0 < j ∧ 0 ≤ i → i % j < j | A User Theorem |
| mod-ls-same-01 | j ≠ 0 ⊦ i % j < i ↔ 0 < i ∧ (abs(j) = 1 ∨ abs(j) ≤ i) | A User Theorem |
| mod-ls-same-02 | j ≠ 0 ⊦ i < i % j ↔ i < 0 ∧ (abs(j) = 1 ∨ abs(j) ≤ abs(i)) | A User Theorem |
| mod-ls-zero | 0 < j ⊦ i % (* j) < 0 ↔ i < 0 ∧ i % j ≠ 0 | A User Theorem |
| mod-lsz | ⊦ 0 < j → ¬ j + i % j < 0 | A User Theorem |
| mod-lsz-01 | ⊦ j ≠ 0 → (i % j < 0 ↔ i < 0 ∧ i % j ≠ 0) | A User Theorem |
| mod-mod-less | ⊦ j % i = 0 ∧ 0 < i ∧ 0 < j ∧ 0 ≤ i1 ∧ i < j → (i1 % j) % i = i1 % i | A User Theorem |
| mod-mult | 0 ≤ i, 0 < j, 0 < i0 ⊦ (i0 * i) % (i0 * j) = i % j * i0 | A User Theorem |
| mod-mult-01 | 0 ≠ j, 0 < i0 ⊦ (i0 * i) % (i0 * j) = i % j * i0 | A User Theorem |
| mod-mult-02 | 0 ≠ j, i0 ≠ 0 ⊦ (i0 * i) % (i0 * j) = i % j * i0 | A User Theorem |
| mod-mult-03 | 0 ≠ j ⊦ (2 * i) % (2 * j) = i % j * 2 | A User Theorem |
| mod-mult-04 | j ≠ 0 ⊦ (i * j) % j = 0 | A User Theorem |
| mod-mult-neg | ⊦ 0 < j ∧ i ≤ 0 ∧ i0 ≤ 0 ∧ abs(i0) < j → (j * i + i0) % j = i0 | A User Theorem |
| mod-mult-neg-01 | ⊦ 0 < j ∧ i ≤ 0 ∧ 0 ≤ i0 ∧ i0 < j → (j * i - i0) % j = ~ i0 | A User Theorem |
| mod-mult-neg-02 | ⊦ 0 < j ∧ i ≤ 0 ∧ i0 ≤ 0 → (j * i + i0) % j = i0 % j | A User Theorem |
| mod-mult-neg-03 | ⊦ 0 < j ∧ i ≤ 0 ∧ i0 ≤ 0 → (i * j + i0) % j = i0 % j | A User Theorem |
| mod-mult-pos | ⊦ 0 < j ∧ 0 ≤ i ∧ 0 ≤ i0 ∧ i0 < j → (j * i + i0) % j = i0 | A User Theorem |
| mod-mult-pos-01 | ⊦ 0 < j ∧ 0 ≤ i ∧ 0 ≤ i0 → (j * i + i0) % j = i0 % j | A User Theorem |
| mod-mult-pos-02 | ⊦ 0 < j ∧ 0 ≤ i ∧ 0 ≤ i0 → (i * j + i0) % j = i0 % j | A User Theorem |
| mod-neg | j ≠ 0 ⊦ i % ~ j = i % j | A User Theorem |
| mod-neg-01 | j ≠ 0 ⊦ ~ i % j = ~(i % j) | A User Theorem |
| mod-neq | j ≠ 0 ⊦ i % j ≠ j | A User Theorem |
| mod-neq-01 | j ≠ 0 ⊦ i % j + j ≠ 0 | A User Theorem |
| mod-neq-02 | ⊦ j ≤ j0 ∧ 0 < j → i % j ≠ j0 | A User Theorem |
| mod-next-square | ⊦ ((i * i) * (i + 1) * (i + 1)) % 4 = 0 | A User Theorem |
| mod-ngez | ⊦ 0 < j ∧ i < 0 → (0 ≤ i % j ↔ i % j = 0) | A User Theorem |
| mod-ngez-01 | ⊦ i < 0 ∧ j < 0 → (0 ≤ i % j ↔ i % j = 0) | A User Theorem |
| mod-ngr | ⊦ i < 0 ∧ 0 < j → (0 ≤ i % j ↔ i % j = 0) | A User Theorem |
| mod-nle | ⊦ 0 < i ∧ 0 ≤ j → (j ≤ j % i ↔ j < i) | A User Theorem |
| mod-nle-01 | ⊦ 0 < j ∧ 0 ≤ i ∧ j ≤ i0 → ¬ i0 ≤ i % j | A User Theorem |
| mod-nle-02 | ⊦ j0 ≤ ~ j ∧ 0 < j → ¬ i % j ≤ j0 | A User Theorem |
| mod-nls | j ≠ 0 ⊦ j0 = 1 + ~ j ∧ j0 < 0 → ¬ i % j < j0 | A User Theorem |
| mod-nls-01 | ⊦ j ≤ i0 ∧ 0 < j → ¬ i0 < i % j | A User Theorem |
| mod-nls-02 | ⊦ i0 ≤ i ∧ i0 < 0 ∧ j ≠ 0 → ¬ i % j < i0 | A User Theorem |
| mod-nls-03 | ⊦ i ≤ i0 ∧ 0 ≤ i0 ∧ j ≠ 0 → ¬ i0 < i % j | A User Theorem |
| mod-nls-04 | ⊦ i0 - 1 ≤ ~ abs(j) ∧ j ≠ 0 → ¬ i % j < i0 | A User Theorem |
| mod-nls-05 | ⊦ j ≤ i0 + 1 ∧ 0 < j → ¬ i0 < i % j | A User Theorem |
| mod-nls-06 | j ≠ 0 ⊦ abs(j) ≤ i0 + 1 → ¬ i0 < i % j | A User Theorem |
| mod-not-less | ⊦ j < 0 ∧ i < 0 → ¬ i % j ≤ j | A User Theorem |
| mod-one | ⊦ i % 1 = 0 | A User Theorem |
| mod-one-01 | ⊦ 1 % 2 = 1 | A User Theorem |
| mod-pos-not-neg | ⊦ 0 < i1 ∧ 0 < i % i1 → ¬ i < 0 | A User Theorem |
| mod-pred | ⊦ (i - 1) % j + 1 ≠ j ∧ 0 < i ∧ 0 < j → i % j = (i - 1) % j + 1 | A User Theorem |
| mod-pred-01 | ⊦ (i - 1) % j + 1 = j ∧ 0 < i ∧ 0 < j → i % j = 0 | A User Theorem |
| mod-pred-02 | ⊦ i % j ≠ 0 ∧ 0 < i ∧ 0 < j → (i - 1) % j = i % j - 1 | A User Theorem |
| mod-pred-03 | ⊦ (i + 1) % j ≠ 0 ∧ 0 ≤ i ∧ 0 < j → i % j = (i + 1) % j - 1 | A User Theorem |
| mod-pred-04 | ⊦ (i + 1) % j = 0 ∧ 0 ≤ i ∧ 0 < j → i % j = j - 1 | A User Theorem |
| mod-pred-neg | ⊦ i % j - 1 ≠ ~ j ∧ i < 0 ∧ 0 < j → i % j = (i - 1) % j + 1 | A User Theorem |
| mod-pred-neg-01 | ⊦ (i - 1) % j ≠ 0 ∧ i < 0 ∧ 0 < j → i % j = (i - 1) % j + 1 | A User Theorem |
| mod-rec | 0 < j, j ≤ i ⊦ i % j = (i - j) % j | A User Theorem |
| mod-rec-01 | i ≤ j, j < 0 ⊦ i % j = (i - j) % j | A User Theorem |
| mod-rew | j ≠ 0 ⊦ i % j = i - i / j * j | A User Theorem |
| mod-same | i ≠ 0 ⊦ i % i = 0 | A User Theorem |
| mod-shift | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → (i * i0 % j) % j = (i * i0) % j | A User Theorem |
| mod-sub | ⊦ 0 < i ∧ j < 0 → (i - j) % i = ~(j % i) | A User Theorem |
| mod-sub-01 | ⊦ 0 < i ∧ 0 ≤ j ∧ i ≤ j → (i - j) % i = ~(j % i) | A User Theorem |
| mod-sub-02 | ⊦ 0 ≤ i ∧ j < i ∧ 0 < j ∧ 0 ≤ i0 ∧ i0 * j ≤ i ∧ i < (i0 + 1) * j → i % j = i - i0 * j | A User Theorem |
| mod-succ | ⊦ 1 < i → (i + 1) % i = 1 | A User Theorem |
| mod-succ-01 | ⊦ i % j + 1 ≠ j ∧ 0 ≤ i ∧ 0 < j → (i + 1) % j = i % j + 1 | A User Theorem |
| mod-succ-02 | ⊦ i % j + 1 = j ∧ 0 ≤ i ∧ 0 < j → (i + 1) % j = 0 | A User Theorem |
| mod-three | ⊦ (1 + 1 + 1) % 2 = 1 | A User Theorem |
| mod-two | ⊦ i % 2 ≠ 1 ∧ 0 < i → i % 2 = 0 | A User Theorem |
| mod-two-01 | ⊦ i % 2 + 1 ≠ 0 ∧ i < 0 → i % 2 = 0 | A User Theorem |
| mod-two-02 | ⊦ (i * 2) % 2 = 0 | A User Theorem |
| mod-two-03 | ⊦ 0 < i → (i * 2 - 1) % 2 = 1 | A User Theorem |
| mod-two-04 | ⊦ 0 ≤ i → (i * 2 + 1) % 2 = 1 | A User Theorem |
| mod-two-05 | ⊦ i % 2 ≠ 1 ∧ 1 < i → i % 2 = 0 | A User Theorem |
| mod-two-06 | ⊦ 0 < i → (i % 2 ≠ 1 ↔ i % 2 = 0) | A User Theorem |
| mod-two-pred | ⊦ 0 < i → (2 * i - 1) % 2 = 1 | A User Theorem |
| mod-two-pred-01 | ⊦ i < 0 → (2 * i - 1) % 2 = ~1 | A User Theorem |
| mod-two-pred-02 | ⊦ i < 0 → (1 - 2 * i) % 2 = 1 | A User Theorem |
| mod-twoeven | i % 2 = 0, j ≠ 0 ⊦ i % (2 * j) = (i / 2) % j * 2 | A User Theorem |
| mod-twoodd | 0 ≤ i, 0 < j ⊦ (2 * i + 1) % (2 * j) = i % j * 2 + 1 | A User Theorem |
| mod-twoodd-01 | i % 2 = 1, 0 ≤ i, 0 < j ⊦ i % (2 * j) = (i / 2) % j * 2 + 1 | A User Theorem |
| mod-twoodd-02 | ⊦ j % (2 * i) = 1 ∧ 0 < i ∧ 0 ≤ j → j % 2 = 1 | A User Theorem |
| mod-twoodd-03 | i < 0, 0 < j ⊦ (2 * i + 1) % (2 * j) = (i + 1) % j * 2 - 1 | A User Theorem |
| mod-zero | ⊦ 0 < j ∧ 0 ≤ i → 0 ≤ i % j | A User Theorem |
| mod-zero-01 | ⊦ 0 < j ∧ 0 ≤ i → ¬ i % j < 0 | A User Theorem |
| mod-zero-02 | ⊦ 0 ≤ i ∧ 0 < j → (i % j ≤ 0 ↔ i % j = 0) | A User Theorem |
| mod-zero-03 | 0 < j, 0 ≤ i, i < j ⊦ i % j = i | A User Theorem |
| mod-zero-04 | j ≠ 0 ⊦ 0 % j = 0 | A User Theorem |
| mod-zero-05 | ⊦ abs(i) < j → i % j = i | A User Theorem |
| mod-zero-06 | ⊦ 0 ≤ i ∧ j ≠ 0 → ¬ i % j < 0 | A User Theorem |
| mod-zero-07 | 0 < j ⊦ 0 ≤ i ∧ i < j → i % (* j) = i | A User Theorem |
| mod-zero-08 | 0 < j ⊦ 0 < i ∧ i < j → i % (* j) = i | A User Theorem |
| mod-zero-09 | ⊦ 0 < i ∧ i < j → i % j = i | A User Theorem |
| mod-zero-ls | ⊦ 0 < i ∧ 0 < j → ¬ i % j < 0 | A User Theorem |
| mod-zero-num | i0 % j = 0, j ≠ 0 ⊦ (i * (* i0)) % (* j) = 0 | A User Theorem |
| mod-zero-one | 0 ≤ i, 0 ≤ i0, 0 < j ⊦ (i % j + i0 % j) / j = 1 ∨ (i % j + i0 % j) / j = 0 | A User Theorem |
| mod2-add-neg | ⊦ j % 2 = 0 ∧ i ≤ 0 ∧ abs(i) ≤ j → (i + j) % 2 = ~ i % 2 | A User Theorem |
| mod2-neg-odd | ⊦ j < 0 → (j % 2 ≠ ~1 ↔ j % 2 = 0) | A User Theorem |
| mod256 | ⊦ ¬ 255 < i % 256 | A User Theorem |
| mod53 | ⊦ (1 + 1 + 1 + 1 + 1) % (1 + 1 + 1) = 1 + 1 | A User Theorem |
| mod62 | ⊦ (1 + 1 + 1 + 1 + 1 + 1) % 2 = 0 | A User Theorem |
| modby6-help | ⊦ (i + 1) * (2 + i) * (2 * (i + 1) + 1) = 6 * (i + 1) * (i + 1) + i * (i + 1) * (2 * i + 1) | A User Theorem |
| modeq-neg | i0 * j + j0 < 0, 0 < j, j0 < 0 ⊦ (i0 * j + j0) % j = j0 % j | A User Theorem |
| modeq-neg-02 | i0 * j + j0 < 0, 0 < j, 0 ≤ j0, j0 % j ≠ 0 ⊦ (i0 * j + j0) % j = j0 % j - j | A User Theorem |
| modeq-pos | 0 ≤ i0 * j + j0, 0 ≤ j0, j0 < j ⊦ (i0 * j + j0) % j = j0 | A User Theorem |
| modeq-pos-01 | 0 ≤ i0 * j + j0, j0 < 0, abs(j0) < j ⊦ (i0 * j + j0) % j = j + j0 | A User Theorem |
| modeq-pos-02 | 0 ≤ i0 * j + j0, 0 < j, 0 ≤ j0 ⊦ (i0 * j + j0) % j = j0 % j | A User Theorem |
| modeq-pos-03 | 0 ≤ i0 * j + j0, 0 < j, j0 < 0, j0 % j ≠ 0 ⊦ (i0 * j + j0) % j = j0 % j + j | A User Theorem |
| modeq-pos-04 | 0 ≤ i0 * j - j0, 0 < j, 0 < j0, j0 % j ≠ 0 ⊦ (i0 * j - j0) % j = j - j0 % j | A User Theorem |
| modeven-neg | ⊦ i < 0 ∧ i % 2 = 0 → (i + 1) % 2 = ~1 | A User Theorem |
| modeven-neg-01 | ⊦ i < 0 → ((i + 1) % 2 ≠ 0 ↔ (i + 1) % 2 = ~1 ∧ i % 2 = 0) | A User Theorem |
| modeven-pos | ⊦ 0 < i ∧ i % 2 = 0 → (i + 1) % 2 = 1 | A User Theorem |
| modex | j ≠ 0 ⊦ i % j = 0 ↔ (∃ j0. i = j0 * j) | A User Theorem |
| modex-odd | ⊦ i % 2 = 1 ↔ (∃ j. i = 2 * j + 1 ∧ 0 ≤ j) | A User Theorem |
| modex-odd-neg | ⊦ i % 2 = ~1 ↔ (∃ j. i = 2 * j - 1 ∧ j ≤ 0) | A User Theorem |
| modex-odd-neg-01 | ⊦ i % 2 = ~1 ↔ (∃ j. i = 2 * j + 1 ∧ j < 0) | A User Theorem |
| modmod | j ≠ 0 ⊦ (i % j) % j = i % j | A User Theorem |
| modmod-add | 0 < j ⊦ 0 ≤ i ∧ 0 ≤ i0 → (i % j + i0) % j = (i + i0) % j | A User Theorem |
| modmod-add-01 | 0 ≠ j ⊦ 0 ≤ i ∧ 0 ≤ i0 → (i % j + i0) % j = (i + i0) % j | A User Theorem |
| modmod-add-02 | 0 ≠ j ⊦ i ≤ 0 ∧ i0 ≤ 0 → (i % j + i0) % j = (i + i0) % j | A User Theorem |
| modmod-add-03 | j ≠ 0 ⊦ i < 0 ∧ i0 < 0 → (i % j + i0 % j) % j = (i + i0) % j | A User Theorem |
| modmod-add-04 | ⊦ 0 < j ∧ 0 ≤ i ∧ 0 ≤ i0 → (i % j + i0 % j) % j = (i + i0) % j | A User Theorem |
| modmod-add-case | 0 < j ⊦ (i + i0 % j) % j = (i + i0) % j ∨ (i + i0 % j) % j = (i + i0) % j + j ∨ (i + i0 % j) % j = (i + i0) % j - j | A User Theorem |
| modmod-add-if | 0 < j ⊦ (i + i0 % j) % j = (0 ≤ i ⊃ (0 ≤ i0 ⊃ (i + i0) % j;(0 ≤ i + i0 ⊃ (i + i0) % j;(i + i0 % j < 0 ⊃ (i + i0) % j;((i + i0 % j) % j ≠ 0 ⊃ (i + i0) % j + j;0)))) ;(i0 < 0 ⊃ (i + i0) % j;(i + i0 < 0 ⊃ (i + i0) % j;(0 ≤ i + i0 % j ⊃ (i + i0) % j;((i + i0 % j) % j ≠ 0 ⊃ (i + i0) % j - j;0)))) ) | A User Theorem |
| modmod-add-if3 | 0 < j ⊦ (i + i0 % j) % j = (0 ≤ i + i0 % j ∧ i + i0 < 0 ∧ 0 ≤ i ∧ i0 < 0 ∧ (i + i0 % j) % j ≠ 0 ⊃ (i + i0) % j + j ;(i + i0 % j < 0 ∧ 0 ≤ i + i0 ∧ i < 0 ∧ 0 ≤ i0 ∧ (i + i0 % j) % j ≠ 0 ⊃ (i + i0) % j - j;(i + i0) % j) ) | A User Theorem |
| modmod-add-law | 0 ≠ j ⊦ (i % j + i0 % j) % j = (i + i0) % j ∨ (i % j + i0 % j) % j = (i + i0) % j + j ∨ (i % j + i0 % j) % j = (i + i0) % j - j | A User Theorem |
| modmod-add-law-pos | 0 < j ⊦ (i % j + i0 % j) % j = (i + i0) % j ∨ (i % j + i0 % j) % j = (i + i0) % j + j ∨ (i % j + i0 % j) % j = (i + i0) % j - j | A User Theorem |
| modmod-add-zero | 0 < j ⊦ (i + i0 % j) % j = 0 → (i + i0) % j = 0 | A User Theorem |
| modmod-add2-negpos-neg | ⊦ i + i0 < 0 ∧ i < 0 ∧ 0 ≤ i0 ∧ 0 < j → (i + i0 % j) % j = (i + i0) % j | A User Theorem |
| modmod-add2-negpos-pos | ⊦ 0 ≤ i + i0 % j ∧ i < 0 ∧ 0 ≤ i0 ∧ 0 < j → (i + i0 % j) % j = (i + i0) % j | A User Theorem |
| modmod-add2-negpos-pos-01 | ⊦ i + i0 % j < 0 ∧ 0 ≤ i + i0 ∧ i < 0 ∧ 0 ≤ i0 ∧ (i + i0 % j) % j ≠ 0 ∧ 0 < j → (i + i0 % j) % j = (i + i0) % j - j | A User Theorem |
| modmod-add2-negpos-pos-02 | ⊦ i + i0 % j < 0 ∧ 0 ≤ i + i0 ∧ i < 0 ∧ 0 ≤ i0 ∧ (i + i0 % j) % j = 0 ∧ 0 < j → (i + i0 % j) % j = (i + i0) % j | A User Theorem |
| modmod-add2-posneg-neg | ⊦ i + i0 % j < 0 ∧ 0 ≤ i ∧ i0 < 0 ∧ 0 < j → (i + i0 % j) % j = (i + i0) % j | A User Theorem |
| modmod-add2-posneg-neg-01 | ⊦ 0 ≤ i + i0 % j ∧ i + i0 < 0 ∧ 0 ≤ i ∧ i0 < 0 ∧ (i + i0 % j) % j ≠ 0 ∧ 0 < j → (i + i0 % j) % j = (i + i0) % j + j | A User Theorem |
| modmod-add2-posneg-neg-02 | ⊦ 0 ≤ i + i0 % j ∧ i + i0 < 0 ∧ 0 ≤ i ∧ i0 < 0 ∧ (i + i0 % j) % j = 0 ∧ 0 < j → (i + i0 % j) % j = (i + i0) % j | A User Theorem |
| modmod-add2-posneg-pos | ⊦ 0 ≤ i + i0 ∧ 0 ≤ i ∧ i0 < 0 ∧ 0 < j → (i + i0 % j) % j = (i + i0) % j | A User Theorem |
| modmod-law-mult | 0 ≠ j ⊦ (i * i0) % j = (i % j * i0 % j) % j | A User Theorem |
| modmod-ma | 0 < j ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 ≤ j0 → (i % j * i0 % j + j0) % j = (i * i0 + j0) % j | A User Theorem |
| modmod-ma-01 | 0 < j ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 ≤ j0 → (i % j * i0 + j0) % j = (i * i0 + j0) % j | A User Theorem |
| modmod-ma-negpos-neg | ⊦ j0 + i0 * i < 0 ∧ j0 < 0 ∧ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → (j0 + i0 * i % j) % j = (j0 + i0 * i) % j | A User Theorem |
| modmod-mult | 0 < j ⊦ 0 ≤ i ∧ 0 ≤ i0 → (i % j * i0 % j) % j = (i * i0) % j | A User Theorem |
| modmod-mult-01 | 0 ≠ j ⊦ (i % j * i0 % j) % j = (i * i0) % j | A User Theorem |
| modmod-mult-02 | 0 < j ⊦ (i % j * i0 % j) % j = (i * i0) % j | A User Theorem |
| modmod-mult-03 | j ≠ 0 ⊦ 0 < j0 → (i % (j * j0)) % j = i % j | A User Theorem |
| modmod-mult-04 | ⊦ 0 < j ∧ 0 ≤ i ∧ 0 < j0 → (i % (j * j0)) % j = i % j | A User Theorem |
| modmod-mult-05 | ⊦ j ≠ 0 ∧ j0 ≠ 0 → (i % (j * j0)) % j = i % j | A User Theorem |
| modmod-mult-06 | 0 < j ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 ≤ j0 → (i % j * i0) % j = (i * i0) % j | A User Theorem |
| modmod-mult-07 | 0 < j ⊦ (i % j * i0) % j = (i * i0) % j | A User Theorem |
| modmod-mult-08 | 0 < j ⊦ 0 ≤ i ∧ 0 ≤ i0 → (i % j * i0) % j = (i * i0) % j | A User Theorem |
| modmod-mult-09 | j ≠ 0 ⊦ (i % j * i0) % j = (i * i0) % j | A User Theorem |
| modmod-pos | ⊦ 0 ≤ i ∧ 0 < j ∧ 0 < j0 → i % (j * j0) = i % j + (i / j) % j0 * j | A User Theorem |
| modnum-neg | j ≠ 0 ⊦ i < 0 → (* i) % j = ~(~ i % j) | A User Theorem |
| modnum-neg-01 | ⊦ j < 0 → i % (* j) = i % ~ j | A User Theorem |
| mult | ⊦ 0 ≤ i0 ∧ i0 < j ∧ 0 ≤ i → (i * j + i0) / j = i | A User Theorem |
| mult-01 | ⊦ 0 ≤ i0 ∧ i0 < abs(j) ∧ j < 0 ∧ 0 ≤ i → (i * abs(j) + i0) / j = ~ i | A User Theorem |
| mult-02 | ⊦ 0 ≤ i0 ∧ i0 < j ∧ 0 ≤ i ∧ 0 < j0 → (i * j + i0) / (j0 * j) = i / j0 | A User Theorem |
| mult-03 | ⊦ 0 < i0 ∧ i0 < j ∧ 0 < i ∧ 0 < j0 → (i * j - i0) / (j0 * j) = (i - 1) / j0 | A User Theorem |
| mult-04 | ⊦ 0 < i0 ∧ i0 < j ∧ 0 < i ∧ 0 < j0 → (j * i - i0) / (j * j0) = (i - 1) / j0 | A User Theorem |
| mult-05 | ⊦ 0 < i0 ∧ i0 < j ∧ 0 < i → (j * i - i0) / j = i - 1 | A User Theorem |
| mult-div-switch | ⊦ j ≠ 0 ∧ i % j = 0 → i / j * j = i | A User Theorem |
| mult-ls | ⊦ 0 < j ∧ i / j < i0 → i < i0 * j | A User Theorem |
| mult-ls-01 | ⊦ 0 < j ∧ i0 < i / j → i0 * j < i | A User Theorem |
| mult-split-mod | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → i / j * i0 + (i0 * i % j) / j = (i0 * i) / j | A User Theorem |
| mult-split-mod-02 | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 ≤ i1 ∧ 0 < j → (i + i0 * i1 / j) + (i0 * i1 % j) / j = i + (i0 * i1) / j | A User Theorem |
| neg | j ≠ 0 ⊦ i / ~ j = ~(i / j) | A User Theorem |
| neg-01 | j ≠ 0 ⊦ ~ i / j = ~(i / j) | A User Theorem |
| neqf | ⊦ i / j ≠ i / i0 → j ≠ i0 | A User Theorem |
| nls-mult-div | ⊦ 0 ≤ i ∧ 0 < j ∧ i1 < j → ¬ i < (i * i1) / j | A User Theorem |
| num-ls | ⊦ 0 < j ∧ 0 ≤ i → (i / (* j) < j0 ↔ i < j * j0) | A User Theorem |
| num-neg | j ≠ 0 ⊦ i < 0 → (* i) / j = ~(~ i / j) | A User Theorem |
| num-neg-01 | ⊦ j < 0 → i / (* j) = ~(i / ~ j) | A User Theorem |
| nummult-eq | ⊦ j ≠ 0 → ((* i) * i0 = (* j) ↔ j % i = 0 ∧ i0 = j / i ∧ i ≠ 0) | A User Theorem |
| nummult-eq-01 | j ≠ 0, j0 % j = 0 ⊦ i * (* j) = i0 * (* j0) ↔ i = i0 * j0 / j | A User Theorem |
| nummult-le | ⊦ 0 < i ∧ 0 ≤ j → ((* i) * i0 ≤ (* j) ↔ i0 ≤ j / i) | A User Theorem |
| nummult-le-01 | ⊦ 0 < i ∧ j < 0 → ((* i) * i0 ≤ (* j) ↔ i0 ≤ (j + 1 - i) / i) | A User Theorem |
| nummult-le-01-01 | 0 < i, j < 0 ⊦ (* i) * i0 ≤ (* j) ↔ i0 ≤ (j + 1 - i) / i | A User Theorem |
| nummult-le-02 | ⊦ 0 < i ∧ 0 ≤ j → ((* j) ≤ (* i) * i0 ↔ (i + j - 1) / i ≤ i0) | A User Theorem |
| nummult-le-02-01 | 0 < i, 0 ≤ j ⊦ (* j) ≤ (* i) * i0 ↔ (i + j - 1) / i ≤ i0 | A User Theorem |
| nummult-le-03 | ⊦ 0 < i ∧ j < 0 → ((* j) ≤ (* i) * i0 ↔ j / i ≤ i0) | A User Theorem |
| nummult-le-03-01 | 0 < i, j < 0 ⊦ (* j) ≤ (* i) * i0 ↔ j / i ≤ i0 | A User Theorem |
| nummult-le-04 | 0 < i, 0 ≤ j ⊦ (* i) * i0 ≤ (* j) ↔ i0 ≤ j / i | A User Theorem |
| nummult-ls | ⊦ 0 < i ∧ 0 ≤ j → ((* i) * i0 < (* j) ↔ i0 < (i + j - 1) / i) | A User Theorem |
| nummult-ls-01 | ⊦ 0 < i ∧ j < 0 → ((* i) * i0 < (* j) ↔ i0 < j / i) | A User Theorem |
| nummult-ls-01-01 | 0 < i, j < 0 ⊦ (* i) * i0 < (* j) ↔ i0 < j / i | A User Theorem |
| nummult-ls-02 | ⊦ 0 < i ∧ 0 ≤ j → ((* j) < (* i) * i0 ↔ j / i < i0) | A User Theorem |
| nummult-ls-02-01 | 0 < i, 0 ≤ j ⊦ (* j) < (* i) * i0 ↔ j / i < i0 | A User Theorem |
| nummult-ls-03 | ⊦ 0 < i ∧ j < 0 → ((* j) < (* i) * i0 ↔ (j + 1 - i) / i < i0) | A User Theorem |
| nummult-ls-03-01 | 0 < i, j < 0 ⊦ (* j) < (* i) * i0 ↔ (j + 1 - i) / i < i0 | A User Theorem |
| nummult-ls-04 | 0 < i, 0 ≤ j ⊦ (* i) * i0 < (* j) ↔ i0 < (i + j - 1) / i | A User Theorem |
| nummult-modle | 0 < i, i < j, j % i = 0 ⊦ (* i) * i0 ≤ (* j) * j0 ↔ i0 ≤ j / i * j0 | A User Theorem |
| nummult-modle-01 | 0 < j, j < i, i % j = 0 ⊦ (* i) * i0 ≤ (* j) * j0 ↔ i / j * i0 ≤ j0 | A User Theorem |
| nummult-modls | 0 < i, i < j, j % i = 0 ⊦ (* i) * i0 < (* j) * j0 ↔ i0 < j / i * j0 | A User Theorem |
| nummult-modls-01 | 0 < j, j < i, i % j = 0 ⊦ (* i) * i0 < (* j) * j0 ↔ i / j * i0 < j0 | A User Theorem |
| one | ⊦ i / 1 = i | A User Theorem |
| one-01 | ⊦ i = 1 → j % i = 0 | A User Theorem |
| one-02 | j ≠ 0 ⊦ 1 / j = 1 ↔ j = 1 | A User Theorem |
| one-03 | ⊦ 1 < j → 1 % j = 1 | A User Theorem |
| one-04 | ⊦ 1 < j → 1 / j = 0 | A User Theorem |
| one-05 | ⊦ 1 < j → ~1 % j = ~1 | A User Theorem |
| one-06 | ⊦ 1 < j → ~1 % 1 = 0 | A User Theorem |
| one-lez | ⊦ 1 / i ≤ 0 ∧ 0 < i → 1 / i = 0 ∧ 1 < i | A User Theorem |
| one-neg | j ≠ 0 ⊦ 1 / j < 0 ↔ j = ~1 | A User Theorem |
| one-pos | j ≠ 0 ⊦ 0 < 1 / j ↔ j = 1 | A User Theorem |
| pdiv-ls | i / j < j0, i0 ≤ i, 0 < j ⊦ i0 / j < j0 | A User Theorem |
| pos | ⊦ 0 < j ∧ 0 ≤ i → 0 ≤ i / j | A User Theorem |
| prod-div-less | ⊦ 0 < i ∧ i < j ∧ 0 < i1 ∧ i1 < j → (i * i1) / j < i | A User Theorem |
| prod-div-less-01 | ⊦ 0 < i ∧ i < j ∧ 0 < i1 ∧ i1 < j → (i * i1) / j < i1 | A User Theorem |
| quad-div-less | ⊦ 0 < i ∧ i < j → (i * i) / j < i | A User Theorem |
| square-even | ⊦ 0 ≤ i → (i * (i + 1)) % 2 = 0 | A User Theorem |
| square-even-01 | ⊦ (i * (i + 1)) % 2 = 0 | A User Theorem |
| square-even-02 | ⊦ ((i + 1) * (i + 2)) % 2 = 0 | A User Theorem |
| square-inject | ⊦ 0 ≤ i ∧ 0 ≤ j ∧ 0 ≤ i0 ∧ 0 ≤ j0 → (((i + j) * (i + j + 1)) / 2 + j = ((i0 + j0) * (i0 + j0 + 1)) / 2 + j0 ↔ i = i0 ∧ j = j0) | A User Theorem |
| square-interval | (i * (i + 1)) / 2 ≤ (j * (j + 1)) / 2 + j0, (j * (j + 1)) / 2 + j0 < ((i + 1) * (i + 2)) / 2, j0 ≤ j, 0 ≤ i, 0 ≤ j0 ⊦ i = j | A User Theorem |
| square-ls | ⊦ 0 ≤ i ∧ 0 ≤ j → ((i * (i + 1)) / 2 < (j * (j + 1)) / 2 ↔ i < j) | A User Theorem |
| square-ls-01 | ⊦ 0 ≤ i ∧ 0 ≤ j → ((i * (i + 1)) / 2 < ((j + 1) * (j + 2)) / 2 ↔ i < j + 1) | A User Theorem |
| square-ls-02 | ⊦ 0 ≤ i ∧ 0 ≤ j → (((i + 1) * (i + 2)) / 2 < ((j + 1) * (j + 2)) / 2 ↔ i < j) | A User Theorem |
| square-nle | ⊦ 0 ≤ j → ((j * (j + 1)) / 2 ≤ j ↔ j < 2) | A User Theorem |
| square-nle-01 | ⊦ 0 ≤ j → ¬ ((j + 1) * (j + 2)) / 2 ≤ j | A User Theorem |
| square-nle-02 | ⊦ 0 ≤ j ∧ i ≤ 0 → ¬ ((j + 1) * (j + 2)) / 2 ≤ i + j | A User Theorem |
| square-nls | ⊦ 0 ≤ j → ¬ (j * (j + 1)) / 2 < j | A User Theorem |
| square-nls-01 | ⊦ 0 ≤ j ∧ i < 0 → ¬ (j * (j + 1)) / 2 < i + j | A User Theorem |
| square-nls-02 | ⊦ 0 ≤ j ∧ i ≤ 0 → ¬ (j * (j + 1)) / 2 < i + j | A User Theorem |
| sub-ls | ⊦ 0 < i0 ∧ i < j → (i - j) / i0 ≤ 0 | A User Theorem |
| sub-ls-01 | ⊦ 0 < i0 ∧ j ≤ i → 0 ≤ (i - j) / i0 | A User Theorem |
| three | ⊦ (1 + 1 + 1) / 2 = 1 | A User Theorem |
| two-add-square | ⊦ 0 ≤ i → ((i * (i - 1)) / 2 + i ≠ (i * (i + 1)) / 2 ↔ false) | A User Theorem |
| two-add-square-01 | ⊦ 0 < i → ((i * (i - 1)) / 2 + i ≠ (i * (i + 1)) / 2 ↔ false) | A User Theorem |
| two-even | ⊦ i % 2 = 0 → (i / 2 = j ↔ i = 2 * j) | A User Theorem |
| two-mult | ⊦ 0 < i ∧ 0 < j0 → (2 * i - 1) / (2 * j0) = (i - 1) / j0 | A User Theorem |
| two-mult-01 | ⊦ 0 < i → (2 * i - 1) / 2 = i - 1 | A User Theorem |
| two-odd | ⊦ i % 2 = 0 ∧ 0 < i → (i - 1) / 2 = i / 2 - 1 | A User Theorem |
| zero | j ≠ 0 ⊦ 0 / j = 0 | A User Theorem |
| zero-01 | ⊦ 0 < j ∧ i < 0 → i / j ≤ 0 | A User Theorem |
| zero-02 | ⊦ 0 < i ∧ j < 0 → i / j ≤ 0 | A User Theorem |
| zero-03 | ⊦ 0 < i ∧ 0 < j → 0 ≤ i / j | A User Theorem |
| zero-04 | 0 < i0, i / i0 + j / i0 < 0 ⊦ i + j < 0 | A User Theorem |
| zero-05 | j ≠ 0 ⊦ i < 0 → i ≤ i / j | A User Theorem |
| zero-06 | j ≠ 0 ⊦ i < 0 ∧ j < 0 → 0 ≤ i / j | A User Theorem |
| zero-07 | j ≠ 0 ⊦ 0 < i → i / j ≤ i | A User Theorem |