Theorem cos01bndlem2 7470

Description: Lemma for cos01bnd 7473.

Hypothesis

Ref	Expression
sin01bndlem2.1	|- F = {<.j, y>. | (j e. NN0 /\ y = (((i x. A)^j) / (!` j)))}

Assertion

Ref	Expression
cos01bndlem2	|- (A e. (0(,]1) -> (abs` (Re` sum_k e. (ZZ>` 4)(F` k))) < ((A^2) / 6))

Distinct variable groups:   A,j,k,y   k,F

Proof of Theorem cos01bndlem2

Step	Hyp	Ref	Expression
1		0re 5440	. . . . . . . . 9 |- 0 e. RR
2		1re 5435	. . . . . . . . 9 |- 1 e. RR
3		elioc2t 6390	. . . . . . . . 9 |- ((0 e. RR /\ 1 e. RR) -> (A e. (0(,]1) <-> (A e. RR /\ 0 < A /\ A <_ 1)))
4	1, 2, 3	mp2an 697	. . . . . . . 8 |- (A e. (0(,]1) <-> (A e. RR /\ 0 < A /\ A <_ 1))
5	4	biimp 151	. . . . . . 7 |- (A e. (0(,]1) -> (A e. RR /\ 0 < A /\ A <_ 1))
6	5	3simp1d 794	. . . . . 6 |- (A e. (0(,]1) -> A e. RR)
7	6	recnd 5315	. . . . 5 |- (A e. (0(,]1) -> A e. CC)
8		axicn 5270	. . . . . 6 |- i e. CC
9		axmulcl 5273	. . . . . 6 |- ((i e. CC /\ A e. CC) -> (i x. A) e. CC)
10	8, 9	mpan 695	. . . . 5 |- (A e. CC -> (i x. A) e. CC)
11	7, 10	syl 10	. . . 4 |- (A e. (0(,]1) -> (i x. A) e. CC)
12		4nn 6002	. . . . 5 |- 4 e. NN
13		sin01bndlem2.1	. . . . . 6 |- F = {<.j, y>. | (j e. NN0 /\ y = (((i x. A)^j) / (!` j)))}
14	13	eftlclt 7379	. . . . 5 |- (((i x. A) e. CC /\ 4 e. NN) -> sum_k e. (ZZ>` 4)(F` k) e. CC)
15	12, 14	mpan2 696	. . . 4 |- ((i x. A) e. CC -> sum_k e. (ZZ>` 4)(F` k) e. CC)
16	11, 15	syl 10	. . 3 |- (A e. (0(,]1) -> sum_k e. (ZZ>` 4)(F` k) e. CC)
17		reclt 6757	. . . 4 |- (sum_k e. (ZZ>` 4)(F` k) e. CC -> (Re` sum_k e. (ZZ>` 4)(F` k)) e. RR)
18	17	recnd 5315	. . 3 |- (sum_k e. (ZZ>` 4)(F` k) e. CC -> (Re` sum_k e. (ZZ>` 4)(F` k)) e. CC)
19		absclt 6833	. . 3 |- ((Re` sum_k e. (ZZ>` 4)(F` k)) e. CC -> (abs` (Re` sum_k e. (ZZ>` 4)(F` k))) e. RR)
20	16, 18, 19	3syl 20	. 2 |- (A e. (0(,]1) -> (abs` (Re` sum_k e. (ZZ>` 4)(F` k))) e. RR)
21	12	nnnn0 6107	. . . 4 |- 4 e. NN0
22		reexpclt 6580	. . . 4 |- ((A e. RR /\ 4 e. NN0) -> (A^4) e. RR)
23	21, 22	mpan2 696	. . 3 |- (A e. RR -> (A^4) e. RR)
24		df-5 5973	. . . . . 6 |- 5 = (4 + 1)
25	24	opreq1i 3971	. . . . 5 |- (5 / ((!` 4) x. 4)) = ((4 + 1) / ((!` 4) x. 4))
26		eftlubclt 7376	. . . . . 6 |- (4 e. NN -> ((4 + 1) / ((!` 4) x. 4)) e. RR)
27	12, 26	ax-mp 7	. . . . 5 |- ((4 + 1) / ((!` 4) x. 4)) e. RR
28	25, 27	eqeltr 1544	. . . 4 |- (5 / ((!` 4) x. 4)) e. RR
29		axmulrcl 5274	. . . 4 |- (((A^4) e. RR /\ (5 / ((!` 4) x. 4)) e. RR) -> ((A^4) x. (5 / ((!` 4) x. 4))) e. RR)
30	28, 29	mpan2 696	. . 3 |- ((A^4) e. RR -> ((A^4) x. (5 / ((!` 4) x. 4))) e. RR)
31	6, 23, 30	3syl 20	. 2 |- (A e. (0(,]1) -> ((A^4) x. (5 / ((!` 4) x. 4))) e. RR)
32		resqclt 6621	. . 3 |- (A e. RR -> (A^2) e. RR)
33		6re 5984	. . . 4 |- 6 e. RR
34		6pos 5994	. . . . 5 |- 0 < 6
35	33, 34	gt0ne0i 5617	. . . 4 |- 6 =/= 0
36		redivclt 5800	. . . 4 |- (((A^2) e. RR /\ 6 e. RR /\ 6 =/= 0) -> ((A^2) / 6) e. RR)
37	33, 35, 36	mp3an23 908	. . 3 |- ((A^2) e. RR -> ((A^2) / 6) e. RR)
38	6, 32, 37	3syl 20	. 2 |- (A e. (0(,]1) -> ((A^2) / 6) e. RR)
39		eqid 1475	. . . . . 6 |- Re = Re
40	39	orci 270	. . . . 5 |- (Re = Re \/ Re = Im)
41	13, 40	abspef01tlub 7395	. . . 4 |- ((A e. (0(,]1) /\ 4 e. NN) -> (abs` (Re` sum_k e. (ZZ>` 4)(F` k))) <_ ((A^4) x. ((4 + 1) / ((!` 4) x. 4))))
42	12, 41	mpan2 696	. . 3 |- (A e. (0(,]1) -> (abs` (Re` sum_k e. (ZZ>` 4)(F` k))) <_ ((A^4) x. ((4 + 1) / ((!` 4) x. 4))))
43	25	opreq2i 3972	. . 3 |- ((A^4) x. (5 / ((!` 4) x. 4))) = ((A^4) x. ((4 + 1) / ((!` 4) x. 4)))
44	42, 43	syl6breqr 2655	. 2 |- (A e. (0(,]1) -> (abs` (Re` sum_k e. (ZZ>` 4)(F` k))) <_ ((A^4) x. (5 / ((!` 4) x. 4))))
45	6, 23	syl 10	. . . 4 |- (A e. (0(,]1) -> (A^4) e. RR)
46	33, 35	rereccl 5801	. . . . 5 |- (1 / 6) e. RR
47		axmulrcl 5274	. . . . 5 |- (((A^4) e. RR /\ (1 / 6) e. RR) -> ((A^4) x. (1 / 6)) e. RR)
48	46, 47	mpan2 696	. . . 4 |- ((A^4) e. RR -> ((A^4) x. (1 / 6)) e. RR)
49	45, 48	syl 10	. . 3 |- (A e. (0(,]1) -> ((A^4) x. (1 / 6)) e. RR)
50		sin01bndlem1 7467	. . . . . . 7 |- (5 / ((!` 4) x. 4)) < (1 / 6)
51		ltmul2t 5831	. . . . . . 7 |- ((((5 / ((!` 4) x. 4)) e. RR /\ (1 / 6) e. RR /\ (A^4) e. RR) /\ 0 < (A^4)) -> ((5 / ((!` 4) x. 4)) < (1 / 6) <-> ((A^4) x. (5 / ((!` 4) x. 4))) < ((A^4) x. (1 / 6))))
52	50, 51	mpbii 193	. . . . . 6 |- ((((5 / ((!` 4) x. 4)) e. RR /\ (1 / 6) e. RR /\ (A^4) e. RR) /\ 0 < (A^4)) -> ((A^4) x. (5 / ((!` 4) x. 4))) < ((A^4) x. (1 / 6)))
53	52	ex 373	. . . . 5 |- (((5 / ((!` 4) x. 4)) e. RR /\ (1 / 6) e. RR /\ (A^4) e. RR) -> (0 < (A^4) -> ((A^4) x. (5 / ((!` 4) x. 4))) < ((A^4) x. (1 / 6))))
54	28, 46, 53	mp3an12 906	. . . 4 |- ((A^4) e. RR -> (0 < (A^4) -> ((A^4) x. (5 / ((!` 4) x. 4))) < ((A^4) x. (1 / 6))))
55		expgt0t 6589	. . . . . 6 |- ((A e. RR /\ 4 e. NN0 /\ 0 < A) -> 0 < (A^4))
56	21, 55	mp3an2 904	. . . . 5 |- ((A e. RR /\ 0 < A) -> 0 < (A^4))
57	5	3simp2d 795	. . . . 5 |- (A e. (0(,]1) -> 0 < A)
58	56, 6, 57	sylanc 471	. . . 4 |- (A e. (0(,]1) -> 0 < (A^4))
59	54, 45, 58	sylc 68	. . 3 |- (A e. (0(,]1) -> ((A^4) x. (5 / ((!` 4) x. 4))) < ((A^4) x. (1 / 6)))
60		2nn0 6115	. . . . . . . 8 |- 2 e. NN0
61		2pos 5989	. . . . . . . . . . . 12 |- 0 < 2
62		2re 5979	. . . . . . . . . . . . 13 |- 2 e. RR
63	1, 62, 62	ltadd1 5591	. . . . . . . . . . . 12 |- (0 < 2 <-> (0 + 2) < (2 + 2))
64	61, 63	mpbi 189	. . . . . . . . . . 11 |- (0 + 2) < (2 + 2)
65		2cn 5980	. . . . . . . . . . . 12 |- 2 e. CC
66	65	addid2 5331	. . . . . . . . . . 11 |- (0 + 2) = 2
67		2p2e4 6001	. . . . . . . . . . 11 |- (2 + 2) = 4
68	64, 66, 67	3brtr3 2642	. . . . . . . . . 10 |- 2 < 4
69		expword2it 6605	. . . . . . . . . . 11 |- (((A e. RR /\ 2 e. NN0 /\ 4 e. NN0) /\ (0 < A /\ A <_ 1 /\ 2 < 4)) -> (A^4) <_ (A^2))
70	69	expcom 374	. . . . . . . . . 10 |- ((0 < A /\ A <_ 1 /\ 2 < 4) -> ((A e. RR /\ 2 e. NN0 /\ 4 e. NN0) -> (A^4) <_ (A^2)))
71	68, 70	mp3an3 905	. . . . . . . . 9 |- ((0 < A /\ A <_ 1) -> ((A e. RR /\ 2 e. NN0 /\ 4 e. NN0) -> (A^4) <_ (A^2)))
72	71	com12 11	. . . . . . . 8 |- ((A e. RR /\ 2 e. NN0 /\ 4 e. NN0) -> ((0 < A /\ A <_ 1) -> (A^4) <_ (A^2)))
73	60, 21, 72	mp3an23 908	. . . . . . 7 |- (A e. RR -> ((0 < A /\ A <_ 1) -> (A^4) <_ (A^2)))
74	73	3impib 831	. . . . . 6 |- ((A e. RR