---

Step * of Lemma rinv_functionality2

∀[x,y:ℝ].  (x ≠ r0 ⇒ (x = y) ⇒ (rinv(x) = rinv(y)))
BY
{ (Auto THEN RepeatFor 2 (Try ((RWO "4<" 0 THEN Auto)))) }

1
1. x : ℝ
2. y : ℝ
3. x ≠ r0@i
4. x = y@i
⊢ rnonzero(x)

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    (x  \mneq{}  r0  {}\mRightarrow{}  (x  =  y)  {}\mRightarrow{}  (rinv(x)  =  rinv(y)))


By

---

Latex:
(Auto  THEN  RepeatFor  2  (Try  ((RWO  "4<"  0  THEN  Auto))))

---

Home Index