---

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

No Annotations
∀n:ℤ. ∀q:ℚ.  (((q * q) = n ∈ ℚ) ⇒ (∃m:ℤ. ((m * m) = n ∈ ℤ)))
BY
{ (Auto THEN Assert ⌜∃m:ℤ. ∃d:ℕ+. (((n * d * d) = (m * m) ∈ ℤ) ∧ CoPrime(m,d))⌝⋅) }

1
.....assertion..... 
1. n : ℤ
2. q : ℚ
3. (q * q) = n ∈ ℚ
⊢ ∃m:ℤ. ∃d:ℕ+. (((n * d * d) = (m * m) ∈ ℤ) ∧ CoPrime(m,d))

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\mBbbZ{}.  \mforall{}q:\mBbbQ{}.    (((q  *  q)  =  n)  {}\mRightarrow{}  (\mexists{}m:\mBbbZ{}.  ((m  *  m)  =  n)))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mexists{}m:\mBbbZ{}.  \mexists{}d:\mBbbN{}\msupplus{}.  (((n  *  d  *  d)  =  (m  *  m))  \mwedge{}  CoPrime(m,d))\mkleeneclose{}\mcdot{})

---

Home Index