---

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


1. v : ℤ
⊢ (|r(v)| ≤ (r1/r(2))) ⇒ (v = 0 ∈ ℤ)
BY
{ Auto }

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

---

Latex:

---

Latex:

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


By

---

Latex:
Auto

---

Home Index