---

Step * 1 1 of Lemma continuous-rneq


1. I : Interval@i
2. f : I ⟶ℝ@i
3. a : {x:ℝ| x ∈ I} @i
4. b : {x:ℝ| x ∈ I} @i
5. f[a] ≠ f[b]@i
6. k : ℕ+
7. (r1/r(k)) < |f[a] - f[b]|
8. n : ℕ+
9. (a ∈ i-approx(I;n)) ∧ (b ∈ i-approx(I;n))
10. d : ℝ@i
11. (r0 < d) ∧ (∀x,y:ℝ.  ((x ∈ i-approx(I;n)) ⇒ (y ∈ i-approx(I;n)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(k)))))
⊢ a ≠ b
BY
{ (Assert d ≤ |a - b| BY
         (BLemma `not-rless` THEN Auto THEN (D 0 THENA Auto) THEN (InstHyp [⌜a⌝;⌜b⌝] (-2)⋅ THEN Auto)⋅)) }

1
1. I : Interval@i
2. f : I ⟶ℝ@i
3. a : {x:ℝ| x ∈ I} @i
4. b : {x:ℝ| x ∈ I} @i
5. f[a] ≠ f[b]@i
6. k : ℕ+
7. (r1/r(k)) < |f[a] - f[b]|
8. n : ℕ+
9. (a ∈ i-approx(I;n)) ∧ (b ∈ i-approx(I;n))
10. d : ℝ@i
11. (r0 < d) ∧ (∀x,y:ℝ.  ((x ∈ i-approx(I;n)) ⇒ (y ∈ i-approx(I;n)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(k)))))
12. d ≤ |a - b|
⊢ a ≠ b

---

Latex:

---

Latex:

1.  I  :  Interval@i
2.  f  :  I  {}\mrightarrow{}\mBbbR{}@i
3.  a  :  \{x:\mBbbR{}|  x  \mmember{}  I\}  @i
4.  b  :  \{x:\mBbbR{}|  x  \mmember{}  I\}  @i
5.  f[a]  \mneq{}  f[b]@i
6.  k  :  \mBbbN{}\msupplus{}
7.  (r1/r(k))  <  |f[a]  -  f[b]|
8.  n  :  \mBbbN{}\msupplus{}
9.  (a  \mmember{}  i-approx(I;n))  \mwedge{}  (b  \mmember{}  i-approx(I;n))
10.  d  :  \mBbbR{}@i
11.  (r0  <  d)
\mwedge{}  (\mforall{}x,y:\mBbbR{}.
          ((x  \mmember{}  i-approx(I;n))  {}\mRightarrow{}  (y  \mmember{}  i-approx(I;n))  {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)  {}\mRightarrow{}  (|f[x]  -  f[y]|  \mleq{}  (r1/r(k)))))
\mvdash{}  a  \mneq{}  b


By

---

Latex:
(Assert  d  \mleq{}  |a  -  b|  BY
              (BLemma  `not-rless`
                THEN  Auto
                THEN  (D  0  THENA  Auto)
                THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)\mcdot{}))

---

Home Index