---

Step * of Lemma rsqrt_2-irrational

irrational(rsqrt(r(2)))
BY
{ ((InstLemma `rsqrt-irrational` [⌜2⌝]⋅ THENM D -1) THEN Auto) }

1
1. ∃m:ℕ2 + 1. ((m * m) = 2 ∈ ℤ)
⊢ irrational(rsqrt(r(2)))

---

Latex:

---

Latex:
irrational(rsqrt(r(2)))


By

---

Latex:
((InstLemma  `rsqrt-irrational`  [\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENM  D  -1)  THEN  Auto)

---

Home Index