---

Step * 2 of Lemma int-with-rational-square-root


1. n : ℤ
2. q : ℚ
3. (q * q) = n ∈ ℚ
4. ∃m:ℤ. ∃d:ℕ+. (((n * d * d) = (m * m) ∈ ℤ) ∧ CoPrime(m,d))
⊢ ∃m:ℤ. ((m * m) = n ∈ ℤ)
BY
{ ExRepD }

1
1. n : ℤ
2. q : ℚ
3. (q * q) = n ∈ ℚ
4. m : ℤ
5. d : ℕ+
6. (n * d * d) = (m * m) ∈ ℤ
7. CoPrime(m,d)
⊢ ∃m:ℤ. ((m * m) = n ∈ ℤ)

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  q  :  \mBbbQ{}
3.  (q  *  q)  =  n
4.  \mexists{}m:\mBbbZ{}.  \mexists{}d:\mBbbN{}\msupplus{}.  (((n  *  d  *  d)  =  (m  *  m))  \mwedge{}  CoPrime(m,d))
\mvdash{}  \mexists{}m:\mBbbZ{}.  ((m  *  m)  =  n)


By

---

Latex:
ExRepD

---

Home Index