---

Step * of Lemma rnonzero-iff

∀x:ℝ. (rnonzero(x) ⇐⇒ x ≠ r0)
BY
{ (RepUR ``rnonzero rneq rless int-to-real`` 0
   THEN Auto
   THEN D -1
   THEN Try ((D -1 THEN With ⌜n⌝ (D 0)⋅ THEN Auto))
   THEN RWW "absval_unfold" 0
   THEN Auto) }

1
1. x : ℝ
2. n : ℕ+
3. 4 < |x n|
⊢ (∃n:{ℕ+| (x n) + 4 < 2 * n * 0}) ∨ (∃n:{ℕ+| (2 * n * 0) + 4 < x n})

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  (rnonzero(x)  \mLeftarrow{}{}\mRightarrow{}  x  \mneq{}  r0)


By

---

Latex:
(RepUR  ``rnonzero  rneq  rless  int-to-real``  0
  THEN  Auto
  THEN  D  -1
  THEN  Try  ((D  -1  THEN  With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
  THEN  RWW  "absval\_unfold"  0
  THEN  Auto)

---

Home Index