| gcd(i, j) = 1, i * i0 = j ^ i1 * j, i * i2 = j ^ i1, 0 < i, 1 < i, 0 ≤ i1, ∀ j1, i, i0, j. i→n(j1) < i→n(i1 + 1) → i * i0 = j ^ j1 ∧ gcd(i, j) = 1 ∧ 0 < i ∧ 1 < i ∧ 0 < j1 → j = 0 ⊦ j = 0 |
Used simplifier rules: numlelsdel-01: i0 ≠ 0, i0 ≤ i ⊦ (* i) < j → (* i0) < j; from specification int-abs%lels: ⊦ ¬ i < j ↔ j ≤ i; from specification int-abs%anti: ⊦ i ≤ j → (j ≤ i ↔ i = j); from specification int-abs%Pot-zero: ⊦ j ^ 0 = 1; from specification int-pot%eq-one: ⊦ i * j = 1 ↔ abs(i) = 1 ∧ i = j; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%one: ⊦ 1 * i = i; from specification int-mult%lf-02: ⊦ i < j ∧ j = i0 → i < i0; (forward) from specification int-basic1%abs-16: ⊦ 0 < j → abs(j) = j; from specification int-abs%one-01: ⊦ i = 1 → i * j = j; from specification int-mult%forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1%rax-04: ⊦ 0 ≤ i → i→n(i + 1) = i→n(i) + 1; from specification intnat%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%s: ⊦ m < n + 1 ↔ ¬ n < m; from specification nat-basic2%labs: ⊦ i→n(i) < i→n(j) ↔ abs(i) < abs(j); from specification intnat%absle: ⊦ 0 ≤ i → abs(i) = i; from specification int-abs%irref: ⊦ ¬ i < i; from specification int-basic1%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%c: ⊦ m + n = n + m; from specification nat-basic2 Used terms: i1, i, i2, j