Proof step 1 from proof square-neq-pos (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  j * j = i * j0 * j0, 0 < j, prime(i), 0 ≤ j0 ⊦

Rule argument

Additional information

Proof step 2 from proof square-neq-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  j * j = i * j0 * j0, 0 < j, prime(i), 0 ≤ j0 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs

Proof step 3 from proof square-neq-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ prime(i) ∧ gcd(j, j0) = 1 ∧ 0 < j ∧ 0 ≤ j0 → j * j ≠ i * j0 * j0

• Proof step 5:

  j * j = i * j0 * j0, 0 < j, prime(i), 0 ≤ j0 ⊦ prime(i) ∧ gcd(j, j0) = 1 ∧ 0 < j ∧ 0 ≤ j0

Rule argument

Additional information

Used terms: j0, i, j

Proof step 4 from proof square-neq-pos (previous step) (back to tree)

Lemma square-neq-pos-h

Proof step 5 from proof square-neq-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  j * j = i * j0 * j0, gcd(j, j0) ≠ 1, 0 < j, prime(i), 0 ≤ j0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s)

Proof step 6 from proof square-neq-pos (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 7:

  j * j = i * j0 * j0, (j * j) / gcd(j, j0) = (i * j0 * j0) / gcd(j, j0), gcd(j, j0) ≠ 1, 0 < j, prime(i), 0 ≤ j0 ⊦

Rule argument

Additional information

Used simplifier rules: neqf: ⊦ i / j ≠ i / i0 → j ≠ i0; (forward) from specification int-div Used formulas: (j * j) / gcd(j, j0) = (i * j0 * j0) / gcd(j, j0)

Proof step 7 from proof square-neq-pos (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 8:

  (j * j) / gcd(j, j0) = (i * j0 * j0) / gcd(j, j0), gcd(j, j0) ≠ 1, 0 < j, prime(i), 0 ≤ j0 ⊦

Rule argument

Additional information

Proof step 8 from proof square-neq-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ i0 ≠ 0 → (i0 * j) / gcd(i0, j0) = i0 / gcd(i0, j0) * j

• Proof step 10:

  j / gcd(j, j0) * j = (i * j0 * j0) / gcd(j, j0), gcd(j, j0) ≠ 1, j ≠ 0, 0 < j, prime(i), 0 ≤ j0 ⊦

Rule argument

Additional information

Used simplifier rules: gcd-zero-04: ⊦ gcd(i, 0) = abs(i); gcd-com: ⊦ gcd(i, j) = gcd(j, i); associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ 0 ≤ i → abs(i) = i; (s) Used terms: j0, j, j

Proof step 9 from proof square-neq-pos (previous step) (back to tree)

Lemma gcd-div-shift

Proof step 10 from proof square-neq-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  j / gcd(j, j0) * j = (i * j0 * j0) / gcd(j, j0), gcd(j, j0) ≠ 1, j ≠ 0, 0 < j, prime(i), 0 ≤ j0 ⊦

Rule argument

Additional information

Proof step 11 from proof square-neq-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ i * j = j * i

• Proof step 13:

  j / gcd(j, j0) * j = ((j0 * j0) * i) / gcd(j, j0), gcd(j, j0) ≠ 1, j ≠ 0, 0 < j, prime(i), 0 ≤ j0 ⊦

Rule argument

Additional information

Used terms: j0 * j0, i

Proof step 12 from proof square-neq-pos (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof square-neq-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ i0 ≠ 0 → (i0 * j) / gcd(i0, j0) = i0 / gcd(i0, j0) * j

• Proof step 15:

  j / gcd(j, j0) * j = j0 / gcd(j0, j) * j0 * i, gcd(j, j0) ≠ 1, j ≠ 0, j0 ≠ 0, 0 < j, prime(i), 0 ≤ j0 ⊦

Rule argument

Additional information

Used simplifier rules: gcd-com: ⊦ gcd(i, j) = gcd(j, i); gcd-zero-03: ⊦ i ≠ 0 → gcd(i, 0) = abs(i); i ≠ 0 ⊦ i / i = 1; (s) ⊦ 1 * i = i; (s) ⊦ i * 0 = 0; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < j → abs(j) = j; (s) j ≠ 0 ⊦ 0 / j = 0; (s) Used terms: j, j0 * i, j0

Proof step 14 from proof square-neq-pos (previous step) (back to tree)

Lemma gcd-div-shift

Proof step 15 from proof square-neq-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  j / gcd(j, j0) * j = j0 / gcd(j0, j) * j0 * i, gcd(j, j0) ≠ 1, j ≠ 0, j0 ≠ 0, 0 < j, 0 < j0, prime(i) ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ i ≠ j → (i ≤ j ↔ i < j); (s)

Proof step 16 from proof square-neq-pos (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 17:

  j / gcd(j, j0) * j = j0 / gcd(j0, j) * j0 * i, (j / gcd(j, j0) * j) / gcd(j, j0) = (j0 / gcd(j0, j) * j0 * i) / gcd(j, j0), gcd(j, j0) ≠ 1, j ≠ 0, j0 ≠ 0, 0 < j0, 0 < j, prime(i) ⊦

Rule argument

Additional information

Used simplifier rules: associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult neqf: ⊦ i / j ≠ i / i0 → j ≠ i0; (forward) from specification int-div Used formulas: (j / gcd(j, j0) * j) / gcd(j, j0) = (j0 / gcd(j0, j) * j0 * i) / gcd(j, j0)

Proof step 17 from proof square-neq-pos (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 18:

  (j / gcd(j, j0) * j) / gcd(j, j0) = (j0 / gcd(j0, j) * j0 * i) / gcd(j, j0), gcd(j, j0) ≠ 1, j ≠ 0, j0 ≠ 0, 0 < j, 0 < j0, prime(i) ⊦

Rule argument

Additional information

Proof step 18 from proof square-neq-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ i * j = j * i

• Proof step 20:

  (j * j / gcd(j, j0)) / gcd(j, j0) = (j0 / gcd(j0, j) * j0 * i) / gcd(j, j0), gcd(j, j0) ≠ 1, j ≠ 0, j0 ≠ 0, 0 < j0, 0 < j, prime(i) ⊦

Rule argument

Additional information

Used terms: j, j / gcd(j, j0)

Proof step 19 from proof square-neq-pos (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof square-neq-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ i0 ≠ 0 → (i0 * j) / gcd(i0, j0) = i0 / gcd(i0, j0) * j

• Proof step 22:

  j / gcd(j, j0) * j / gcd(j, j0) = (j0 / gcd(j0, j) * j0 * i) / gcd(j, j0), gcd(j, j0) ≠ 1, j ≠ 0, j0 ≠ 0, 0 < j, 0 < j0, prime(i) ⊦

Rule argument

Additional information

Used terms: j0, j / gcd(j, j0), j

Proof step 21 from proof square-neq-pos (previous step) (back to tree)

Lemma gcd-div-shift

Proof step 22 from proof square-neq-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  j / gcd(j, j0) * j / gcd(j, j0) = (j0 / gcd(j0, j) * j0 * i) / gcd(j, j0), gcd(j, j0) ≠ 1, j ≠ 0, j0 ≠ 0, 0 < j0, 0 < j, prime(i) ⊦

Rule argument

Additional information

Proof step 23 from proof square-neq-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ i * j = j * i

• Proof step 25:

  j / gcd(j, j0) * j / gcd(j, j0) = ((j0 * i) * j0 / gcd(j0, j)) / gcd(j, j0), gcd(j, j0) ≠ 1, j ≠ 0, j0 ≠ 0, 0 < j, 0 < j0, prime(i) ⊦

Rule argument

Additional information

Used terms: j0 * i, j0 / gcd(j0, j)

Proof step 24 from proof square-neq-pos (previous step) (back to tree)

A spec-lemma

Proof step 25 from proof square-neq-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ i0 ≠ 0 → (i0 * j) / gcd(i0, j0) = i0 / gcd(i0, j0) * j

• Proof step 27:

  j / gcd(j, j0) * j / gcd(j, j0) = j0 / gcd(j0, j) * i * j0 / gcd(j0, j), gcd(j, j0) ≠ 1, j ≠ 0, j0 ≠ 0, 0 < j0, 0 < j, prime(i) ⊦

Rule argument

Additional information

Used simplifier rules: gcd-com: ⊦ gcd(i, j) = gcd(j, i); associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j, i * j0 / gcd(j0, j), j0

Proof step 26 from proof square-neq-pos (previous step) (back to tree)

Lemma gcd-div-shift

Proof step 27 from proof square-neq-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  j / gcd(j, j0) * j / gcd(j, j0) = j0 / gcd(j0, j) * i * j0 / gcd(j0, j), gcd(j, j0) ≠ 1, j ≠ 0, j0 ≠ 0, 0 < j, 0 < j0, prime(i) ⊦

Rule argument

Additional information

Proof step 28 from proof square-neq-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ i * j = j * i

• Proof step 30:

  j / gcd(j, j0) * j / gcd(j, j0) = (i * j0 / gcd(j0, j)) * j0 / gcd(j0, j), gcd(j, j0) ≠ 1, j ≠ 0, j0 ≠ 0, 0 < j0, 0 < j, prime(i) ⊦

Rule argument

Additional information

Used terms: i * j0 / gcd(j0, j), j0 / gcd(j0, j)

Proof step 29 from proof square-neq-pos (previous step) (back to tree)

A spec-lemma

Proof step 30 from proof square-neq-pos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

  ⊦ prime(i) ∧ gcd(j, j0) = 1 ∧ 0 < j ∧ 0 ≤ j0 → j * j ≠ i * j0 * j0

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-nls-zero: ⊦ 0 < i → ¬ i / gcd(i, j) < 0; ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j ↔ ¬ j < i; (ss) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j0 / gcd(j0, j), i, j / gcd(j, j0)

Proof step 31 from proof square-neq-pos (previous step) (back to tree)

Lemma square-neq-pos-h