---

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


1. n : ℤ
2. q : ℚ
3. (q * q) = n ∈ ℚ
4. qrep(q) = q ∈ ℚ
5. |gcd(fst(qrep(q));snd(qrep(q)))| = 1 ∈ ℤ
⊢ ∃m:ℤ. ∃d:ℕ+. (((n * d * d) = (m * m) ∈ ℤ) ∧ CoPrime(m,d))
BY
{ (Assert (qrep(q) * qrep(q)) = n ∈ ℚ BY
         Auto) }

1
1. n : ℤ
2. q : ℚ
3. (q * q) = n ∈ ℚ
4. qrep(q) = q ∈ ℚ
5. |gcd(fst(qrep(q));snd(qrep(q)))| = 1 ∈ ℤ
6. (qrep(q) * qrep(q)) = n ∈ ℚ
⊢ ∃m:ℤ. ∃d:ℕ+. (((n * d * d) = (m * m) ∈ ℤ) ∧ CoPrime(m,d))

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  q  :  \mBbbQ{}
3.  (q  *  q)  =  n
4.  qrep(q)  =  q
5.  |gcd(fst(qrep(q));snd(qrep(q)))|  =  1
\mvdash{}  \mexists{}m:\mBbbZ{}.  \mexists{}d:\mBbbN{}\msupplus{}.  (((n  *  d  *  d)  =  (m  *  m))  \mwedge{}  CoPrime(m,d))


By

---

Latex:
(Assert  (qrep(q)  *  qrep(q))  =  n  BY
              Auto)

---

Home Index