---

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


1. a : ℤ
2. b : ℤ
3. ∃n:ℕ. ((<|a|, |b|> = vexample(n;1;1) ∈ (ℤ × ℤ)) ∨ (<|b|, |a|> = vexample(n;1;1) ∈ (ℤ × ℤ)))
⊢ (|a| * |b|) | (((|a| * |a|) + (|b| * |b|)) + 1)
BY
{ ((D 0 With ⌜3⌝  THENA Auto)
   THEN ExRepD
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜vexample(n;1;1)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN EqHD (-1)
   THEN All Reduce
   THEN Auto
   THEN RWO "-1 -2" 0
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((D  0  With  \mkleeneopen{}3\mkleeneclose{}    THENA  Auto)
  THEN  ExRepD
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}vexample(n;1;1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  EqHD  (-1)
  THEN  All  Reduce
  THEN  Auto
  THEN  RWO  "-1  -2"  0
  THEN  Auto)

---

Home Index