---

Step * of Lemma rabs-rinv

∀y:ℝ. (y ≠ r0 ⇒ (|rinv(y)| = rinv(|y|)))
BY
{ (Auto THEN (Assert r0 < |y| BY (BLemma `rabs-neq-zero` THEN Auto)) THEN DupHyp (-2) THEN D -1) }

1
1. y : ℝ
2. y ≠ r0
3. r0 < |y|
4. y < r0
⊢ |rinv(y)| = rinv(|y|)

2
1. y : ℝ
2. y ≠ r0
3. r0 < |y|
4. r0 < y
⊢ |rinv(y)| = rinv(|y|)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (Assert  r0  <  |y|  BY  (BLemma  `rabs-neq-zero`  THEN  Auto))  THEN  DupHyp  (-2)  THEN  D  -1)

---

Home Index