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