Step
*
of Lemma
int-has-rational-square-root
∀n:ℤ. (∃q:ℚ. ((q * q) = n ∈ ℚ) 
⇐⇒ ∃m:ℤ. ((m * m) = n ∈ ℤ))
BY
{ Auto }
1
1. n : ℤ@i
2. ∃q:ℚ. ((q * q) = n ∈ ℚ)@i
⊢ ∃m:ℤ. ((m * m) = n ∈ ℤ)
2
1. n : ℤ@i
2. ∃m:ℤ. ((m * m) = n ∈ ℤ)@i
⊢ ∃q:ℚ. ((q * q) = n ∈ ℚ)
Latex:
Latex:
\mforall{}n:\mBbbZ{}.  (\mexists{}q:\mBbbQ{}.  ((q  *  q)  =  n)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}m:\mBbbZ{}.  ((m  *  m)  =  n))
By
Latex:
Auto
Home
Index