---

Step * of Lemma ratreduce_wf

∀[x:ℤ × ℕ+]. (ratreduce(x) ∈ {y:ℤ × ℕ+| ratreal(x) = ratreal(y)} )
BY
{ (Intro
   THEN Unhide
   THEN D 1
   THEN RepUR ``ratreduce`` 0
   THEN (RWO "better-gcd-gcd" 0 THENA Auto)
   THEN (Assert (|gcd(x1;x2)| | x1) ∧ (|gcd(x1;x2)| | x2) BY
               (RWO "absval-divides" 0 THEN Auto))
   THEN MoveToConcl (-1)
   THEN (Assert 0 < |gcd(x1;x2)| BY
               (RWO "absval-positive" 0 THEN Auto THEN BLemma  `gcd-non-zero` THEN Auto))
   THEN MoveToConcl (-1)
   THEN (GenConcl⌜gcd(x1;x2) = g ∈ ℤ⌝⋅ THENA Auto)
   THEN Unfold `divides` 0
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN ExRepD
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (Subst' x1 ÷ |g| ~ c1 0 THENA (Auto THEN RWO "7" 0 THEN Auto))
   THEN (Subst' x2 ÷ |g| ~ c 0 THENA (Auto THEN RWO "9" 0 THEN Auto))
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN (Assert c ∈ ℕ+ BY
               (MemTypeCD
                THEN Auto
                THEN (Assert 0 < c * |g| BY
                            Auto)
                THEN (RWO  "mul_positive_iff" (-1) ⋅ THENA Auto)
                THEN D -1
                THEN Auto))) }

1
1. x1 : ℤ
2. x2 : ℕ+
3. g : ℤ
4. gcd(x1;x2) = g ∈ ℤ
5. 0 < |g|
6. c1 : ℤ
7. x1 = (|g| * c1) ∈ ℤ
8. c : ℤ
9. x2 = (|g| * c) ∈ ℤ
10. c ∈ ℕ+
⊢ <c1, c> ∈ {y:ℤ × ℕ+| ratreal(<x1, x2>) = ratreal(y)} 

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}].  (ratreduce(x)  \mmember{}  \{y:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  ratreal(x)  =  ratreal(y)\}  )


By

---

Latex:
(Intro
  THEN  Unhide
  THEN  D  1
  THEN  RepUR  ``ratreduce``  0
  THEN  (RWO  "better-gcd-gcd"  0  THENA  Auto)
  THEN  (Assert  (|gcd(x1;x2)|  |  x1)  \mwedge{}  (|gcd(x1;x2)|  |  x2)  BY
                          (RWO  "absval-divides"  0  THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  (Assert  0  <  |gcd(x1;x2)|  BY
                          (RWO  "absval-positive"  0  THEN  Auto  THEN  BLemma    `gcd-non-zero`  THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl\mkleeneopen{}gcd(x1;x2)  =  g\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Unfold  `divides`  0
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  ExRepD
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (Subst'  x1  \mdiv{}  |g|  \msim{}  c1  0  THENA  (Auto  THEN  RWO  "7"  0  THEN  Auto))
  THEN  (Subst'  x2  \mdiv{}  |g|  \msim{}  c  0  THENA  (Auto  THEN  RWO  "9"  0  THEN  Auto))
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  (Assert  c  \mmember{}  \mBbbN{}\msupplus{}  BY
                          (MemTypeCD
                            THEN  Auto
                            THEN  (Assert  0  <  c  *  |g|  BY
                                                    Auto)
                            THEN  (RWO    "mul\_positive\_iff"  (-1)  \mcdot{}  THENA  Auto)
                            THEN  D  -1
                            THEN  Auto)))

---

Home Index