---

Step * of Lemma int-rdiv-int-rdiv

∀[k,j:ℤ-o]. ∀[x:ℝ].  (((x)/k)/j = (x)/j * k)
BY
{ (Auto THEN RWO "int-rdiv-req" 0 THEN Auto) }

1
1. k : ℤ-o
2. j : ℤ-o
3. x : ℝ
⊢ ((x)/k/r(j)) = (x/r(j * k))

---

Latex:

---

Latex:
\mforall{}[k,j:\mBbbZ{}\msupminus{}\msupzero{}].  \mforall{}[x:\mBbbR{}].    (((x)/k)/j  =  (x)/j  *  k)


By

---

Latex:
(Auto  THEN  RWO  "int-rdiv-req"  0  THEN  Auto)

---

Home Index