Step * 1 of Lemma rsqrt2-repels-rationals

.....assertion..... 
1. : ℕ+
2. : ℤ
⊢ (|(r(n) rsqrt(r(2))) r(m)| |(r(n) rsqrt(r(2))) r(m)|) |r((2 n) m)|
BY
((RWO "rabs-rmul<THENM nRNorm THENM RWW "rsqrt_squared" 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