---

Step * 1 1 1 1 2 1 1 2 of Lemma derivative-continuous


1. I : Interval@i
2. g : I ⟶ℝ@i
3. ∀x,y:{x:ℝ| x ∈ I} .  (g[x] ≠ g[y] ⇒ x ≠ y)@i
4. m : {m:ℕ+| icompact(i-approx(I;m))} @i
5. n : ℕ+@i
6. i-approx(I;m) ⊆ I 
7. del : ℝ
8. r0 < del
9. r0 < del
10. x : ℝ@i
11. y : ℝ@i
12. x ∈ i-approx(I;m)@i
13. y ∈ i-approx(I;m)@i
14. |x - y| ≤ del@i
15. (|g[x] - g[y]| * |x - y|) ≤ ((r1/r(n)) * |x - y|)
16. (r1/r(n)) < |g[x] - g[y]|@i
17. r0 < |x - y|
⊢ False
BY
{ (RepeatFor 3 (MoveToConcl (-1)) THEN GenConclTerms Auto [⌜|x - y|⌝;⌜|g[x] - g[y]|⌝]⋅ THEN All Thin) }

1
1. n : ℕ+@i
2. v : ℝ@i
3. v1 : ℝ@i
⊢ ((v1 * v) ≤ ((r1/r(n)) * v)) ⇒ ((r1/r(n)) < v1) ⇒ (r0 < v) ⇒ False

---

Latex:

---

Latex:

1.  I  :  Interval@i
2.  g  :  I  {}\mrightarrow{}\mBbbR{}@i
3.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    (g[x]  \mneq{}  g[y]  {}\mRightarrow{}  x  \mneq{}  y)@i
4.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\}  @i
5.  n  :  \mBbbN{}\msupplus{}@i
6.  i-approx(I;m)  \msubseteq{}  I 
7.  del  :  \mBbbR{}
8.  r0  <  del
9.  r0  <  del
10.  x  :  \mBbbR{}@i
11.  y  :  \mBbbR{}@i
12.  x  \mmember{}  i-approx(I;m)@i
13.  y  \mmember{}  i-approx(I;m)@i
14.  |x  -  y|  \mleq{}  del@i
15.  (|g[x]  -  g[y]|  *  |x  -  y|)  \mleq{}  ((r1/r(n))  *  |x  -  y|)
16.  (r1/r(n))  <  |g[x]  -  g[y]|@i
17.  r0  <  |x  -  y|
\mvdash{}  False


By

---

Latex:
(RepeatFor  3  (MoveToConcl  (-1))  THEN  GenConclTerms  Auto  [\mkleeneopen{}|x  -  y|\mkleeneclose{};\mkleeneopen{}|g[x]  -  g[y]|\mkleeneclose{}]\mcdot{}  THEN  All  Thin)

---

Home Index