---

Step * of Lemma ratmul_wf

∀[a,b:ℤ × ℕ+].  (ratmul(a;b) ∈ {r:ℤ × ℕ+| ratreal(r) = (ratreal(a) * ratreal(b))} )
BY
{ ((Intros THEN Unhide)
   THEN Unfold `ratmul` 0
   THEN (GenConclTerm ⌜rat-mul(a;b)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN DoSubsume
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Intros  THEN  Unhide)
  THEN  Unfold  `ratmul`  0
  THEN  (GenConclTerm  \mkleeneopen{}rat-mul(a;b)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  DoSubsume
  THEN  Auto)

---

Home Index