---

Step * 1 of Lemma int-has-rational-square-root


1. n : ℤ@i
2. ∃q:ℚ. ((q * q) = n ∈ ℚ)@i
⊢ ∃m:ℤ. ((m * m) = n ∈ ℤ)
BY
{ (D (-1) THEN InstLemma `int-with-rational-square-root` [⌜n⌝;⌜q⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}@i
2.  \mexists{}q:\mBbbQ{}.  ((q  *  q)  =  n)@i
\mvdash{}  \mexists{}m:\mBbbZ{}.  ((m  *  m)  =  n)


By

---

Latex:
(D  (-1)  THEN  InstLemma  `int-with-rational-square-root`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index