---

Step * of Lemma rabs-rdiv

∀x,y:ℝ.  (y ≠ r0 ⇒ (|(x/y)| = (|x|/|y|)))
BY
{ ((Unfold `rdiv` 0 THEN Auto)
   THEN (Assert r0 < |y| BY
               (BLemma `rabs-neq-zero` THEN Auto))
   THEN RWW "rabs-rmul rabs-rinv" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    (y  \mneq{}  r0  {}\mRightarrow{}  (|(x/y)|  =  (|x|/|y|)))


By

---

Latex:
((Unfold  `rdiv`  0  THEN  Auto)
  THEN  (Assert  r0  <  |y|  BY
                          (BLemma  `rabs-neq-zero`  THEN  Auto))
  THEN  RWW  "rabs-rmul  rabs-rinv"  0
  THEN  Auto)

---

Home Index