---

Step * of Lemma rmul_preserves_req

∀[x,y,z:ℝ].  uiff(x = z;(x * y) = (z * y)) supposing y ≠ r0
BY
{ Auto }

1
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. y ≠ r0
5. (x * y) = (z * y)
⊢ x = z

---

Latex:

---

Latex:
\mforall{}[x,y,z:\mBbbR{}].    uiff(x  =  z;(x  *  y)  =  (z  *  y))  supposing  y  \mneq{}  r0


By

---

Latex:
Auto

---

Home Index