---

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