Step
*
2
1
1
1
1
1
1
1
of Lemma
intermediate-value-theorem
.....assertion.....
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} ))
⊢ ∀i:ℕ. (i < ||full-partition([b, a];p)|| ⇒ (y ≤ f[full-partition([b, a];p)[i]]))
BY
{ InductionOnNat⋅ }
1
.....basecase.....
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 : ℤ
⊢ 0 < ||full-partition([b, a];p)|| ⇒ (y ≤ f[full-partition([b, a];p)[0]])
2
.....upcase.....
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 : ℤ
33. 0 < i
34. i - 1 < ||full-partition([b, a];p)|| ⇒ (y ≤ f[full-partition([b, a];p)[i - 1]])
⊢ i < ||full-partition([b, a];p)|| ⇒ (y ≤ f[full-partition([b, a];p)[i]])
Latex:
Latex:
.....assertion.....
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\} ))
\mvdash{} \mforall{}i:\mBbbN{}. (i < ||full-partition([b, a];p)|| {}\mRightarrow{} (y \mleq{} f[full-partition([b, a];p)[i]]))
By
Latex:
InductionOnNat\mcdot{}
Home
Index