---

Step * of Lemma rnonzero_functionality

∀x,y:ℝ.  ((x = y) ⇒ (rnonzero(x) ⇐⇒ rnonzero(y)))
BY
{ (Assert ⌜∀x,y:ℝ.  ((x = y) ⇒ rnonzero(x) ⇒ rnonzero(y))⌝⋅ THENA Auto) }

1
1. x : ℝ
2. y : ℝ
3. x = y
4. rnonzero(x)
⊢ rnonzero(y)

2
1. ∀x,y:ℝ.  ((x = y) ⇒ rnonzero(x) ⇒ rnonzero(y))
⊢ ∀x,y:ℝ.  ((x = y) ⇒ (rnonzero(x) ⇐⇒ rnonzero(y)))

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (rnonzero(x)  \mLeftarrow{}{}\mRightarrow{}  rnonzero(y)))


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  rnonzero(x)  {}\mRightarrow{}  rnonzero(y))\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index