---

Step * 1 of Lemma rsqrt2-repels-rationals

.....assertion..... 
1. n : ℕ+
2. m : ℤ
⊢ (|(r(n) * rsqrt(r(2))) - r(m)| * |(r(n) * rsqrt(r(2))) + r(m)|) = |r((2 * n * n) - m * m)|
BY
{ ((RWO "rabs-rmul<" 0 THENM nRNorm 0 THENM RWW "rsqrt_squared" 0 THENM nRNorm 0) THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  n  :  \mBbbN{}\msupplus{}
2.  m  :  \mBbbZ{}
\mvdash{}  (|(r(n)  *  rsqrt(r(2)))  -  r(m)|  *  |(r(n)  *  rsqrt(r(2)))  +  r(m)|)  =  |r((2  *  n  *  n)  -  m  *  m)|


By

---

Latex:
((RWO  "rabs-rmul<"  0  THENM  nRNorm  0  THENM  RWW  "rsqrt\_squared"  0  THENM  nRNorm  0)  THEN  Auto)

---

Home Index