Step
*
1
1
1
1
1
1
1
of Lemma
intermediate-value-theorem
1. I : Interval
2. f : I ⟶ℝ
3. f[x] continuous for x ∈ I
4. a : {x:ℝ| x ∈ I}
5. b : {x:ℝ| x ∈ I}
6. f(a) < f(b)
7. y : {y:ℝ| y ∈ [f(a), f(b)]}
8. e : {e:ℝ| r0 < e}
9. a < b
10. icompact([a, b])
11. [a, b] ⊆ I
12. mc : |f[x] - y| continuous for x ∈ [a, b]
13. r0 < inf{|f[x] - y||x ∈ [a, b]}
14. n : ℕ+
15. a ∈ i-approx(I;n)
16. b ∈ i-approx(I;n)
17. [a, b] ⊆ i-approx(I;n)
18. k : ℕ+
19. (r1/r(k)) < inf{|f[x] - y||x ∈ [a, b]}
20. d : ℝ
21. r0 < d
22. ∀x,y:ℝ. ((x ∈ i-approx(I;n)) ⇒ (y ∈ i-approx(I;n)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(k))))
23. p : partition([a, b])
24. partition-mesh([a, b];p) ≤ d
25. ∀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)
⊢ False
BY
{ (DSetVars
THEN (InstLemma `full-partition-point-member` [⌜[a, b]⌝;⌜p⌝]⋅ THENA Auto)
THEN (Assert ∀i:ℕ. (i < ||full-partition([a, b];p)|| ⇒ (full-partition([a, b];p)[i] ∈ {x:ℝ| x ∈ I} )) BY
((UnivCD THENA Auto) THEN With ⌜i⌝ (D (-3))⋅ THEN Try (MemTypeCD) THEN Auto))⋅
THEN Assert ∀i:ℕ. (i < ||full-partition([a, b];p)|| ⇒ (f[full-partition([a, b];p)[i]] ≤ y))⋅)⋅ }
1
.....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))
2
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
Latex:
Latex:
1. I : Interval
2. f : I {}\mrightarrow{}\mBbbR{}
3. f[x] continuous for x \mmember{} I
4. a : \{x:\mBbbR{}| x \mmember{} I\}
5. b : \{x:\mBbbR{}| x \mmember{} I\}
6. f(a) < f(b)
7. y : \{y:\mBbbR{}| y \mmember{} [f(a), f(b)]\}
8. e : \{e:\mBbbR{}| r0 < e\}
9. a < b
10. icompact([a, b])
11. [a, b] \msubseteq{} I
12. mc : |f[x] - y| continuous for x \mmember{} [a, b]
13. r0 < inf\{|f[x] - y||x \mmember{} [a, b]\}
14. n : \mBbbN{}\msupplus{}
15. a \mmember{} i-approx(I;n)
16. b \mmember{} i-approx(I;n)
17. [a, b] \msubseteq{} i-approx(I;n)
18. k : \mBbbN{}\msupplus{}
19. (r1/r(k)) < inf\{|f[x] - y||x \mmember{} [a, b]\}
20. d : \mBbbR{}
21. r0 < d
22. \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))))
23. p : partition([a, b])
24. partition-mesh([a, b];p) \mleq{} d
25. \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)
\mvdash{} False
By
Latex:
(DSetVars
THEN (InstLemma `full-partition-point-member` [\mkleeneopen{}[a, b]\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (Assert \mforall{}i:\mBbbN{}
(i < ||full-partition([a, b];p)|| {}\mRightarrow{} (full-partition([a, b];p)[i] \mmember{} \{x:\mBbbR{}| x \mmember{} I\} )) \000CBY
((UnivCD THENA Auto) THEN With \mkleeneopen{}i\mkleeneclose{} (D (-3))\mcdot{} THEN Try (MemTypeCD) THEN Auto))\mcdot{}
THEN Assert \mforall{}i:\mBbbN{}. (i < ||full-partition([a, b];p)|| {}\mRightarrow{} (f[full-partition([a, b];p)[i]] \mleq{} y))\mcdot{})\mcdot{}
Home
Index