Proof step 52 from proof square-neq-any-pos-02 (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  j / gcd(j, j0 * j1) * j / gcd(j0 * j1, j) = (j0 * j1) / gcd(j0 * j1, j) * (j0 * j1) / gcd(j0 * j1, j) * i, j * j / gcd(j0 * j1, j) = (j0 * j1) * (j0 * j1) / gcd(j0 * j1, j) * i, gcd(j, j0) = 1, (j0 * j1) / gcd(j0 * j1, j) < j / gcd(j, j0 * j1), (j0 * j1) / gcd(j0 * j1, j) < j, (j0 * j1) / gcd(j0 * j1, j) < j0, (j0 * j1) / gcd(j0 * j1, j) < j1, (j0 * j1) / gcd(j0 * j1, j) < i, (j0 * j1) / gcd(j0 * j1, j) ≤ 0, 0 < j / gcd(j, j0 * j1), prime(j1), 1 < j1 * j1 * i, 0 ≤ j0, 0 < j, 0 < j0, 0 < j1, 0 < i, j0 * j1 < j, ∀ i1, j, j0. i→n(i1) < i→n(j1 * j1 * i) → 0 < i1 ∧ 0 < j ∧ 0 < j0 ∧ gcd(j, j0) = 1 ∧ j * j = i1 * j0 * j0 → (∃ i2. i1 = i2 * i2) ⊦ gcd(j0 * j1, j) = 1, j1 = 0, j = 0, ∃ i1. j1 * j1 * i = i1 * i1

Rule argument

Additional information

Used simplifier rules: gcd-div-gcd: ⊦ i ≠ 0 → gcd(i / gcd(i, j), j / gcd(i, j)) = 1;%gcd-com: ⊦ gcd(i, j) = gcd(j, i);%div-gcd-not-neg: ⊦ 0 < i → ¬ i / gcd(i, i0) ≤ 0;%gcd-less-eq-zero: ⊦ gcd(i, j) ≤ 0 ↔ gcd(i, j) = 0;%gcd-zero-zero: ⊦ gcd(i, j) = 0 ↔ i = 0 ∧ j = 0;%lsfc-01: 0 < i0 ⊦ i / i0 < j / i0 → i < j; (forward) from specification int-div%zero-neq-01: ⊦ 0 < i → (i * j = 0 ↔ j = 0); from specification int-mult%zero-gels-04: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs%forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs%forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs%forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs%lels: ⊦ ¬ i < j ↔ j ≤ i; from specification int-abs%commutativity: ⊦ i * j = j * i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult