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

.....assertion..... 
1. : ℤ
2. : ℚ
3. (q q) n ∈ ℚ
⊢ ∃m:ℤ. ∃d:ℕ+(((n d) (m m) ∈ ℤ) ∧ CoPrime(m,d))
BY
(InstLemma `equals-qrep` [⌜q⌝]⋅ THENA Auto)⋅ }

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


Latex:


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


By


Latex:
(InstLemma  `equals-qrep`  [\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  Auto)\mcdot{}




Home Index