---

Step * of Lemma rat-nat-div_wf

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

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

---

Latex:

---

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


By

---

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

---

Home Index