---

Step * 1 of Lemma rsqrt_2-irrational


1. ∃m:ℕ2 + 1. ((m * m) = 2 ∈ ℤ)
⊢ irrational(rsqrt(r(2)))
BY
{ (D (-1) THEN Reduce 1 THEN IntSegCases 1 THEN HypSubst' (-1) (2) THEN Auto') }

---

Latex:

---

Latex:

1.  \mexists{}m:\mBbbN{}2  +  1.  ((m  *  m)  =  2)
\mvdash{}  irrational(rsqrt(r(2)))


By

---

Latex:
(D  (-1)  THEN  Reduce  1  THEN  IntSegCases  1  THEN  HypSubst'  (-1)  (2)  THEN  Auto')

---

Home Index