---

Step * 1 1 of Lemma ratsub_wf

.....set predicate..... 
1. a : ℤ × ℕ+
2. b : ℤ × ℕ+
⊢ ratreal(ratadd(a;int-rat-mul(-1;b))) = (ratreal(a) - ratreal(b))
BY
{ (RWW  "ratreal-ratadd ratreal-int-rat-mul int-rmul-req" 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(RWW    "ratreal-ratadd  ratreal-int-rat-mul  int-rmul-req"  0  THEN  Auto)

---

Home Index