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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  j * j = i * j0 * j0, gcd(j, j0) = 1, 0 < j0, 0 < j, 0 < i ⊦ ∃ i0. i = i0 * i0

Rule argument

Additional information

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

User applied rule induction

And obtained the following new goals

• Proof step 3:

  j * j = i * j0 * j0, gcd(j, j0) = 1, 0 < j0, 0 < j, 0 < i, ∀ i0, j, j0. i→n(i0) < i→n(i) → j * j = i0 * j0 * j0 ∧ gcd(j, j0) = 1 ∧ 0 < j0 ∧ 0 < j ∧ 0 < i0 → (∃ i1. i0 = i1 * i1) ⊦ ∃ i0. i = i0 * i0

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: i→n(i)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  j * j = i * j0 * j0, gcd(j, j0) = 1, 0 < i, 0 < j, 0 < j0, ∀ i0, j, j0. i→n(i0) < i→n(i) → j * j = i0 * j0 * j0 ∧ gcd(j, j0) = 1 ∧ 0 < j0 ∧ 0 < j ∧ 0 < i0 → (∃ i1. i0 = i1 * i1) ⊦ ∃ i0. i = i0 * i0

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

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

Rule argument

Additional information

Used terms: j0, i, j

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

Lemma square-neq-pos-h

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

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

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

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

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

• Proof step 80:

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

Rule argument

Additional information

Used formulas: 1 < i

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ 1 < i → (prime(i) ↔ (∀ j. prime(j) ∧ j * j ≤ i → ¬ j | i))

• Proof step 10:

  j * j = i * j0 * j0, gcd(j, j0) = 1, 0 < j0, 0 < j, 0 < i, 1 < i, 0 ≤ j0, ∃ j. ¬(prime(j) ∧ j * j ≤ i → ¬ j | i), ∀ i0, j, j0. i→n(i0) < i→n(i) → j * j = i0 * j0 * j0 ∧ gcd(j, j0) = 1 ∧ 0 < j0 ∧ 0 < j ∧ 0 < i0 → (∃ i1. i0 = i1 * i1) ⊦ ∃ i0. i = i0 * i0

Rule argument

Additional information

Used terms: i

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

Lemma prime-def-prime

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used simplifier rules: forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ i | j ↔ (∃ i0. i * i0 = j)

• Proof step 13:

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

Rule argument

Additional information

Used terms: i, j1

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

Lemma divides

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

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

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

User applied rule cut formula

And obtained the following new goals

• Proof step 15:

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

• Proof step 62:

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

Rule argument

Additional information

Used formulas: j1 | i0

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ i | j ↔ (∃ i0. i * i0 = j)

• Proof step 17:

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

Rule argument

Additional information

Used terms: i0, j1

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

Lemma divides

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

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

Rule argument

Additional information

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

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

User applied rule apply induction

And obtained the following new goals

• Proof step 19:

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

• Proof step 25:

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

• Proof step 60:

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

Rule argument

Additional information

Used terms: i1, j, j0 * j1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

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

Rule argument

Additional information

Used simplifier rules: prime-abs: ⊦ prime(j) → abs(j) = j; ⊦ i < j ↔ ¬ j ≤ i; (ss) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ abs(i * j) = abs(i) * abs(j); (s) ⊦ i→n(i) < i→n(j) ↔ abs(i) < abs(j); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ 1 < i → (i * abs(j) ≤ abs(j) ↔ j = 0)

• Proof step 22:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i * i = 0 ↔ i = 0; (s) ⊦ i * i ≤ 0 ↔ i = 0; (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 Used terms: j1 * j1, i1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ls-forward: ⊦ i * j < i * j0 → i ≠ 0; (forward) from specification int-mult forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs ⊦ i < j ↔ ¬ j ≤ i; (ss)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ 1 < j → (i * j ≤ 1 ↔ i ≤ 0)

Rule argument

Additional information

Used simplifier rules: prime-one: ⊦ i ≤ 1 → ¬ prime(i); prime-not-neg: ⊦ j < 0 → ¬ prime(j); ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i < 0 → (i * j ≤ i * i0 ↔ i0 ≤ j); (s) ⊦ i < 0 → (i * j ≤ i ↔ 1 ≤ j); (s) ⊦ 1 ≤ i ↔ 0 < i; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i < j ↔ ¬ j ≤ i; (ss) Used terms: j1, j1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

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

Rule argument

Additional information

Used simplifier rules: prime-not-neg-01: ⊦ j ≤ 0 → ¬ prime(j); forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < i → (0 < i * j ↔ 0 < j); (s) ⊦ ¬ i * i < 0; (s) ⊦ i ≤ 0 → (0 < i * j ↔ j < 0 ∧ i ≠ 0); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 27:

  j * j = (j1 * j1 * i1) * j0 * j0, (j1 * j1 * i1) * j0 * j0 = i1 * (j0 * j1) * j0 * j1, gcd(j, j0) = 1, gcd(j, j0 * j1) ≠ 1, 0 < i1, 0 < j1, 1 < j1 * j1 * i1, 0 < j0, 0 < j, prime(j1), 0 ≤ j0, j1 * j1 ≤ j1 * j1 * i1, ∀ i, j, j0. i→n(i) < i→n(j1 * j1 * i1) → j * j = i * j0 * j0 ∧ gcd(j, j0) = 1 ∧ 0 < j0 ∧ 0 < j ∧ 0 < i → (∃ i0. i = i0 * i0) ⊦ ∃ i. j1 * j1 * i1 = i * 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 Used formulas: (j1 * j1 * i1) * j0 * j0 = i1 * (j0 * j1) * j0 * j1

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

User applied rule subst equation

And obtained the following new goals

• Proof step 28:

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

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 29:

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

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 * j1) = (i1 * (j0 * j1) * j0 * j1) / gcd(j, j0 * j1)

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

User applied rule weakening

And obtained the following new goals

• Proof step 30:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

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

• Proof step 32:

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

Rule argument

Additional information

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

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

Lemma gcd-div-shift

Proof step 32 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 33:

  j / gcd(j, j0 * j1) * j = (i1 * (j0 * j1) * j0 * j1) / gcd(j, j0 * j1), i1 * (j0 * j1) * j0 * j1 = (j0 * j1) * i1 * j0 * j1, gcd(j, j0) = 1, gcd(j, j0 * j1) ≠ 1, j ≠ 0, 0 < j, 0 < j0, 1 < j1 * j1 * i1, 0 < j1, 0 < i1, prime(j1), j1 * j1 ≤ j1 * j1 * i1, 0 ≤ j0, ∀ i, j, j0. i→n(i) < i→n(j1 * j1 * i1) → j * j = i * j0 * j0 ∧ gcd(j, j0) = 1 ∧ 0 < j0 ∧ 0 < j ∧ 0 < i → (∃ i0. i = i0 * i0) ⊦ ∃ i. j1 * j1 * i1 = i * 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 Used formulas: i1 * (j0 * j1) * j0 * j1 = (j0 * j1) * i1 * j0 * j1

Proof step 33 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 34:

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

Rule argument

Additional information

Proof step 34 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  ⊦ gcd(i, j) = gcd(j, i)

• Proof step 36:

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

Rule argument

Additional information

Used terms: j0 * j1, j

Proof step 35 from proof square-neq-any-pos-02 (previous step) (back to tree)

Lemma gcd-com

Proof step 36 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

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

• Proof step 38:

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

Rule argument

Additional information

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

Proof step 37 from proof square-neq-any-pos-02 (previous step) (back to tree)

Lemma gcd-div-shift

Proof step 38 from proof square-neq-any-pos-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ i * j = 0 ↔ i = 0 ∨ j = 0; (ws)

Proof step 39 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 40:

  j / gcd(j0 * j1, j) * j = (j0 * j1) / gcd(j0 * j1, j) * i1 * j0 * j1, (j / gcd(j0 * j1, j) * j) / gcd(j0 * j1, j) = ((j0 * j1) / gcd(j0 * j1, j) * i1 * j0 * j1) / gcd(j0 * j1, j), gcd(j, j0) = 1, gcd(j0 * j1, j) ≠ 1, j ≠ 0, j0 ≠ 0, j1 ≠ 0, 0 < j0, 0 < i1, 0 < j1, 1 < j1 * j1 * i1, 0 < j, prime(j1), j1 * j1 ≤ j1 * j1 * i1, ∀ i, j, j0. i→n(i) < i→n(j1 * j1 * i1) → j * j = i * j0 * j0 ∧ gcd(j, j0) = 1 ∧ 0 < j0 ∧ 0 < j ∧ 0 < i → (∃ i0. i = i0 * i0) ⊦ ∃ i. j1 * j1 * i1 = i * 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(j0 * j1, j) * j) / gcd(j0 * j1, j) = ((j0 * j1) / gcd(j0 * j1, j) * i1 * j0 * j1) / gcd(j0 * j1, j)

Proof step 40 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 41:

  ⊦ i * j = j * i

• Proof step 42:

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

Rule argument

Additional information

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

Proof step 41 from proof square-neq-any-pos-02 (previous step) (back to tree)

A spec-lemma

Proof step 42 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

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

• Proof step 44:

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

Rule argument

Additional information

Used simplifier rules: gcd-com: ⊦ gcd(i, j) = gcd(j, i); Used terms: j0 * j1, j / gcd(j0 * j1, j), j

Proof step 43 from proof square-neq-any-pos-02 (previous step) (back to tree)

Lemma gcd-div-shift

Proof step 44 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 45:

  j * j / gcd(j0 * j1, j) = (j0 * j1) / gcd(j0 * j1, j) * i1 * j0 * j1, j / gcd(j, j0 * j1) * j / gcd(j0 * j1, j) = ((j0 * j1) / gcd(j0 * j1, j) * i1 * j0 * j1) / gcd(j0 * j1, j), (j0 * j1) / gcd(j0 * j1, j) * i1 * j0 * j1 = (j0 * j1) * (j0 * j1) / gcd(j0 * j1, j) * i1, gcd(j, j0) = 1, gcd(j0 * j1, j) ≠ 1, j ≠ 0, j0 ≠ 0, j1 ≠ 0, 0 < j, 1 < j1 * j1 * i1, 0 < j1, 0 < i1, 0 < j0, prime(j1), j1 * j1 ≤ j1 * j1 * i1, ∀ i, j, j0. i→n(i) < i→n(j1 * j1 * i1) → j * j = i * j0 * j0 ∧ gcd(j, j0) = 1 ∧ 0 < j0 ∧ 0 < j ∧ 0 < i → (∃ i0. i = i0 * i0) ⊦ ∃ i. j1 * j1 * i1 = i * 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 Used formulas: (j0 * j1) / gcd(j0 * j1, j) * i1 * j0 * j1 = (j0 * j1) * (j0 * j1) / gcd(j0 * j1, j) * i1

Proof step 45 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 46:

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

Rule argument

Additional information

Proof step 46 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 47:

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

• Proof step 48:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i * j = 0 ↔ i = 0 ∨ j = 0; (ws) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j, (j0 * j1) / gcd(j0 * j1, j) * i1, j0 * j1

Proof step 47 from proof square-neq-any-pos-02 (previous step) (back to tree)

Lemma gcd-div-shift

Proof step 48 from proof square-neq-any-pos-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

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

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ i * j = 0 ↔ i = 0 ∨ j = 0; (ws)

Proof step 49 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 50:

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

• Proof step 53:

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

• Proof step 58:

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

Rule argument

Additional information

Used terms: i1, j / gcd(j, j0 * j1), (j0 * j1) / gcd(j0 * j1, j)

Proof step 50 from proof square-neq-any-pos-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

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

Rule argument

Additional information

Used simplifier rules: forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1 commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < i → (i < i * j ↔ 1 < j); (s) ⊦ 0 < i → (i * j < i * j0 ↔ j < j0); (s) ⊦ 0 < i → (i * j ≤ i ↔ j ≤ 1); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ 0 < j → abs(j) = j; (s) ⊦ abs(i * j) = abs(i) * abs(j); (s) ⊦ i→n(i) < i→n(j) ↔ abs(i) < abs(j); (s)

Proof step 51 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

  ⊦ 1 < j → (i * j ≤ 1 ↔ i ≤ 0)

Rule argument

Additional information

Used simplifier rules: gcd-com: ⊦ gcd(i, j) = gcd(j, i); ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i < j → ¬ j < i; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ 0 < i → (i ≤ 1 ↔ i = 1); (s) ⊦ i = 1 → i * j = j; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j1, j1

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

A spec-lemma

Proof step 53 from proof square-neq-any-pos-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

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

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; forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (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 ⊦ i < j ↔ ¬ j ≤ i; (ss) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult

Proof step 54 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 55:

  ⊦ 0 < j → (i / j ≤ 0 ↔ i < j)

• Proof step 56:

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

Rule argument

Additional information

Used simplifier rules: gcd-less-eq-zero: ⊦ gcd(i, j) ≤ 0 ↔ gcd(i, j) = 0; gcd-zero-zero: ⊦ gcd(i, j) = 0 ↔ i = 0 ∧ j = 0; ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i * j = 0 ↔ i = 0 ∨ j = 0; (ws) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: gcd(j0 * j1, j), j0 * j1

Proof step 55 from proof square-neq-any-pos-02 (previous step) (back to tree)

A spec-lemma

Proof step 56 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 57:

  ⊦ 0 < i → ¬ i < gcd(i, j)

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < i → (0 < i * j ↔ 0 < j); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i < j → ¬ j < i; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j, j0 * j1

Proof step 57 from proof square-neq-any-pos-02 (previous step) (back to tree)

Lemma not-less-gcd

Proof step 58 from proof square-neq-any-pos-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

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

Rule argument

Additional information

Used simplifier rules: gcd-com: ⊦ gcd(i, j) = gcd(j, i); gcd-zero-zero: ⊦ gcd(i, j) = 0 ↔ i = 0 ∧ j = 0; gcd-abs: ⊦ abs(gcd(i, j)) = gcd(i, j); commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < i → (0 < i * j ↔ 0 < j); (s) forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1 ⊦ 0 < j → abs(j) = j; (s) ⊦ abs(i * j) = abs(i) * abs(j); (s) ⊦ i * i = j * j ↔ abs(i) = abs(j); (s) j ≠ 0 ⊦ abs(i / j) = abs(i) / abs(j); (s) ⊦ i * j = 0 ↔ i = 0 ∨ j = 0; (ws)

Proof step 59 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: prime-abs: ⊦ prime(j) → abs(j) = j; ⊦ abs(i * j) = abs(i) * abs(j); (s) ⊦ abs(abs(i)) = abs(i); (s) ⊦ i ≠ 0 → (i * j = i * j0 ↔ j = j0); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j1 * abs(i0)

Proof step 60 from proof square-neq-any-pos-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

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

Rule argument

Additional information

Used simplifier rules: prime-abs: ⊦ prime(j) → abs(j) = j; gcd-mult-01: ⊦ gcd(i, i * j) = abs(i); gcd-com: ⊦ gcd(i, j) = gcd(j, i); forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i = 1 → i * j = j; (s) ⊦ 0 < j → abs(j) = j; (s) forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1 ⊦ abs(i * j) = abs(i) * abs(j); (s) ⊦ i * i = j * j ↔ abs(i) = abs(j); (s) ⊦ i * i ≤ j * j ↔ abs(i) ≤ abs(j); (s)

Proof step 61 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: prime-abs: ⊦ prime(j) → abs(j) = j; ⊦ abs(i * j) = abs(i) * abs(j); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j1 * i0

Proof step 62 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 63:

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

• Proof step 77:

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

Rule argument

Additional information

Used formulas: j1 | j

Proof step 63 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 64:

  ⊦ i | j ↔ (∃ i0. i * i0 = j)

• Proof step 65:

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

Rule argument

Additional information

Used terms: j, j1

Proof step 64 from proof square-neq-any-pos-02 (previous step) (back to tree)

Lemma divides

Proof step 65 from proof square-neq-any-pos-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

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

Rule argument

Additional information

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

Proof step 66 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 67:

  ⊦ i ≠ 0 → (i * j = i * j0 ↔ j = j0)

• Proof step 68:

  i * j1 * i = j0 * j0 * i0, gcd(j1 * i, j0) = 1, j1 ≠ 0, 0 < j1 * i, 0 < j1 * i0, 1 < j1 * i0, 0 < j0, prime(j1), 0 ≤ j0, j1 * j1 ≤ j1 * i0, ¬ j1 | i0, ∀ i1, j, j0. i→n(i1) < i→n(j1 * i0) → j * j = i1 * j0 * j0 ∧ gcd(j, j0) = 1 ∧ 0 < j0 ∧ 0 < j ∧ 0 < i1 → (∃ i. i1 = i * i) ⊦ ∃ i1. j1 * i0 = i1 * i1

Rule argument

Additional information

Used simplifier rules: gcd-zero-04: ⊦ gcd(i, 0) = abs(i); gcd-com: ⊦ gcd(i, j) = gcd(j, i); prime-small: ⊦ j < 2 → ¬ prime(j); ⊦ 0 < j → abs(j) = j; (s) ⊦ i * 0 = 0; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j0 * j0 * i0, i * j1 * i, j1

Proof step 67 from proof square-neq-any-pos-02 (previous step) (back to tree)

A spec-lemma

Proof step 68 from proof square-neq-any-pos-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

  i * j1 * i = j0 * j0 * i0, gcd(j1 * i, j0) = 1, j1 ≠ 0, 0 < j0, 1 < j1 * i0, 0 < j1 * i0, 0 < j1 * i, prime(j1), j1 * j1 ≤ j1 * i0, 0 ≤ j0, ¬ j1 | i0, ∀ i1, j, j0. i→n(i1) < i→n(j1 * i0) → j * j = i1 * j0 * j0 ∧ gcd(j, j0) = 1 ∧ 0 < j0 ∧ 0 < j ∧ 0 < i1 → (∃ i. i1 = i * i) ⊦ ∃ i1. j1 * i0 = i1 * i1

Rule argument

Additional information

Proof step 69 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 70:

  i * j1 * i = j0 * j0 * i0, gcd(j1 * i, j0) = 1, j1 ≠ 0, 0 < j1 * i, 0 < j1 * i0, 1 < j1 * i0, 0 < j0, prime(j1), j1 | j0 * j0 * i0, 0 ≤ j0, j1 * j1 ≤ j1 * i0, ¬ j1 | i0, ∀ i1, j, j0. i→n(i1) < i→n(j1 * i0) → j * j = i1 * j0 * j0 ∧ gcd(j, j0) = 1 ∧ 0 < j0 ∧ 0 < j ∧ 0 < i1 → (∃ i. i1 = i * i) ⊦ ∃ i1. j1 * i0 = i1 * i1

• Proof step 76:

  i * j1 * i = j0 * j0 * i0, gcd(j1 * i, j0) = 1, j1 ≠ 0, 0 < j1 * i, 0 < j1 * i0, 1 < j1 * i0, 0 < j0, prime(j1), 0 ≤ j0, j1 * j1 ≤ j1 * i0, ¬ j1 | j0 * j0 * i0, ¬ j1 | i0, ∀ i1, j, j0. i→n(i1) < i→n(j1 * i0) → j * j = i1 * j0 * j0 ∧ gcd(j, j0) = 1 ∧ 0 < j0 ∧ 0 < j ∧ 0 < i1 → (∃ i. i1 = i * i) ⊦ ∃ i1. j1 * i0 = i1 * i1

Rule argument

Additional information

Used formulas: j1 | j0 * j0 * i0

Proof step 70 from proof square-neq-any-pos-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  i * j1 * i = j0 * j0 * i0, gcd(j1 * i, j0) = 1, j1 ≠ 0, 0 < j0, 1 < j1 * i0, 0 < j1 * i0, 0 < j1 * i, prime(j1), j1 | j0 * j0, j1 * j1 ≤ j1 * i0, 0 ≤ j0, ¬ j1 | i0, ∀ i1, j, j0. i→n(i1) < i→n(j1 * i0) → j * j = i1 * j0 * j0 ∧ gcd(j, j0) = 1 ∧ 0 < j0 ∧ 0 < j ∧ 0 < i1 → (∃ i. i1 = i * i) ⊦ ∃ i1. j1 * i0 = i1 * i1

Rule argument

Additional information

Used simplifier rules: prime-divides: ⊦ prime(i) → (i | j * j0 ↔ i | j ∨ i | j0); commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult

Proof step 71 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

  ⊦ prime(i) → (i | j * j0 ↔ i | j ∨ i | j0)

• Proof step 73:

  i * j1 * i = j0 * j0 * i0, gcd(j1 * i, j0) = 1, j1 ≠ 0, 0 < j1 * i, 0 < j1 * i0, 1 < j1 * i0, 0 < j0, prime(j1), 0 ≤ j0, j1 * j1 ≤ j1 * i0, ¬ j1 | i0, j1 | j0 ∨ j1 | j0, ∀ i1, j, j0. i→n(i1) < i→n(j1 * i0) → j * j = i1 * j0 * j0 ∧ gcd(j, j0) = 1 ∧ 0 < j0 ∧ 0 < j ∧ 0 < i1 → (∃ i. i1 = i * i) ⊦ ∃ i1. j1 * i0 = i1 * i1

Rule argument

Additional information

Used terms: j0, j0, j1

Proof step 72 from proof square-neq-any-pos-02 (previous step) (back to tree)

Lemma prime-divides

Proof step 73 from proof square-neq-any-pos-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  i * j1 * i = j0 * j0 * i0, gcd(j1 * i, j0) = 1, j1 ≠ 0, 0 < j0, 1 < j1 * i0, 0 < j1 * i0, 0 < j1 * i, prime(j1), j1 | j0, j1 * j1 ≤ j1 * i0, 0 ≤ j0, ¬ j1 | i0, ∀ i1, j, j0. i→n(i1) < i→n(j1 * i0) → j * j = i1 * j0 * j0 ∧ gcd(j, j0) = 1 ∧ 0 < j0 ∧ 0 < j ∧ 0 < i1 → (∃ i. i1 = i * i) ⊦ ∃ i1. j1 * i0 = i1 * i1

Rule argument

Additional information

Proof step 74 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 75:

  ⊦ i | j ↔ (∃ i0. i * i0 = j)

Rule argument

Additional information

Used simplifier rules: gcd-mult: ⊦ gcd(i * i1, j * i1) = gcd(i, j) * abs(i1); prime-abs: ⊦ prime(j) → abs(j) = j; gcd-abs: ⊦ abs(gcd(i, j)) = gcd(i, j); prime-small: ⊦ j < 2 → ¬ prime(j); ⊦ i * j = 1 ↔ abs(i) = 1 ∧ i = j; (ws) ⊦ i ≠ 0 → (i * j = i * j0 ↔ j = j0); (s) forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs ⊦ 1 * i = i; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j0, j1

Proof step 75 from proof square-neq-any-pos-02 (previous step) (back to tree)

Lemma divides

Proof step 76 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: prime-divides: ⊦ prime(i) → (i | j * j0 ↔ i | j ∨ i | j0); div-mult: ⊦ i | i * j; associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult

Proof step 77 from proof square-neq-any-pos-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 78:

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

Rule argument

Additional information

Proof step 78 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 79:

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

Rule argument

Additional information

Used simplifier rules: prime-divides: ⊦ prime(i) → (i | j * j0 ↔ i | j ∨ i | j0); associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used formulas: j1 | j * j

Proof step 79 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: prime-divides: ⊦ prime(i) → (i | j * j0 ↔ i | j ∨ i | j0); div-same: ⊦ i | i; associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult

Proof step 80 from proof square-neq-any-pos-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 81:

  ∀ i0, j, j0. i→n(i0) < i→n(1) → j * j = i0 * j0 * j0 ∧ gcd(j, j0) = 1 ∧ 0 < j0 ∧ 0 < j ∧ 0 < i0 → (∃ i1. i0 = i1 * i1) ⊦ ∃ i0. 1 = i0 * i0

Rule argument

Additional information

Used simplifier rules: gcd-same-01: ⊦ 0 < j → gcd(j, j) = j; prime-small: ⊦ j < 2 → ¬ prime(j); 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) ⊦ i * i = j * j ↔ abs(i) = abs(j); (s) ⊦ i = 1 → i * j = j; (s) ⊦ 0 < i → (i ≤ 1 ↔ i = 1); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss)

Proof step 81 from proof square-neq-any-pos-02 (previous step) (back to tree)

User applied rule exists right

And closed the goal!

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 Used terms: 1