---

Step * of Lemma rat-mul_wf

∀[a,b:ℤ × ℕ+].  (rat-mul(a;b) ∈ {r:ℤ × ℕ+| ratreal(r) = (ratreal(a) * ratreal(b))} )
BY
{ (Intros
   THEN Unhide
   THEN D 1
   THEN D -1
   THEN (Unfold `rat-mul` 0 THEN Reduce 0)
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN (MemTypeCD THEN Auto)
   THEN (RWO "ratreal-req" 0 THENA Auto)
   THEN Symmetry
   THEN Try (BLemma `rmul-int-fractions`)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}].    (rat-mul(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  `rat-mul`  0  THEN  Reduce  0)
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  (MemTypeCD  THEN  Auto)
  THEN  (RWO  "ratreal-req"  0  THENA  Auto)
  THEN  Symmetry
  THEN  Try  (BLemma  `rmul-int-fractions`)
  THEN  Auto)

---

Home Index