---

Step * 1 of Lemma ratsub_wf


1. a : ℤ × ℕ+
2. b : ℤ × ℕ+
⊢ ratadd(a;int-rat-mul(-1;b)) ∈ {r:ℤ × ℕ+| ratreal(r) = (ratreal(a) - ratreal(b))} 
BY
{ (MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. a : ℤ × ℕ+
2. b : ℤ × ℕ+
⊢ ratreal(ratadd(a;int-rat-mul(-1;b))) = (ratreal(a) - ratreal(b))

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
2.  b  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
\mvdash{}  ratadd(a;int-rat-mul(-1;b))  \mmember{}  \{r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  ratreal(r)  =  (ratreal(a)  -  ratreal(b))\} 


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index