---

Step * 2 1 2 1 1 1 1 1 1 2 2 1 1 1 1 4 2 1 1 1 1 1 1 2 1 1 1 of Lemma small-rexp-remainder


1. x : {x:ℝ| |x| ≤ (r1/r(4))} 
2. n : ℕ
3. ¬(n = 0 ∈ ℤ)
4. e : {e:ℝ| r0 < e} 
5. c : ℝ
6. rmin(r0;x) ≤ c
7. c ≤ rmax(r0;x)
8. r0 < r(4^n * 3 * (n)!)
9. v : ℝ
10. Taylor-remainder((-∞, ∞);n;x;r0;k,x.e^x) = v ∈ ℝ
11. v1 : ℝ
12. (e^x - Σ{(x^k/r((k)!)) | 0≤k≤n}) = v1 ∈ ℝ
13. |v - (x - c^n * (e^c/r((n)!))) * (x - r0)| ≤ e
14. v1 = v
15. |(e^c/r((n)!))| = (e^c/r((n)!))
16. v2 : ℝ
17. |x - c^n| = v2 ∈ ℝ
18. v3 : ℝ
19. |x - r0| = v3 ∈ ℝ
20. (e^(r1/r(4)) * v3) ≤ (e^(r1/r(4))/r(4))
21. v2 ≤ |x|^n
22. M : ℕ+
23. (n)! = M ∈ ℕ+
24. v2 ≤ (r1/r(4^n))
25. c ≤ (r1/r(4))
26. (e^c * v3) ≤ (e^(r1/r(4)) * v3)
27. r0 ≤ e^c
28. r0 ≤ v3
29. r0 ≤ e^(r1/r(4))
30. (e^c * v3) ≤ (e^(r1/r(4))/r(4))
31. (e^(r1/r(4))/r(4)) < (r1/r(3))
32. (e^c * v3) ≤ (r1/r(3))
33. r0 ≤ v2
34. (r1/r(4^n) * r(3)) = ((r1/r(4^n)) * (r1/r(3)))
⊢ ((v2 * e^c) * v3) ≤ (r1/r(4^n) * r(3))
BY
{ (RWO "rmul_assoc" 0 THENA Auto) }

1
1. x : {x:ℝ| |x| ≤ (r1/r(4))} 
2. n : ℕ
3. ¬(n = 0 ∈ ℤ)
4. e : {e:ℝ| r0 < e} 
5. c : ℝ
6. rmin(r0;x) ≤ c
7. c ≤ rmax(r0;x)
8. r0 < r(4^n * 3 * (n)!)
9. v : ℝ
10. Taylor-remainder((-∞, ∞);n;x;r0;k,x.e^x) = v ∈ ℝ
11. v1 : ℝ
12. (e^x - Σ{(x^k/r((k)!)) | 0≤k≤n}) = v1 ∈ ℝ
13. |v - (x - c^n * (e^c/r((n)!))) * (x - r0)| ≤ e
14. v1 = v
15. |(e^c/r((n)!))| = (e^c/r((n)!))
16. v2 : ℝ
17. |x - c^n| = v2 ∈ ℝ
18. v3 : ℝ
19. |x - r0| = v3 ∈ ℝ
20. (e^(r1/r(4)) * v3) ≤ (e^(r1/r(4))/r(4))
21. v2 ≤ |x|^n
22. M : ℕ+
23. (n)! = M ∈ ℕ+
24. v2 ≤ (r1/r(4^n))
25. c ≤ (r1/r(4))
26. (e^c * v3) ≤ (e^(r1/r(4)) * v3)
27. r0 ≤ e^c
28. r0 ≤ v3
29. r0 ≤ e^(r1/r(4))
30. (e^c * v3) ≤ (e^(r1/r(4))/r(4))
31. (e^(r1/r(4))/r(4)) < (r1/r(3))
32. (e^c * v3) ≤ (r1/r(3))
33. r0 ≤ v2
34. (r1/r(4^n) * r(3)) = ((r1/r(4^n)) * (r1/r(3)))
⊢ (v2 * e^c * v3) ≤ (r1/r(4^n) * r(3))

---

Latex:

---

Latex:

1.  x  :  \{x:\mBbbR{}|  |x|  \mleq{}  (r1/r(4))\} 
2.  n  :  \mBbbN{}
3.  \mneg{}(n  =  0)
4.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
5.  c  :  \mBbbR{}
6.  rmin(r0;x)  \mleq{}  c
7.  c  \mleq{}  rmax(r0;x)
8.  r0  <  r(4\^{}n  *  3  *  (n)!)
9.  v  :  \mBbbR{}
10.  Taylor-remainder((-\minfty{},  \minfty{});n;x;r0;k,x.e\^{}x)  =  v
11.  v1  :  \mBbbR{}
12.  (e\^{}x  -  \mSigma{}\{(x\^{}k/r((k)!))  |  0\mleq{}k\mleq{}n\})  =  v1
13.  |v  -  (x  -  c\^{}n  *  (e\^{}c/r((n)!)))  *  (x  -  r0)|  \mleq{}  e
14.  v1  =  v
15.  |(e\^{}c/r((n)!))|  =  (e\^{}c/r((n)!))
16.  v2  :  \mBbbR{}
17.  |x  -  c\^{}n|  =  v2
18.  v3  :  \mBbbR{}
19.  |x  -  r0|  =  v3
20.  (e\^{}(r1/r(4))  *  v3)  \mleq{}  (e\^{}(r1/r(4))/r(4))
21.  v2  \mleq{}  |x|\^{}n
22.  M  :  \mBbbN{}\msupplus{}
23.  (n)!  =  M
24.  v2  \mleq{}  (r1/r(4\^{}n))
25.  c  \mleq{}  (r1/r(4))
26.  (e\^{}c  *  v3)  \mleq{}  (e\^{}(r1/r(4))  *  v3)
27.  r0  \mleq{}  e\^{}c
28.  r0  \mleq{}  v3
29.  r0  \mleq{}  e\^{}(r1/r(4))
30.  (e\^{}c  *  v3)  \mleq{}  (e\^{}(r1/r(4))/r(4))
31.  (e\^{}(r1/r(4))/r(4))  <  (r1/r(3))
32.  (e\^{}c  *  v3)  \mleq{}  (r1/r(3))
33.  r0  \mleq{}  v2
34.  (r1/r(4\^{}n)  *  r(3))  =  ((r1/r(4\^{}n))  *  (r1/r(3)))
\mvdash{}  ((v2  *  e\^{}c)  *  v3)  \mleq{}  (r1/r(4\^{}n)  *  r(3))


By

---

Latex:
(RWO  "rmul\_assoc"  0  THENA  Auto)

---

Home Index