Step
*
1
1
of Lemma
int-with-rational-square-root
1. n : ℤ
2. q : ℚ
3. (q * q) = n ∈ ℚ
4. qrep(q) = q ∈ ℚ
⊢ ∃m:ℤ. ∃d:ℕ+. (((n * d * d) = (m * m) ∈ ℤ) ∧ CoPrime(m,d))
BY
{ (InstLemma `qrep-coprime` [⌜q⌝]⋅ THENA Auto) }
1
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))
Latex:
Latex:
1. n : \mBbbZ{}
2. q : \mBbbQ{}
3. (q * q) = n
4. qrep(q) = q
\mvdash{} \mexists{}m:\mBbbZ{}. \mexists{}d:\mBbbN{}\msupplus{}. (((n * d * d) = (m * m)) \mwedge{} CoPrime(m,d))
By
Latex:
(InstLemma `qrep-coprime` [\mkleeneopen{}q\mkleeneclose{}]\mcdot{} THENA Auto)
Home
Index