---

Step * of Lemma int-rat-mul_wf

∀[a:ℤ × ℕ+]. ∀[n:ℤ].  (int-rat-mul(n;a) ∈ {r:ℤ × ℕ+| ratreal(r) = n * ratreal(a)} )
BY
{ (Intros
   THEN Unhide
   THEN D 1
   THEN RepUR ``int-rat-mul`` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN MemTypeCD
   THEN Auto) }

1
.....set predicate..... 
1. a1 : ℤ
2. a2 : ℕ+
3. n : ℤ
⊢ ratreal(<n * a1, a2>) = n * ratreal(<a1, a2>)

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}].  \mforall{}[n:\mBbbZ{}].    (int-rat-mul(n;a)  \mmember{}  \{r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  ratreal(r)  =  n  *  ratreal(a)\}  )


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  D  1
  THEN  RepUR  ``int-rat-mul``  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index