---

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

∀a,b:ℤ.
  ((a * b) | (((a * a) + (b * b)) + 1)
  ⇐⇒ ∃n:ℕ. ((<|a|, |b|> = vexample(n;1;1) ∈ (ℤ × ℤ)) ∨ (<|b|, |a|> = vexample(n;1;1) ∈ (ℤ × ℤ))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (Assert (a * b) | (((a * a) + (b * b)) + 1) ⇐⇒ (|a| * |b|) | (((|a| * |a|) + (|b| * |b|)) + 1) BY
               ((RWO "absval_squared" 0 THENA Auto)
                THEN (RWO "absval_mul<" 0 THENA Auto)
                THEN RWO "absval-divides" 0
                THEN Auto))
   THEN (RWO  "-1" 0 THENA Auto)
   THEN Thin (-1)
   THEN Auto) }

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) ∈ (ℤ × ℤ)))

2
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)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.
    ((a  *  b)  |  (((a  *  a)  +  (b  *  b))  +  1)
    \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  ((<|a|,  |b|>  =  vexample(n;1;1))  \mvee{}  (<|b|,  |a|>  =  vexample(n;1;1))))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (Assert  (a  *  b)  |  (((a  *  a)  +  (b  *  b))  +  1)
                          \mLeftarrow{}{}\mRightarrow{}  (|a|  *  |b|)  |  (((|a|  *  |a|)  +  (|b|  *  |b|))  +  1)  BY
                          ((RWO  "absval\_squared"  0  THENA  Auto)
                            THEN  (RWO  "absval\_mul<"  0  THENA  Auto)
                            THEN  RWO  "absval-divides"  0
                            THEN  Auto))
  THEN  (RWO    "-1"  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Auto)

---

Home Index