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


1. : ℤ
2. : ℚ
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) (m m) ∈ ℤ) ∧ CoPrime(m,d))
BY
(RepeatFor (MoveToConcl (-1)) THEN GenConclAtAddr [2;1;2;1] THEN ThinVar `q' THEN -1 THEN Reduce 0) }

1
1. : ℤ
2. v1 : ℤ
3. v2 : ℕ+
⊢ (|gcd(v1;v2)| 1 ∈ ℤ ((<v1, v2> * <v1, v2>n ∈ ℚ (∃m:ℤ. ∃d:ℕ+(((n d) (m m) ∈ ℤ) ∧ CoPrime(m,d)\000C))


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
6.  (qrep(q)  *  qrep(q))  =  n
\mvdash{}  \mexists{}m:\mBbbZ{}.  \mexists{}d:\mBbbN{}\msupplus{}.  (((n  *  d  *  d)  =  (m  *  m))  \mwedge{}  CoPrime(m,d))


By


Latex:
(RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclAtAddr  [2;1;2;1]
  THEN  ThinVar  `q'
  THEN  D  -1
  THEN  Reduce  0)




Home Index