Step
*
1
1
1
1
2
1
1
1
of Lemma
real-path-comp-exists
.....aux.....
1. f : [r0, r1] ⟶ℝ
2. g : [r0, r1] ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ [r0, r1]} . ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:{x:ℝ| x ∈ [r0, r1]} . ((x = y) ⇒ (g(x) = g(y)))
5. f(r1) = g(r0)
6. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (rmin(t;(r1/r(2))) = t)
7. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (r(2) * t ∈ [r0, r1])
8. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (f(r(2) * rmin(t;(r1/r(2)))) = f(r(2) * t))
9. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (rmax(t;(r1/r(2))) = t)
10. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . ((r(2) * t) - r1 ∈ [r0, r1])
11. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) = g((r(2) * t) - r1))
12. ∀t:{x:ℝ| x ∈ [r0, r1]} . (f(r(2) * rmin(t;(r1/r(2)))) ∈ ℝ)
13. ∀t:{x:ℝ| x ∈ [r0, r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) ∈ ℝ)
14. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
∃m:ℕ+
((|t - (r1/r(2))| ≤ (r1/r(m)))
⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(n))))
15. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
∃x:ℝ
(((t < ((r1/r(2)) + (r1/r(n)))) ∧ (x = f(r(2) * rmin(t;(r1/r(2))))))
∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ (x = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
16. h : t:{x:ℝ| x ∈ [r0, r1]} ⟶ n:ℕ+ ⟶ ℝ
17. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
(((t < ((r1/r(2)) + (r1/r(n)))) ∧ ((h t n) = f(r(2) * rmin(t;(r1/r(2))))))
∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ ((h t n) = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
18. t : {x:ℝ| x ∈ [r0, r1]}
19. k : ℕ+
⊢ ∃N:ℕ [(∀n,m:ℕ. ((N ≤ n) ⇒ (N ≤ m) ⇒ (|(h t (n + 1)) - h t (m + 1)| ≤ (r1/r(k)))))]
BY
{ ((InstHyp [⌜t⌝;⌜k⌝] (-6)⋅ THENA Auto)
THEN D -1
THEN D 0 With ⌜m⌝
THEN Auto
THEN RenameVar `j' (-3)
THEN (InstHyp [⌜t⌝;⌜j + 1⌝] 17⋅ THENA Auto)
THEN (InstHyp [⌜t⌝;⌜n + 1⌝] 17⋅ THENA Auto)
THEN SplitOrHyps
THEN ExRepD
THEN RWO "-3 -1" 0
THEN Auto) }
1
1. f : [r0, r1] ⟶ℝ
2. g : [r0, r1] ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ [r0, r1]} . ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:{x:ℝ| x ∈ [r0, r1]} . ((x = y) ⇒ (g(x) = g(y)))
5. f(r1) = g(r0)
6. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (rmin(t;(r1/r(2))) = t)
7. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (r(2) * t ∈ [r0, r1])
8. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (f(r(2) * rmin(t;(r1/r(2)))) = f(r(2) * t))
9. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (rmax(t;(r1/r(2))) = t)
10. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . ((r(2) * t) - r1 ∈ [r0, r1])
11. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) = g((r(2) * t) - r1))
12. ∀t:{x:ℝ| x ∈ [r0, r1]} . (f(r(2) * rmin(t;(r1/r(2)))) ∈ ℝ)
13. ∀t:{x:ℝ| x ∈ [r0, r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) ∈ ℝ)
14. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
∃m:ℕ+
((|t - (r1/r(2))| ≤ (r1/r(m)))
⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(n))))
15. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
∃x:ℝ
(((t < ((r1/r(2)) + (r1/r(n)))) ∧ (x = f(r(2) * rmin(t;(r1/r(2))))))
∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ (x = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
16. h : t:{x:ℝ| x ∈ [r0, r1]} ⟶ n:ℕ+ ⟶ ℝ
17. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
(((t < ((r1/r(2)) + (r1/r(n)))) ∧ ((h t n) = f(r(2) * rmin(t;(r1/r(2))))))
∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ ((h t n) = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
18. t : {x:ℝ| x ∈ [r0, r1]}
19. k : ℕ+
20. m : ℕ+
21. (|t - (r1/r(2))| ≤ (r1/r(m))) ⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(k)))
22. n : ℕ
23. j : ℕ
24. m ≤ n
25. m ≤ j
26. t < ((r1/r(2)) + (r1/r(j + 1)))
27. (h t (j + 1)) = f(r(2) * rmin(t;(r1/r(2))))
28. t < ((r1/r(2)) + (r1/r(n + 1)))
29. (h t (n + 1)) = f(r(2) * rmin(t;(r1/r(2))))
⊢ |f(r(2) * rmin(t;(r1/r(2)))) - f(r(2) * rmin(t;(r1/r(2))))| ≤ (r1/r(k))
2
1. f : [r0, r1] ⟶ℝ
2. g : [r0, r1] ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ [r0, r1]} . ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:{x:ℝ| x ∈ [r0, r1]} . ((x = y) ⇒ (g(x) = g(y)))
5. f(r1) = g(r0)
6. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (rmin(t;(r1/r(2))) = t)
7. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (r(2) * t ∈ [r0, r1])
8. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (f(r(2) * rmin(t;(r1/r(2)))) = f(r(2) * t))
9. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (rmax(t;(r1/r(2))) = t)
10. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . ((r(2) * t) - r1 ∈ [r0, r1])
11. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) = g((r(2) * t) - r1))
12. ∀t:{x:ℝ| x ∈ [r0, r1]} . (f(r(2) * rmin(t;(r1/r(2)))) ∈ ℝ)
13. ∀t:{x:ℝ| x ∈ [r0, r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) ∈ ℝ)
14. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
∃m:ℕ+
((|t - (r1/r(2))| ≤ (r1/r(m)))
⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(n))))
15. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
∃x:ℝ
(((t < ((r1/r(2)) + (r1/r(n)))) ∧ (x = f(r(2) * rmin(t;(r1/r(2))))))
∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ (x = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
16. h : t:{x:ℝ| x ∈ [r0, r1]} ⟶ n:ℕ+ ⟶ ℝ
17. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
(((t < ((r1/r(2)) + (r1/r(n)))) ∧ ((h t n) = f(r(2) * rmin(t;(r1/r(2))))))
∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ ((h t n) = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
18. t : {x:ℝ| x ∈ [r0, r1]}
19. k : ℕ+
20. m : ℕ+
21. (|t - (r1/r(2))| ≤ (r1/r(m))) ⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(k)))
22. n : ℕ
23. j : ℕ
24. m ≤ n
25. m ≤ j
26. ((r1/r(2)) - (r1/r(j + 1))) < t
27. (h t (j + 1)) = g((r(2) * rmax(t;(r1/r(2)))) - r1)
28. t < ((r1/r(2)) + (r1/r(n + 1)))
29. (h t (n + 1)) = f(r(2) * rmin(t;(r1/r(2))))
⊢ |f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(k))
3
1. f : [r0, r1] ⟶ℝ
2. g : [r0, r1] ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ [r0, r1]} . ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:{x:ℝ| x ∈ [r0, r1]} . ((x = y) ⇒ (g(x) = g(y)))
5. f(r1) = g(r0)
6. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (rmin(t;(r1/r(2))) = t)
7. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (r(2) * t ∈ [r0, r1])
8. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (f(r(2) * rmin(t;(r1/r(2)))) = f(r(2) * t))
9. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (rmax(t;(r1/r(2))) = t)
10. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . ((r(2) * t) - r1 ∈ [r0, r1])
11. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) = g((r(2) * t) - r1))
12. ∀t:{x:ℝ| x ∈ [r0, r1]} . (f(r(2) * rmin(t;(r1/r(2)))) ∈ ℝ)
13. ∀t:{x:ℝ| x ∈ [r0, r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) ∈ ℝ)
14. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
∃m:ℕ+
((|t - (r1/r(2))| ≤ (r1/r(m)))
⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(n))))
15. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
∃x:ℝ
(((t < ((r1/r(2)) + (r1/r(n)))) ∧ (x = f(r(2) * rmin(t;(r1/r(2))))))
∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ (x = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
16. h : t:{x:ℝ| x ∈ [r0, r1]} ⟶ n:ℕ+ ⟶ ℝ
17. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
(((t < ((r1/r(2)) + (r1/r(n)))) ∧ ((h t n) = f(r(2) * rmin(t;(r1/r(2))))))
∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ ((h t n) = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
18. t : {x:ℝ| x ∈ [r0, r1]}
19. k : ℕ+
20. m : ℕ+
21. (|t - (r1/r(2))| ≤ (r1/r(m))) ⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(k)))
22. n : ℕ
23. j : ℕ
24. m ≤ n
25. m ≤ j
26. t < ((r1/r(2)) + (r1/r(j + 1)))
27. (h t (j + 1)) = f(r(2) * rmin(t;(r1/r(2))))
28. ((r1/r(2)) - (r1/r(n + 1))) < t
29. (h t (n + 1)) = g((r(2) * rmax(t;(r1/r(2)))) - r1)
⊢ |g((r(2) * rmax(t;(r1/r(2)))) - r1) - f(r(2) * rmin(t;(r1/r(2))))| ≤ (r1/r(k))
4
1. f : [r0, r1] ⟶ℝ
2. g : [r0, r1] ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ [r0, r1]} . ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:{x:ℝ| x ∈ [r0, r1]} . ((x = y) ⇒ (g(x) = g(y)))
5. f(r1) = g(r0)
6. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (rmin(t;(r1/r(2))) = t)
7. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (r(2) * t ∈ [r0, r1])
8. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (f(r(2) * rmin(t;(r1/r(2)))) = f(r(2) * t))
9. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (rmax(t;(r1/r(2))) = t)
10. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . ((r(2) * t) - r1 ∈ [r0, r1])
11. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) = g((r(2) * t) - r1))
12. ∀t:{x:ℝ| x ∈ [r0, r1]} . (f(r(2) * rmin(t;(r1/r(2)))) ∈ ℝ)
13. ∀t:{x:ℝ| x ∈ [r0, r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) ∈ ℝ)
14. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
∃m:ℕ+
((|t - (r1/r(2))| ≤ (r1/r(m)))
⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(n))))
15. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
∃x:ℝ
(((t < ((r1/r(2)) + (r1/r(n)))) ∧ (x = f(r(2) * rmin(t;(r1/r(2))))))
∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ (x = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
16. h : t:{x:ℝ| x ∈ [r0, r1]} ⟶ n:ℕ+ ⟶ ℝ
17. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
(((t < ((r1/r(2)) + (r1/r(n)))) ∧ ((h t n) = f(r(2) * rmin(t;(r1/r(2))))))
∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ ((h t n) = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
18. t : {x:ℝ| x ∈ [r0, r1]}
19. k : ℕ+
20. m : ℕ+
21. (|t - (r1/r(2))| ≤ (r1/r(m))) ⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(k)))
22. n : ℕ
23. j : ℕ
24. m ≤ n
25. m ≤ j
26. ((r1/r(2)) - (r1/r(j + 1))) < t
27. (h t (j + 1)) = g((r(2) * rmax(t;(r1/r(2)))) - r1)
28. ((r1/r(2)) - (r1/r(n + 1))) < t
29. (h t (n + 1)) = g((r(2) * rmax(t;(r1/r(2)))) - r1)
⊢ |g((r(2) * rmax(t;(r1/r(2)))) - r1) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(k))
Latex:
Latex:
.....aux.....
1. f : [r0, r1] {}\mrightarrow{}\mBbbR{}
2. g : [r0, r1] {}\mrightarrow{}\mBbbR{}
3. \mforall{}x,y:\{x:\mBbbR{}| x \mmember{} [r0, r1]\} . ((x = y) {}\mRightarrow{} (f(x) = f(y)))
4. \mforall{}x,y:\{x:\mBbbR{}| x \mmember{} [r0, r1]\} . ((x = y) {}\mRightarrow{} (g(x) = g(y)))
5. f(r1) = g(r0)
6. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [r0, (r1/r(2))]\} . (rmin(t;(r1/r(2))) = t)
7. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [r0, (r1/r(2))]\} . (r(2) * t \mmember{} [r0, r1])
8. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [r0, (r1/r(2))]\} . (f(r(2) * rmin(t;(r1/r(2)))) = f(r(2) * t))
9. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [(r1/r(2)), r1]\} . (rmax(t;(r1/r(2))) = t)
10. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [(r1/r(2)), r1]\} . ((r(2) * t) - r1 \mmember{} [r0, r1])
11. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [(r1/r(2)), r1]\} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) = g((r(2) * t) - r1))
12. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [r0, r1]\} . (f(r(2) * rmin(t;(r1/r(2)))) \mmember{} \mBbbR{})
13. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [r0, r1]\} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) \mmember{} \mBbbR{})
14. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [r0, r1]\} . \mforall{}n:\mBbbN{}\msupplus{}.
\mexists{}m:\mBbbN{}\msupplus{}
((|t - (r1/r(2))| \mleq{} (r1/r(m)))
{}\mRightarrow{} (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| \mleq{} (r1/r(n))))
15. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [r0, r1]\} . \mforall{}n:\mBbbN{}\msupplus{}.
\mexists{}x:\mBbbR{}
(((t < ((r1/r(2)) + (r1/r(n)))) \mwedge{} (x = f(r(2) * rmin(t;(r1/r(2))))))
\mvee{} ((((r1/r(2)) - (r1/r(n))) < t) \mwedge{} (x = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
16. h : t:\{x:\mBbbR{}| x \mmember{} [r0, r1]\} {}\mrightarrow{} n:\mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbR{}
17. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [r0, r1]\} . \mforall{}n:\mBbbN{}\msupplus{}.
(((t < ((r1/r(2)) + (r1/r(n)))) \mwedge{} ((h t n) = f(r(2) * rmin(t;(r1/r(2))))))
\mvee{} ((((r1/r(2)) - (r1/r(n))) < t) \mwedge{} ((h t n) = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
18. t : \{x:\mBbbR{}| x \mmember{} [r0, r1]\}
19. k : \mBbbN{}\msupplus{}
\mvdash{} \mexists{}N:\mBbbN{} [(\mforall{}n,m:\mBbbN{}. ((N \mleq{} n) {}\mRightarrow{} (N \mleq{} m) {}\mRightarrow{} (|(h t (n + 1)) - h t (m + 1)| \mleq{} (r1/r(k)))))]
By
Latex:
((InstHyp [\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}] (-6)\mcdot{} THENA Auto)
THEN D -1
THEN D 0 With \mkleeneopen{}m\mkleeneclose{}
THEN Auto
THEN RenameVar `j' (-3)
THEN (InstHyp [\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}j + 1\mkleeneclose{}] 17\mcdot{} THENA Auto)
THEN (InstHyp [\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}n + 1\mkleeneclose{}] 17\mcdot{} THENA Auto)
THEN SplitOrHyps
THEN ExRepD
THEN RWO "-3 -1" 0
THEN Auto)
Home
Index