---

Step * of Lemma ratsub_wf

∀[a,b:ℤ × ℕ+].  (ratsub(a;b) ∈ {r:ℤ × ℕ+| ratreal(r) = (ratreal(a) - ratreal(b))} )
BY
{ ProveWfLemma }

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

---

Latex:

---

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


By

---

Latex:
ProveWfLemma

---

Home Index