---

Step * 1 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. a < b
14. icompact([a, b])
15. [a, b] ⊆ I 
16. mc : |f[x] - y| continuous for x ∈ [a, b]
17. r0 < inf{|f[x] - y||x ∈ [a, b]}
18. n : ℕ+
19. a ∈ i-approx(I;n)
20. b ∈ i-approx(I;n)
21. [a, b] ⊆ i-approx(I;n) 
22. k : ℕ+
23. (r1/r(k)) < inf{|f[x] - y||x ∈ [a, b]}
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([a, b])
28. partition-mesh([a, b];p) ≤ d
29. ∀i:ℕ||full-partition([a, b];p)|| - 1
      r0≤full-partition([a, b];p)[i + 1] - full-partition([a, b];p)[i]≤partition-mesh([a, b];p)
30. (∀x∈full-partition([a, b];p).x ∈ [a, b])
31. ∀i:ℕ. (i < ||full-partition([a, b];p)|| ⇒ (full-partition([a, b];p)[i] ∈ {x:ℝ| x ∈ I} ))
32. ∀i:ℕ. (i < ||full-partition([a, b];p)|| ⇒ (f[full-partition([a, b];p)[i]] ≤ y))
⊢ False
BY
{ (Assert f[b] ≤ y BY
         (RepUR ``full-partition`` -1
          THEN (InstHyp [⌜||p @ [right-endpoint([a, b])]||⌝] (-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. a < b
14. icompact([a, b])
15. [a, b] ⊆ I 
16. mc : |f[x] - y| continuous for x ∈ [a, b]
17. r0 < inf{|f[x] - y||x ∈ [a, b]}
18. n : ℕ+
19. a ∈ i-approx(I;n)
20. b ∈ i-approx(I;n)
21. [a, b] ⊆ i-approx(I;n) 
22. k : ℕ+
23. (r1/r(k)) < inf{|f[x] - y||x ∈ [a, b]}
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([a, b])
28. partition-mesh([a, b];p) ≤ d
29. ∀i:ℕ||full-partition([a, b];p)|| - 1
      r0≤full-partition([a, b];p)[i + 1] - full-partition([a, b];p)[i]≤partition-mesh([a, b];p)
30. (∀x∈full-partition([a, b];p).x ∈ [a, b])
31. ∀i:ℕ. (i < ||full-partition([a, b];p)|| ⇒ (full-partition([a, b];p)[i] ∈ {x:ℝ| x ∈ I} ))
32. ∀i:ℕ. (i < ||full-partition([a, b];p)|| ⇒ (f[full-partition([a, b];p)[i]] ≤ y))
33. f[b] ≤ y
⊢ 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.  a  <  b
14.  icompact([a,  b])
15.  [a,  b]  \msubseteq{}  I 
16.  mc  :  |f[x]  -  y|  continuous  for  x  \mmember{}  [a,  b]
17.  r0  <  inf\{|f[x]  -  y||x  \mmember{}  [a,  b]\}
18.  n  :  \mBbbN{}\msupplus{}
19.  a  \mmember{}  i-approx(I;n)
20.  b  \mmember{}  i-approx(I;n)
21.  [a,  b]  \msubseteq{}  i-approx(I;n) 
22.  k  :  \mBbbN{}\msupplus{}
23.  (r1/r(k))  <  inf\{|f[x]  -  y||x  \mmember{}  [a,  b]\}
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([a,  b])
28.  partition-mesh([a,  b];p)  \mleq{}  d
29.  \mforall{}i:\mBbbN{}||full-partition([a,  b];p)||  -  1
            r0\mleq{}full-partition([a,  b];p)[i  +  1]  -  full-partition([a,  b];p)[i]\mleq{}partition-mesh([a,  b];p)
30.  (\mforall{}x\mmember{}full-partition([a,  b];p).x  \mmember{}  [a,  b])
31.  \mforall{}i:\mBbbN{}.  (i  <  ||full-partition([a,  b];p)||  {}\mRightarrow{}  (full-partition([a,  b];p)[i]  \mmember{}  \{x:\mBbbR{}|  x  \mmember{}  I\}  ))
32.  \mforall{}i:\mBbbN{}.  (i  <  ||full-partition([a,  b];p)||  {}\mRightarrow{}  (f[full-partition([a,  b];p)[i]]  \mleq{}  y))
\mvdash{}  False


By

---

Latex:
(Assert  f[b]  \mleq{}  y  BY
              (RepUR  ``full-partition``  -1
                THEN  (InstHyp  [\mkleeneopen{}||p  @  [right-endpoint([a,  b])]||\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))

---

Home Index