---

Step * of Lemma clear-denominator1

∀[a,b,c,d:ℝ].  uiff(((a/b) * c) = d;(c * a) = (d * b)) supposing b ≠ r0
BY
{ Auto }

1
1. a : ℝ
2. b : ℝ
3. c : ℝ
4. d : ℝ
5. b ≠ r0
6. ((a/b) * c) = d
⊢ (c * a) = (d * b)

2
1. a : ℝ
2. b : ℝ
3. c : ℝ
4. d : ℝ
5. b ≠ r0
6. (c * a) = (d * b)
⊢ ((a/b) * c) = d

---

Latex:

---

Latex:
\mforall{}[a,b,c,d:\mBbbR{}].    uiff(((a/b)  *  c)  =  d;(c  *  a)  =  (d  *  b))  supposing  b  \mneq{}  r0


By

---

Latex:
Auto

---

Home Index