---

Step * 2 1 1 1 1 1 1 2 of Lemma intermediate-value-theorem


1. I : Interval
2. f : I ⟶ℝ
3. f[x] continuous for x ∈ I
4. a : ℝ
5. a ∈ I
6. b : ℝ
7. b ∈ I
8. f(a) < f(b)
9. y : ℝ
10. y ∈ [f(a), f(b)]
11. e : ℝ
12. r0 < e
13. b < a
14. icompact([b, a])
15. [b, a] ⊆ I 
16. mc : |f[x] - y| continuous for x ∈ [b, a]
17. r0 < inf{|f[x] - y||x ∈ [b, a]}
18. n : ℕ+
19. b ∈ i-approx(I;n)
20. a ∈ i-approx(I;n)
21. [b, a] ⊆ i-approx(I;n) 
22. k : ℕ+
23. (r1/r(k)) < inf{|f[x] - y||x ∈ [b, a]}
24. d : ℝ
25. r0 < d
26. ∀x,y:ℝ.  ((x ∈ i-approx(I;n)) ⇒ (y ∈ i-approx(I;n)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(k))))
27. p : partition([b, a])
28. partition-mesh([b, a];p) ≤ d
29. ∀i:ℕ||full-partition([b, a];p)|| - 1
      r0≤full-partition([b, a];p)[i + 1] - full-partition([b, a];p)[i]≤partition-mesh([b, a];p)
30. (∀x∈full-partition([b, a];p).x ∈ [b, a])
31. ∀i:ℕ. (i < ||full-partition([b, a];p)|| ⇒ (full-partition([b, a];p)[i] ∈ {x:ℝ| x ∈ I} ))
32. ∀i:ℕ. (i < ||full-partition([b, a];p)|| ⇒ (y ≤ f[full-partition([b, a];p)[i]]))
⊢ False
BY
{ (Assert y ≤ f[a] BY
         (RepUR ``full-partition`` -1
          THEN (InstHyp [⌜||p @ [right-endpoint([b, a])]||⌝] (-1)⋅ THENA Auto)
          THEN Reduce (-1)
          THEN NthHypSq (-1)
          THEN RepeatFor 2 (EqCD)
          THEN Try (Trivial)
          THEN ((RWO "length-append" 0 THENM Reduce 0) THENA Auto)
          THEN (RWW "select-cons select-append" 0 THENA Auto)
          THEN Repeat (AutoSplit)
          THEN Auto'
          THEN RepUR ``right-endpoint endpoints`` 0
          THEN Auto))⋅ }

1
1. I : Interval
2. f : I ⟶ℝ
3. f[x] continuous for x ∈ I
4. a : ℝ
5. a ∈ I
6. b : ℝ
7. b ∈ I
8. f(a) < f(b)
9. y : ℝ
10. y ∈ [f(a), f(b)]
11. e : ℝ
12. r0 < e
13. b < a
14. icompact([b, a])
15. [b, a] ⊆ I 
16. mc : |f[x] - y| continuous for x ∈ [b, a]
17. r0 < inf{|f[x] - y||x ∈ [b, a]}
18. n : ℕ+
19. b ∈ i-approx(I;n)
20. a ∈ i-approx(I;n)
21. [b, a] ⊆ i-approx(I;n) 
22. k : ℕ+
23. (r1/r(k)) < inf{|f[x] - y||x ∈ [b, a]}
24. d : ℝ
25. r0 < d
26. ∀x,y:ℝ.  ((x ∈ i-approx(I;n)) ⇒ (y ∈ i-approx(I;n)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(k))))
27. p : partition([b, a])
28. partition-mesh([b, a];p) ≤ d
29. ∀i:ℕ||full-partition([b, a];p)|| - 1
      r0≤full-partition([b, a];p)[i + 1] - full-partition([b, a];p)[i]≤partition-mesh([b, a];p)
30. (∀x∈full-partition([b, a];p).x ∈ [b, a])
31. ∀i:ℕ. (i < ||full-partition([b, a];p)|| ⇒ (full-partition([b, a];p)[i] ∈ {x:ℝ| x ∈ I} ))
32. ∀i:ℕ. (i < ||full-partition([b, a];p)|| ⇒ (y ≤ f[full-partition([b, a];p)[i]]))
33. y ≤ f[a]
⊢ False

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  f[x]  continuous  for  x  \mmember{}  I
4.  a  :  \mBbbR{}
5.  a  \mmember{}  I
6.  b  :  \mBbbR{}
7.  b  \mmember{}  I
8.  f(a)  <  f(b)
9.  y  :  \mBbbR{}
10.  y  \mmember{}  [f(a),  f(b)]
11.  e  :  \mBbbR{}
12.  r0  <  e
13.  b  <  a
14.  icompact([b,  a])
15.  [b,  a]  \msubseteq{}  I 
16.  mc  :  |f[x]  -  y|  continuous  for  x  \mmember{}  [b,  a]
17.  r0  <  inf\{|f[x]  -  y||x  \mmember{}  [b,  a]\}
18.  n  :  \mBbbN{}\msupplus{}
19.  b  \mmember{}  i-approx(I;n)
20.  a  \mmember{}  i-approx(I;n)
21.  [b,  a]  \msubseteq{}  i-approx(I;n) 
22.  k  :  \mBbbN{}\msupplus{}
23.  (r1/r(k))  <  inf\{|f[x]  -  y||x  \mmember{}  [b,  a]\}
24.  d  :  \mBbbR{}
25.  r0  <  d
26.  \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))))
27.  p  :  partition([b,  a])
28.  partition-mesh([b,  a];p)  \mleq{}  d
29.  \mforall{}i:\mBbbN{}||full-partition([b,  a];p)||  -  1
            r0\mleq{}full-partition([b,  a];p)[i  +  1]  -  full-partition([b,  a];p)[i]\mleq{}partition-mesh([b,  a];p)
30.  (\mforall{}x\mmember{}full-partition([b,  a];p).x  \mmember{}  [b,  a])
31.  \mforall{}i:\mBbbN{}.  (i  <  ||full-partition([b,  a];p)||  {}\mRightarrow{}  (full-partition([b,  a];p)[i]  \mmember{}  \{x:\mBbbR{}|  x  \mmember{}  I\}  ))
32.  \mforall{}i:\mBbbN{}.  (i  <  ||full-partition([b,  a];p)||  {}\mRightarrow{}  (y  \mleq{}  f[full-partition([b,  a];p)[i]]))
\mvdash{}  False


By

---

Latex:
(Assert  y  \mleq{}  f[a]  BY
              (RepUR  ``full-partition``  -1
                THEN  (InstHyp  [\mkleeneopen{}||p  @  [right-endpoint([b,  a])]||\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                THEN  Reduce  (-1)
                THEN  NthHypSq  (-1)
                THEN  RepeatFor  2  (EqCD)
                THEN  Try  (Trivial)
                THEN  ((RWO  "length-append"  0  THENM  Reduce  0)  THENA  Auto)
                THEN  (RWW  "select-cons  select-append"  0  THENA  Auto)
                THEN  Repeat  (AutoSplit)
                THEN  Auto'
                THEN  RepUR  ``right-endpoint  endpoints``  0
                THEN  Auto))\mcdot{}

---

Home Index