Step
*
2
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. b < a
10. icompact([b, a])
11. [b, a] ⊆ I
12. mc : |f[x] - y| continuous for x ∈ [b, a]
13. r0 < inf{|f[x] - y||x ∈ [b, a]}
14. n : ℕ+
15. b ∈ i-approx(I;n)
16. a ∈ i-approx(I;n)
17. [b, a] ⊆ i-approx(I;n)
18. k : ℕ+
19. (r1/r(k)) < inf{|f[x] - y||x ∈ [b, a]}
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([b, a])
24. partition-mesh([b, a];p) ≤ d
25. ∀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)
⊢ False
BY
{ (TACTIC:DSetVars
THEN (InstLemma `full-partition-point-member` [⌜[b, a]⌝;⌜p⌝]⋅ THENA Auto)
THEN (Assert ∀i:ℕ. (i < ||full-partition([b, a];p)|| ⇒ (full-partition([b, a];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([b, a];p)|| ⇒ (y ≤ f[full-partition([b, a];p)[i]]))⋅) }
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. 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]]))
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. 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:ℕ. (i < ||full-partition([b, a];p)|| ⇒ (y ≤ f[full-partition([b, a];p)[i]]))
⊢ 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. b < a
10. icompact([b, a])
11. [b, a] \msubseteq{} I
12. mc : |f[x] - y| continuous for x \mmember{} [b, a]
13. r0 < inf\{|f[x] - y||x \mmember{} [b, a]\}
14. n : \mBbbN{}\msupplus{}
15. b \mmember{} i-approx(I;n)
16. a \mmember{} i-approx(I;n)
17. [b, a] \msubseteq{} i-approx(I;n)
18. k : \mBbbN{}\msupplus{}
19. (r1/r(k)) < inf\{|f[x] - y||x \mmember{} [b, a]\}
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([b, a])
24. partition-mesh([b, a];p) \mleq{} d
25. \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)
\mvdash{} False
By
Latex:
(TACTIC:DSetVars
THEN (InstLemma `full-partition-point-member` [\mkleeneopen{}[b, a]\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (Assert \mforall{}i:\mBbbN{}
(i < ||full-partition([b, a];p)|| {}\mRightarrow{} (full-partition([b, a];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([b, a];p)|| {}\mRightarrow{} (y \mleq{} f[full-partition([b, a];p)[i]]))\mcdot{})
Home
Index