Theorem ef01bndlem

Description: Lemma for sin01bnd and cos01bnd . (Contributed by Paul Chapman, 19-Jan-2008)

	Ref	Expression
Hypothesis	ef01bnd.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{{\mathrm{i}A}^n}{n!}\right)$$
Assertion	ef01bndlem	$$⊢A\in \left(0,1\right]\to \left|\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)\right|<\frac{A^4}{6}$$

Proof

Step	Hyp	Ref	Expression
1		ef01bnd.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{{\mathrm{i}A}^n}{n!}\right)$$
2		ax-icn	$$⊢\mathrm{i}\in ℂ$$
3		0xr	$$⊢0\in {ℝ}^{*}$$
4		1re	$$⊢1\in ℝ$$
5		elioc2	$$⊢\left(0\in {ℝ}^{*}\wedge 1\in ℝ\right)\to \left(A\in \left(0,1\right]\leftrightarrow \left(A\in ℝ\wedge 0<A\wedge A\le 1\right)\right)$$
6	3 4 5	mp2an	$$⊢A\in \left(0,1\right]\leftrightarrow \left(A\in ℝ\wedge 0<A\wedge A\le 1\right)$$
7	6	simp1bi	$$⊢A\in \left(0,1\right]\to A\in ℝ$$
8	7	recnd	$$⊢A\in \left(0,1\right]\to A\in ℂ$$
9		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}A\in ℂ$$
10	2 8 9	sylancr	$$⊢A\in \left(0,1\right]\to \mathrm{i}A\in ℂ$$
11		4nn0	$$⊢4\in {\mathbb{N}}_0$$
12	1	eftlcl	$$⊢\left(\mathrm{i}A\in ℂ\wedge 4\in {\mathbb{N}}_0\right)\to \sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)\in ℂ$$
13	10 11 12	sylancl	$$⊢A\in \left(0,1\right]\to \sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)\in ℂ$$
14	13	abscld	$$⊢A\in \left(0,1\right]\to \left|\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)\right|\in ℝ$$
15		reexpcl	$$⊢\left(A\in ℝ\wedge 4\in {\mathbb{N}}_0\right)\to A^4\in ℝ$$
16	7 11 15	sylancl	$$⊢A\in \left(0,1\right]\to A^4\in ℝ$$
17		4re	$$⊢4\in ℝ$$
18	17 4	readdcli	$$⊢4+1\in ℝ$$
19		faccl	$$⊢4\in {\mathbb{N}}_0\to 4!\in \mathbb{N}$$
20	11 19	ax-mp	$$⊢4!\in \mathbb{N}$$
21		4nn	$$⊢4\in \mathbb{N}$$
22	20 21	nnmulcli	$$⊢4!\cdot 4\in \mathbb{N}$$
23		nndivre	$$⊢\left(4+1\in ℝ\wedge 4!\cdot 4\in \mathbb{N}\right)\to \frac{4+1}{4!\cdot 4}\in ℝ$$
24	18 22 23	mp2an	$$⊢\frac{4+1}{4!\cdot 4}\in ℝ$$
25		remulcl	$$⊢\left(A^4\in ℝ\wedge \frac{4+1}{4!\cdot 4}\in ℝ\right)\to A^4\left(\frac{4+1}{4!\cdot 4}\right)\in ℝ$$
26	16 24 25	sylancl	$$⊢A\in \left(0,1\right]\to A^4\left(\frac{4+1}{4!\cdot 4}\right)\in ℝ$$
27		6nn	$$⊢6\in \mathbb{N}$$
28		nndivre	$$⊢\left(A^4\in ℝ\wedge 6\in \mathbb{N}\right)\to \frac{A^4}{6}\in ℝ$$
29	16 27 28	sylancl	$$⊢A\in \left(0,1\right]\to \frac{A^4}{6}\in ℝ$$
30		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼\frac{{\left|\mathrm{i}A\right|}^n}{n!}\right)=\left(n\in {\mathbb{N}}_0⟼\frac{{\left|\mathrm{i}A\right|}^n}{n!}\right)$$
31		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼\left(\frac{{\left|\mathrm{i}A\right|}^4}{4!}\right){\left(\frac{1}{4+1}\right)}^n\right)=\left(n\in {\mathbb{N}}_0⟼\left(\frac{{\left|\mathrm{i}A\right|}^4}{4!}\right){\left(\frac{1}{4+1}\right)}^n\right)$$
32	21	a1i	$$⊢A\in \left(0,1\right]\to 4\in \mathbb{N}$$
33		absmul	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \left|\mathrm{i}A\right|=\left|\mathrm{i}\right|\left|A\right|$$
34	2 8 33	sylancr	$$⊢A\in \left(0,1\right]\to \left|\mathrm{i}A\right|=\left|\mathrm{i}\right|\left|A\right|$$
35		absi	$$⊢\left|\mathrm{i}\right|=1$$
36	35	oveq1i	$$⊢\left|\mathrm{i}\right|\left|A\right|=1\left|A\right|$$
37	6	simp2bi	$$⊢A\in \left(0,1\right]\to 0<A$$
38	7 37	elrpd	$$⊢A\in \left(0,1\right]\to A\in {ℝ}^{+}$$
39		rpre	$$⊢A\in {ℝ}^{+}\to A\in ℝ$$
40		rpge0	$$⊢A\in {ℝ}^{+}\to 0\le A$$
41	39 40	absidd	$$⊢A\in {ℝ}^{+}\to \left|A\right|=A$$
42	38 41	syl	$$⊢A\in \left(0,1\right]\to \left|A\right|=A$$
43	42	oveq2d	$$⊢A\in \left(0,1\right]\to 1\left|A\right|=1A$$
44	36 43	syl5eq	$$⊢A\in \left(0,1\right]\to \left|\mathrm{i}\right|\left|A\right|=1A$$
45	8	mulid2d	$$⊢A\in \left(0,1\right]\to 1A=A$$
46	34 44 45	3eqtrd	$$⊢A\in \left(0,1\right]\to \left|\mathrm{i}A\right|=A$$
47	6	simp3bi	$$⊢A\in \left(0,1\right]\to A\le 1$$
48	46 47	eqbrtrd	$$⊢A\in \left(0,1\right]\to \left|\mathrm{i}A\right|\le 1$$
49	1 30 31 32 10 48	eftlub	$$⊢A\in \left(0,1\right]\to \left|\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)\right|\le {\left|\mathrm{i}A\right|}^4\left(\frac{4+1}{4!\cdot 4}\right)$$
50	46	oveq1d	$$⊢A\in \left(0,1\right]\to {\left|\mathrm{i}A\right|}^4=A^4$$
51	50	oveq1d	$$⊢A\in \left(0,1\right]\to {\left|\mathrm{i}A\right|}^4\left(\frac{4+1}{4!\cdot 4}\right)=A^4\left(\frac{4+1}{4!\cdot 4}\right)$$
52	49 51	breqtrd	$$⊢A\in \left(0,1\right]\to \left|\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)\right|\le A^4\left(\frac{4+1}{4!\cdot 4}\right)$$
53		3pos	$$⊢0<3$$
54		0re	$$⊢0\in ℝ$$
55		3re	$$⊢3\in ℝ$$
56		5re	$$⊢5\in ℝ$$
57	54 55 56	ltadd1i	$$⊢0<3\leftrightarrow 0+5<3+5$$
58	53 57	mpbi	$$⊢0+5<3+5$$
59		5cn	$$⊢5\in ℂ$$
60	59	addid2i	$$⊢0+5=5$$
61		cu2	$$⊢2^3=8$$
62		5p3e8	$$⊢5+3=8$$
63		3cn	$$⊢3\in ℂ$$
64	59 63	addcomi	$$⊢5+3=3+5$$
65	61 62 64	3eqtr2ri	$$⊢3+5=2^3$$
66	58 60 65	3brtr3i	$$⊢5<2^3$$
67		2re	$$⊢2\in ℝ$$
68		1le2	$$⊢1\le 2$$
69		4z	$$⊢4\in \mathbb{Z}$$
70		3lt4	$$⊢3<4$$
71	55 17 70	ltleii	$$⊢3\le 4$$
72		3z	$$⊢3\in \mathbb{Z}$$
73	72	eluz1i	$$⊢4\in {\mathbb{Z}}_{\ge 3}\leftrightarrow \left(4\in \mathbb{Z}\wedge 3\le 4\right)$$
74	69 71 73	mpbir2an	$$⊢4\in {\mathbb{Z}}_{\ge 3}$$
75		leexp2a	$$⊢\left(2\in ℝ\wedge 1\le 2\wedge 4\in {\mathbb{Z}}_{\ge 3}\right)\to 2^3\le 2^4$$
76	67 68 74 75	mp3an	$$⊢2^3\le 2^4$$
77		8re	$$⊢8\in ℝ$$
78	61 77	eqeltri	$$⊢2^3\in ℝ$$
79		2nn	$$⊢2\in \mathbb{N}$$
80		nnexpcl	$$⊢\left(2\in \mathbb{N}\wedge 4\in {\mathbb{N}}_0\right)\to 2^4\in \mathbb{N}$$
81	79 11 80	mp2an	$$⊢2^4\in \mathbb{N}$$
82	81	nnrei	$$⊢2^4\in ℝ$$
83	56 78 82	ltletri	$$⊢\left(5<2^3\wedge 2^3\le 2^4\right)\to 5<2^4$$
84	66 76 83	mp2an	$$⊢5<2^4$$
85		6re	$$⊢6\in ℝ$$
86	85 82	remulcli	$$⊢62^4\in ℝ$$
87		6pos	$$⊢0<6$$
88	81	nngt0i	$$⊢0<2^4$$
89	85 82 87 88	mulgt0ii	$$⊢0<62^4$$
90	56 82 86 89	ltdiv1ii	$$⊢5<2^4\leftrightarrow \frac{5}{62^4}<\frac{2^4}{62^4}$$
91	84 90	mpbi	$$⊢\frac{5}{62^4}<\frac{2^4}{62^4}$$
92		df-5	$$⊢5=4+1$$
93		df-4	$$⊢4=3+1$$
94	93	fveq2i	$$⊢4!=\left(3+1\right)!$$
95		3nn0	$$⊢3\in {\mathbb{N}}_0$$
96		facp1	$$⊢3\in {\mathbb{N}}_0\to \left(3+1\right)!=3!\left(3+1\right)$$
97	95 96	ax-mp	$$⊢\left(3+1\right)!=3!\left(3+1\right)$$
98		sq2	$$⊢2^2=4$$
99	98 93	eqtr2i	$$⊢3+1=2^2$$
100	99	oveq2i	$$⊢3!\left(3+1\right)=3!2^2$$
101	94 97 100	3eqtri	$$⊢4!=3!2^2$$
102	101	oveq1i	$$⊢4!2^2=3!2^2{2}^2$$
103	98	oveq2i	$$⊢4!2^2=4!\cdot 4$$
104		fac3	$$⊢3!=6$$
105		6cn	$$⊢6\in ℂ$$
106	104 105	eqeltri	$$⊢3!\in ℂ$$
107	17	recni	$$⊢4\in ℂ$$
108	98 107	eqeltri	$$⊢2^2\in ℂ$$
109	106 108 108	mulassi	$$⊢3!2^2{2}^2=3!2^2{2}^2$$
110	102 103 109	3eqtr3i	$$⊢4!\cdot 4=3!2^2{2}^2$$
111		2p2e4	$$⊢2+2=4$$
112	111	oveq2i	$$⊢2^{2+2}=2^4$$
113		2cn	$$⊢2\in ℂ$$
114		2nn0	$$⊢2\in {\mathbb{N}}_0$$
115		expadd	$$⊢\left(2\in ℂ\wedge 2\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\to 2^{2+2}=2^2{2}^2$$
116	113 114 114 115	mp3an	$$⊢2^{2+2}=2^2{2}^2$$
117	112 116	eqtr3i	$$⊢2^4=2^2{2}^2$$
118	117	oveq2i	$$⊢3!2^4=3!2^2{2}^2$$
119	104	oveq1i	$$⊢3!2^4=62^4$$
120	110 118 119	3eqtr2ri	$$⊢62^4=4!\cdot 4$$
121	92 120	oveq12i	$$⊢\frac{5}{62^4}=\frac{4+1}{4!\cdot 4}$$
122	81	nncni	$$⊢2^4\in ℂ$$
123	122	mulid2i	$$⊢12^4=2^4$$
124	123	oveq1i	$$⊢\frac{12^4}{62^4}=\frac{2^4}{62^4}$$
125	81	nnne0i	$$⊢2^4\ne 0$$
126	122 125	dividi	$$⊢\frac{2^4}{2^4}=1$$
127	126	oveq2i	$$⊢\left(\frac{1}{6}\right)\left(\frac{2^4}{2^4}\right)=\left(\frac{1}{6}\right)\cdot 1$$
128		ax-1cn	$$⊢1\in ℂ$$
129	85 87	gt0ne0ii	$$⊢6\ne 0$$
130	128 105 122 122 129 125	divmuldivi	$$⊢\left(\frac{1}{6}\right)\left(\frac{2^4}{2^4}\right)=\frac{12^4}{62^4}$$
131	85 129	rereccli	$$⊢\frac{1}{6}\in ℝ$$
132	131	recni	$$⊢\frac{1}{6}\in ℂ$$
133	132	mulid1i	$$⊢\left(\frac{1}{6}\right)\cdot 1=\frac{1}{6}$$
134	127 130 133	3eqtr3i	$$⊢\frac{12^4}{62^4}=\frac{1}{6}$$
135	124 134	eqtr3i	$$⊢\frac{2^4}{62^4}=\frac{1}{6}$$
136	91 121 135	3brtr3i	$$⊢\frac{4+1}{4!\cdot 4}<\frac{1}{6}$$
137		rpexpcl	$$⊢\left(A\in {ℝ}^{+}\wedge 4\in \mathbb{Z}\right)\to A^4\in {ℝ}^{+}$$
138	38 69 137	sylancl	$$⊢A\in \left(0,1\right]\to A^4\in {ℝ}^{+}$$
139		elrp	$$⊢A^4\in {ℝ}^{+}\leftrightarrow \left(A^4\in ℝ\wedge 0<A^4\right)$$
140		ltmul2	$$⊢\left(\frac{4+1}{4!\cdot 4}\in ℝ\wedge \frac{1}{6}\in ℝ\wedge \left(A^4\in ℝ\wedge 0<A^4\right)\right)\to \left(\frac{4+1}{4!\cdot 4}<\frac{1}{6}\leftrightarrow A^4\left(\frac{4+1}{4!\cdot 4}\right)<A^4\left(\frac{1}{6}\right)\right)$$
141	24 131 140	mp3an12	$$⊢\left(A^4\in ℝ\wedge 0<A^4\right)\to \left(\frac{4+1}{4!\cdot 4}<\frac{1}{6}\leftrightarrow A^4\left(\frac{4+1}{4!\cdot 4}\right)<A^4\left(\frac{1}{6}\right)\right)$$
142	139 141	sylbi	$$⊢A^4\in {ℝ}^{+}\to \left(\frac{4+1}{4!\cdot 4}<\frac{1}{6}\leftrightarrow A^4\left(\frac{4+1}{4!\cdot 4}\right)<A^4\left(\frac{1}{6}\right)\right)$$
143	138 142	syl	$$⊢A\in \left(0,1\right]\to \left(\frac{4+1}{4!\cdot 4}<\frac{1}{6}\leftrightarrow A^4\left(\frac{4+1}{4!\cdot 4}\right)<A^4\left(\frac{1}{6}\right)\right)$$
144	136 143	mpbii	$$⊢A\in \left(0,1\right]\to A^4\left(\frac{4+1}{4!\cdot 4}\right)<A^4\left(\frac{1}{6}\right)$$
145	16	recnd	$$⊢A\in \left(0,1\right]\to A^4\in ℂ$$
146		divrec	$$⊢\left(A^4\in ℂ\wedge 6\in ℂ\wedge 6\ne 0\right)\to \frac{A^4}{6}=A^4\left(\frac{1}{6}\right)$$
147	105 129 146	mp3an23	$$⊢A^4\in ℂ\to \frac{A^4}{6}=A^4\left(\frac{1}{6}\right)$$
148	145 147	syl	$$⊢A\in \left(0,1\right]\to \frac{A^4}{6}=A^4\left(\frac{1}{6}\right)$$
149	144 148	breqtrrd	$$⊢A\in \left(0,1\right]\to A^4\left(\frac{4+1}{4!\cdot 4}\right)<\frac{A^4}{6}$$
150	14 26 29 52 149	lelttrd	$$⊢A\in \left(0,1\right]\to \left|\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)\right|<\frac{A^4}{6}$$