---

Step * of Lemma ratadd_wf

∀[a,b:ℤ × ℕ+].  (ratadd(a;b) ∈ {r:ℤ × ℕ+| ratreal(r) = (ratreal(a) + ratreal(b))} )
BY
{ (Intros
   THEN Unhide
   THEN D 1
   THEN D -1
   THEN (Unfold `ratadd` 0 THEN Reduce 0)
   THEN (RWO "better-gcd-gcd" 0 THENA Auto)
   THEN (InstLemma `gcd-properties` [⌜a2⌝;⌜b2⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl⌜gcd(a2;b2) = g ∈ ℤ⌝⋅ THENA Auto)
   THEN (D 0 THENA Auto)
   THEN ExRepD
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (InstLemma `gcd-positive` [⌜b2⌝;⌜a2⌝]⋅ THENA Auto)
   THEN (Subst' a2 ÷ g ~ c 0 THENA (Auto THEN RWO "8<" 0 THEN Auto))
   THEN (Subst' b2 ÷ g ~ d 0 THENA (Auto THEN RWO "10<" 0 THEN Auto))
   THEN RepeatFor 4 ((CallByValueReduce 0 THENA Auto))
   THEN ((Assert 0 < c * g BY Auto) THEN (RWO  "mul_positive_iff" (-1) ⋅ THENA Auto))
   THEN D -1
   THEN Auto) }

1
1. a1 : ℤ
2. a2 : ℕ+
3. b1 : ℤ
4. b2 : ℕ+
5. g : ℤ
6. gcd(a2;b2) = g ∈ ℤ
7. c : ℤ
8. (c * g) = a2 ∈ ℤ
9. d : ℤ
10. (d * g) = b2 ∈ ℤ
11. s : ℤ
12. t : ℤ
13. g = ((s * a2) + (t * b2)) ∈ ℤ
14. 0 < gcd(a2;b2)
15. 0 < c
16. 0 < g
⊢ <(d * a1) + (c * b1), c * b2> ∈ {r:ℤ × ℕ+| ratreal(r) = (ratreal(<a1, a2>) + ratreal(<b1, b2>))} 

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}].    (ratadd(a;b)  \mmember{}  \{r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  ratreal(r)  =  (ratreal(a)  +  ratreal(b))\}  )


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  D  1
  THEN  D  -1
  THEN  (Unfold  `ratadd`  0  THEN  Reduce  0)
  THEN  (RWO  "better-gcd-gcd"  0  THENA  Auto)
  THEN  (InstLemma  `gcd-properties`  [\mkleeneopen{}a2\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl\mkleeneopen{}gcd(a2;b2)  =  g\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  ExRepD
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (InstLemma  `gcd-positive`  [\mkleeneopen{}b2\mkleeneclose{};\mkleeneopen{}a2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Subst'  a2  \mdiv{}  g  \msim{}  c  0  THENA  (Auto  THEN  RWO  "8<"  0  THEN  Auto))
  THEN  (Subst'  b2  \mdiv{}  g  \msim{}  d  0  THENA  (Auto  THEN  RWO  "10<"  0  THEN  Auto))
  THEN  RepeatFor  4  ((CallByValueReduce  0  THENA  Auto))
  THEN  ((Assert  0  <  c  *  g  BY  Auto)  THEN  (RWO    "mul\_positive\_iff"  (-1)  \mcdot{}  THENA  Auto))
  THEN  D  -1
  THEN  Auto)

---

Home Index