---

Step * 1 1 1 1 1 1 1 of Lemma extensional-discrete-real-fun-is-constant


1. v : ℤ
2. |r(v)| ≤ (r1/r(2))
⊢ v = 0 ∈ ℤ
BY
{ nRMul ⌜r(2)⌝ (-1)⋅ }

1
1. v : ℤ
2. r(2 * |v|) ≤ r1
⊢ v = 0 ∈ ℤ

---

Latex:

---

Latex:

1.  v  :  \mBbbZ{}
2.  |r(v)|  \mleq{}  (r1/r(2))
\mvdash{}  v  =  0


By

---

Latex:
nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  (-1)\mcdot{}

---

Home Index