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