---

Step * 1 of Lemma ab-divides-a^2+b^2+1


1. a : ℤ
2. b : ℤ
3. (|a| * |b|) | (((|a| * |a|) + (|b| * |b|)) + 1)
⊢ ∃n:ℕ. ((<|a|, |b|> = vexample(n;1;1) ∈ (ℤ × ℤ)) ∨ (<|b|, |a|> = vexample(n;1;1) ∈ (ℤ × ℤ)))
BY
{ (D -1 THEN (InstLemma `Vieta-jumping-example2-corollary` [⌜c⌝]⋅ THENA Auto) THEN (Decide ⌜|a| ≤ |b|⌝⋅ THENA Auto)) }

1
1. a : ℤ
2. b : ℤ
3. c : ℤ
4. (((|a| * |a|) + (|b| * |b|)) + 1) = ((|a| * |b|) * c) ∈ ℤ
5. ∀a,b:ℕ.  (((((a * a) + (b * b)) + 1) = (c * a * b) ∈ ℤ) ⇒ (a ≤ b) ⇒ (∃n:ℕ. (<a, b> = vexample(n;1;1) ∈ (ℤ × ℤ))))
6. |a| ≤ |b|
⊢ ∃n:ℕ. ((<|a|, |b|> = vexample(n;1;1) ∈ (ℤ × ℤ)) ∨ (<|b|, |a|> = vexample(n;1;1) ∈ (ℤ × ℤ)))

2
1. a : ℤ
2. b : ℤ
3. c : ℤ
4. (((|a| * |a|) + (|b| * |b|)) + 1) = ((|a| * |b|) * c) ∈ ℤ
5. ∀a,b:ℕ.  (((((a * a) + (b * b)) + 1) = (c * a * b) ∈ ℤ) ⇒ (a ≤ b) ⇒ (∃n:ℕ. (<a, b> = vexample(n;1;1) ∈ (ℤ × ℤ))))
6. ¬(|a| ≤ |b|)
⊢ ∃n:ℕ. ((<|a|, |b|> = vexample(n;1;1) ∈ (ℤ × ℤ)) ∨ (<|b|, |a|> = vexample(n;1;1) ∈ (ℤ × ℤ)))

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  (|a|  *  |b|)  |  (((|a|  *  |a|)  +  (|b|  *  |b|))  +  1)
\mvdash{}  \mexists{}n:\mBbbN{}.  ((<|a|,  |b|>  =  vexample(n;1;1))  \mvee{}  (<|b|,  |a|>  =  vexample(n;1;1)))


By

---

Latex:
(D  -1
  THEN  (InstLemma  `Vieta-jumping-example2-corollary`  [\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Decide  \mkleeneopen{}|a|  \mleq{}  |b|\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index