---

Step * of Lemma rsqrt2-repels-rationals

∀n:ℕ+. ∀m:ℤ.  ((r1/r(3 * n * n)) ≤ |rsqrt(r(2)) - (r(m)/r(n))|)
BY
{ (Auto THEN Assert ⌜(|(r(n) * rsqrt(r(2))) - r(m)| * |(r(n) * rsqrt(r(2))) + r(m)|) = |r((2 * n * n) - m * m)|⌝⋅) }

1
.....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)|

2
1. n : ℕ+
2. m : ℤ
3. (|(r(n) * rsqrt(r(2))) - r(m)| * |(r(n) * rsqrt(r(2))) + r(m)|) = |r((2 * n * n) - m * m)|
⊢ (r1/r(3 * n * n)) ≤ |rsqrt(r(2)) - (r(m)/r(n))|

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}m:\mBbbZ{}.    ((r1/r(3  *  n  *  n))  \mleq{}  |rsqrt(r(2))  -  (r(m)/r(n))|)


By

---

Latex:
(Auto
  THEN  Assert  \mkleeneopen{}(|(r(n)  *  rsqrt(r(2)))  -  r(m)|  *  |(r(n)  *  rsqrt(r(2)))  +  r(m)|)
                            =  |r((2  *  n  *  n)  -  m  *  m)|\mkleeneclose{}\mcdot{}
  )

---

Home Index