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


1. Interval
2. I ⟶ℝ
3. f[x] continuous for x ∈ I
4. : ℝ
5. a ∈ I
6. : ℝ
7. b ∈ I
8. f(a) < f(b)
9. : ℝ
10. y ∈ [f(a), f(b)]
11. : ℝ
12. r0 < e
13. b < a
14. icompact([b, a])
15. [b, a] ⊆ 
16. mc |f[x] y| continuous for x ∈ [b, a]
17. r0 < inf{|f[x] y||x ∈ [b, a]}
18. : ℕ+
19. b ∈ i-approx(I;n)
20. a ∈ i-approx(I;n)
21. [b, a] ⊆ i-approx(I;n) 
22. : ℕ+
23. (r1/r(k)) < inf{|f[x] y||x ∈ [b, a]}
24. : ℝ
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. 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. : ℤ
33. 0 < i
34. i < ||full-partition([b, a];p)||
35. {u:ℝu ∈ [b, a]} 
36. full-partition([b, a];p)[i] u ∈ {u:ℝu ∈ [b, a]} 
37. {u:ℝu ∈ [b, a]} 
38. full-partition([b, a];p)[i 1] v ∈ {u:ℝu ∈ [b, a]} 
39. r0≤v≤partition-mesh([b, a];p)
40. y ≤ f[v]
41. -(f[u] f[v]) ≤ (r1/r(k))
42. f[u] < y
⊢ False
BY
(Assert ∀x:ℝ((x ∈ [b, a])  ((r1/r(k)) < |f[x] y|)) BY
         (Auto
          THEN ((InstLemma `range-inf-property` [⌜[b, a]⌝;⌜λ2x.|f[x] y|⌝;⌜mc⌝]⋅ THENA Auto)
                THEN -1
                THEN Thin (-1)
                THEN Unfold `lower-bound` -1
                THEN InstHyp [⌜|f[x] y|⌝(-1)⋅
                THEN Auto
                THEN RepUR ``rset-member rrange`` 0
                THEN With ⌜x⌝ (D 0)⋅
                THEN Auto)⋅
          )) }

1
1. Interval
2. I ⟶ℝ
3. f[x] continuous for x ∈ I
4. : ℝ
5. a ∈ I
6. : ℝ
7. b ∈ I
8. f(a) < f(b)
9. : ℝ
10. y ∈ [f(a), f(b)]
11. : ℝ
12. r0 < e
13. b < a
14. icompact([b, a])
15. [b, a] ⊆ 
16. mc |f[x] y| continuous for x ∈ [b, a]
17. r0 < inf{|f[x] y||x ∈ [b, a]}
18. : ℕ+
19. b ∈ i-approx(I;n)
20. a ∈ i-approx(I;n)
21. [b, a] ⊆ i-approx(I;n) 
22. : ℕ+
23. (r1/r(k)) < inf{|f[x] y||x ∈ [b, a]}
24. : ℝ
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. 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. : ℤ
33. 0 < i
34. i < ||full-partition([b, a];p)||
35. {u:ℝu ∈ [b, a]} 
36. full-partition([b, a];p)[i] u ∈ {u:ℝu ∈ [b, a]} 
37. {u:ℝu ∈ [b, a]} 
38. full-partition([b, a];p)[i 1] v ∈ {u:ℝu ∈ [b, a]} 
39. r0≤v≤partition-mesh([b, a];p)
40. y ≤ f[v]
41. -(f[u] f[v]) ≤ (r1/r(k))
42. f[u] < y
43. ∀x:ℝ((x ∈ [b, a])  ((r1/r(k)) < |f[x] 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.  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.  i  :  \mBbbZ{}
33.  0  <  i
34.  i  <  ||full-partition([b,  a];p)||
35.  u  :  \{u:\mBbbR{}|  u  \mmember{}  [b,  a]\} 
36.  full-partition([b,  a];p)[i]  =  u
37.  v  :  \{u:\mBbbR{}|  u  \mmember{}  [b,  a]\} 
38.  full-partition([b,  a];p)[i  -  1]  =  v
39.  r0\mleq{}u  -  v\mleq{}partition-mesh([b,  a];p)
40.  y  \mleq{}  f[v]
41.  -(f[u]  -  f[v])  \mleq{}  (r1/r(k))
42.  f[u]  <  y
\mvdash{}  False


By


Latex:
(Assert  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  [b,  a])  {}\mRightarrow{}  ((r1/r(k))  <  |f[x]  -  y|))  BY
              (Auto
                THEN  ((InstLemma  `range-inf-property`  [\mkleeneopen{}[b,  a]\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.|f[x]  -  y|\mkleeneclose{};\mkleeneopen{}mc\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  D  -1
                            THEN  Thin  (-1)
                            THEN  Unfold  `lower-bound`  -1
                            THEN  InstHyp  [\mkleeneopen{}|f[x]  -  y|\mkleeneclose{}]  (-1)\mcdot{}
                            THEN  Auto
                            THEN  RepUR  ``rset-member  rrange``  0
                            THEN  With  \mkleeneopen{}x\mkleeneclose{}  (D  0)\mcdot{}
                            THEN  Auto)\mcdot{}
                ))




Home Index