Proof of Nuprl Lemma : Taylor-series-converges

Step * 1 2 1 1 1 1 1 2 1 1 1 1 1 1 1 1 1 1 1 1 1 of Lemma Taylor-series-converges

.....aux.....
1. a : ℝ
2. t : {t:ℝ| r0 < t}
3. F : ℕ ⟶ (a - t, a + t) ⟶ℝ
4. ∀k:ℕ. ∀x,y:{x:ℝ| x ∈ (a - t, a + t)} .  ((x = y) ⇒ (F[k;x] = F[k;y]))
5. infinite-deriv-seq((a - t, a + t);i,x.F[i;x])
6. m : ℕ⁺
7. icompact(i-approx((a - t, a + t);m))
8. r0 ≤ (t - (r1/r(m)))
9. n : ℕ⁺
10. M : ℕ⁺
11. ∀x:{x:ℝ| x ∈ [(a - t) + (r1/r(m)), (a + t) - (r1/r(m))]} . (|x - a| ≤ r(M))
12. N : ℕ⁺
13. ∀x:{x:ℝ| (((a - t) + (r1/r(m))) ≤ x) ∧ (x ≤ ((a + t) - (r1/r(m))))} . ∀k:{N...}.
      (|(t - (r1/r(m))^k * (F[k + 1;x]/r((k)!))) - r0| ≤ (r1/r(2 * n * M)))
14. [(a - t) + (r1/r(m)), (a + t) - (r1/r(m))] ⊆ (a - t, a + t)
15. x : ℝ
16. x ∈ i-approx((a - t, a + t);m)
17. ∀k:{N...}. (|(t - (r1/r(m))^k * (F[k + 1;x]/r((k)!))) - r0| ≤ (r1/r(2 * n * M)))
18. k : {N...}
19. |(t - (r1/r(m))^k * (F[k + 1;x]/r((k)!))) - r0| ≤ (r1/r(2 * n * M))
20. a ∈ [(a - t) + (r1/r(m)), (a + t) - (r1/r(m))]
21. ∀e:ℝ
      ((r0 < e)
      ⇒ (∃c:ℝ
           ((rmin(a;x) ≤ c)
           ∧ (c ≤ rmax(a;x))

           ∧ (|Taylor-remainder([(a - t) + (r1/r(m)), (a + t) - (r1/r(m))];k;x;a;k,x.F[k;x]) - (x - c^k

             * (F[k + 1;c]/r((k)!)))
             * (x - a)| ≤ e))))
22. c : ℝ
23. rmin(a;x) ≤ c
24. c ≤ rmax(a;x)
25. [rmin(a;x), rmax(a;x)] ⊆ (a - t, a + t)
⊢ c ∈ {x:ℝ| (((a - t) + (r1/r(m))) ≤ x) ∧ (x ≤ ((a + t) - (r1/r(m))))}
BY
{ TACTIC:TACTIC:(MemTypeCD THEN Auto THEN All  (RepUR ``i-member``)⋅ THEN Auto) }

1
1. a : ℝ
2. t : {t:ℝ| r0 < t}
3. F : ℕ ⟶ (a - t, a + t) ⟶ℝ
4. ∀k:ℕ. ∀x,y:{x:ℝ| ((a - t) < x) ∧ (x < (a + t))} .  ((x = y) ⇒ (F[k;x] = F[k;y]))
5. infinite-deriv-seq((a - t, a + t);i,x.F[i;x])
6. m : ℕ⁺
7. icompact(i-approx((a - t, a + t);m))
8. r0 ≤ (t - (r1/r(m)))
9. n : ℕ⁺
10. M : ℕ⁺

11. ∀x:{x:ℝ| (((a - t) + (r1/r(m))) ≤ x) ∧ (x ≤ ((a + t) - (r1/r(m))))} . (|x - a| ≤ r(M))

12. N : ℕ⁺
13. ∀x:{x:ℝ| (((a - t) + (r1/r(m))) ≤ x) ∧ (x ≤ ((a + t) - (r1/r(m))))} . ∀k:{N...}.
      (|(t - (r1/r(m))^k * (F[k + 1;x]/r((k)!))) - r0| ≤ (r1/r(2 * n * M)))
14. [(a - t) + (r1/r(m)), (a + t) - (r1/r(m))] ⊆ (a - t, a + t)
15. x : ℝ
16. ((a - t) + (r1/r(m))) ≤ x
17. x ≤ ((a + t) - (r1/r(m)))
18. ∀k:{N...}. (|(t - (r1/r(m))^k * (F[k + 1;x]/r((k)!))) - r0| ≤ (r1/r(2 * n * M)))
19. k : {N...}
20. |(t - (r1/r(m))^k * (F[k + 1;x]/r((k)!))) - r0| ≤ (r1/r(2 * n * M))
21. ((a - t) + (r1/r(m))) ≤ a
22. a ≤ ((a + t) - (r1/r(m)))
23. ∀e:ℝ
      ((r0 < e)
      ⇒ (∃c:ℝ
           ((rmin(a;x) ≤ c)
           ∧ (c ≤ rmax(a;x))

           ∧ (|Taylor-remainder([(a - t) + (r1/r(m)), (a + t) - (r1/r(m))];k;x;a;k,x.F[k;x]) - (x - c^k

             * (F[k + 1;c]/r((k)!)))
             * (x - a)| ≤ e))))
24. c : ℝ
25. rmin(a;x) ≤ c
26. c ≤ rmax(a;x)
27. [rmin(a;x), rmax(a;x)] ⊆ (a - t, a + t)
⊢ ((a - t) + (r1/r(m))) ≤ c

2
1. a : ℝ
2. t : {t:ℝ| r0 < t}
3. F : ℕ ⟶ (a - t, a + t) ⟶ℝ
4. ∀k:ℕ. ∀x,y:{x:ℝ| ((a - t) < x) ∧ (x < (a + t))} .  ((x = y) ⇒ (F[k;x] = F[k;y]))
5. infinite-deriv-seq((a - t, a + t);i,x.F[i;x])
6. m : ℕ⁺
7. icompact(i-approx((a - t, a + t);m))
8. r0 ≤ (t - (r1/r(m)))
9. n : ℕ⁺
10. M : ℕ⁺

11. ∀x:{x:ℝ| (((a - t) + (r1/r(m))) ≤ x) ∧ (x ≤ ((a + t) - (r1/r(m))))} . (|x - a| ≤ r(M))

           ∧ (|Taylor-remainder([(a - t) + (r1/r(m)), (a + t) - (r1/r(m))];k;x;a;k,x.F[k;x]) - (x - c^k

* (F[k + 1;c]/r((k)!)))
* (x - a)| ≤ e))))
24. c : ℝ
25. rmin(a;x) ≤ c
26. c ≤ rmax(a;x)
27. [rmin(a;x), rmax(a;x)] ⊆ (a - t, a + t)
28. ((a - t) + (r1/r(m))) ≤ c
⊢ c ≤ ((a + t) - (r1/r(m)))

Latex:

Latex:
.....aux..... 1. a : \mBbbR{} 2. t : \{t:\mBbbR{}| r0 < t\} 3. F : \mBbbN{} {}\mrightarrow{} (a - t, a + t) {}\mrightarrow{}\mBbbR{} 4. \mforall{}k:\mBbbN{}. \mforall{}x,y:\{x:\mBbbR{}| x \mmember{} (a - t, a + t)\} . ((x = y) {}\mRightarrow{} (F[k;x] = F[k;y])) 5. infinite-deriv-seq((a - t, a + t);i,x.F[i;x]) 6. m : \mBbbN{}\msupplus{} 7. icompact(i-approx((a - t, a + t);m)) 8. r0 \mleq{} (t - (r1/r(m))) 9. n : \mBbbN{}\msupplus{} 10. M : \mBbbN{}\msupplus{} 11. \mforall{}x:\{x:\mBbbR{}| x \mmember{} [(a - t) + (r1/r(m)), (a + t) - (r1/r(m))]\} . (|x - a| \mleq{} r(M)) 12. N : \mBbbN{}\msupplus{} 13. \mforall{}x:\{x:\mBbbR{}| (((a - t) + (r1/r(m))) \mleq{} x) \mwedge{} (x \mleq{} ((a + t) - (r1/r(m))))\} . \mforall{}k:\{N...\}. (|(t - (r1/r(m))\^{}k * (F[k + 1;x]/r((k)!))) - r0| \mleq{} (r1/r(2 * n * M))) 14. [(a - t) + (r1/r(m)), (a + t) - (r1/r(m))] \msubseteq{} (a - t, a + t) 15. x : \mBbbR{} 16. x \mmember{} i-approx((a - t, a + t);m) 17. \mforall{}k:\{N...\}. (|(t - (r1/r(m))\^{}k * (F[k + 1;x]/r((k)!))) - r0| \mleq{} (r1/r(2 * n * M))) 18. k : \{N...\} 19. |(t - (r1/r(m))\^{}k * (F[k + 1;x]/r((k)!))) - r0| \mleq{} (r1/r(2 * n * M)) 20. a \mmember{} [(a - t) + (r1/r(m)), (a + t) - (r1/r(m))] 21. \mforall{}e:\mBbbR{} ((r0 < e) {}\mRightarrow{} (\mexists{}c:\mBbbR{} ((rmin(a;x) \mleq{} c) \mwedge{} (c \mleq{} rmax(a;x)) \mwedge{} (|Taylor-remainder([(a - t) + (r1/r(m)), (a + t) - (r1/r(m))];k;x;a;k,x.F[k;x]) - (x - c\^{}k * (F[k + 1;c]/r((k)!))) * (x - a)| \mleq{} e)))) 22. c : \mBbbR{} 23. rmin(a;x) \mleq{} c 24. c \mleq{} rmax(a;x) 25. [rmin(a;x), rmax(a;x)] \msubseteq{} (a - t, a + t) \mvdash{} c \mmember{} \{x:\mBbbR{}| (((a - t) + (r1/r(m))) \mleq{} x) \mwedge{} (x \mleq{} ((a + t) - (r1/r(m))))\} By Latex: TACTIC:TACTIC:(MemTypeCD THEN Auto THEN All (RepUR ``i-member``)\mcdot{} THEN Auto) Home Index