Theorem cos01bndlem3 7471

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
cos01bndlem3	|- (A e. (0(,]1) -> ((1 - (2 x. ((A^2) / 3))) < (cos` A) /\ (cos` A) < (1 - ((A^2) / 3))))

Distinct variable group:   A,j,y

Proof of Theorem cos01bndlem3

Step	Hyp	Ref	Expression
1		ax1cn 5269	. . . . . 6 |- 1 e. CC
2		subsubt 5462	. . . . . 6 |- ((1 e. CC /\ ((A^2) / 2) e. CC /\ -u((A^2) / 6) e. CC) -> (1 - (((A^2) / 2) - -u((A^2) / 6))) = ((1 - ((A^2) / 2)) + -u((A^2) / 6)))
3	1, 2	mp3an1 903	. . . . 5 |- ((((A^2) / 2) e. CC /\ -u((A^2) / 6) e. CC) -> (1 - (((A^2) / 2) - -u((A^2) / 6))) = ((1 - ((A^2) / 2)) + -u((A^2) / 6)))
4		0re 5440	. . . . . . . . . . 11 |- 0 e. RR
5		1re 5435	. . . . . . . . . . 11 |- 1 e. RR
6		elioc2t 6390	. . . . . . . . . . 11 |- ((0 e. RR /\ 1 e. RR) -> (A e. (0(,]1) <-> (A e. RR /\ 0 < A /\ A <_ 1)))
7	4, 5, 6	mp2an 697	. . . . . . . . . 10 |- (A e. (0(,]1) <-> (A e. RR /\ 0 < A /\ A <_ 1))
8	7	biimp 151	. . . . . . . . 9 |- (A e. (0(,]1) -> (A e. RR /\ 0 < A /\ A <_ 1))
9	8	3simp1d 794	. . . . . . . 8 |- (A e. (0(,]1) -> A e. RR)
10		resqclt 6621	. . . . . . . 8 |- (A e. RR -> (A^2) e. RR)
11	9, 10	syl 10	. . . . . . 7 |- (A e. (0(,]1) -> (A^2) e. RR)
12		rehalfclt 6034	. . . . . . 7 |- ((A^2) e. RR -> ((A^2) / 2) e. RR)
13	11, 12	syl 10	. . . . . 6 |- (A e. (0(,]1) -> ((A^2) / 2) e. RR)
14	13	recnd 5315	. . . . 5 |- (A e. (0(,]1) -> ((A^2) / 2) e. CC)
15		2nn0 6115	. . . . . . . . 9 |- 2 e. NN0
16		reexpclt 6580	. . . . . . . . . 10 |- ((A e. RR /\ 2 e. NN0) -> (A^2) e. RR)
17		6re 5984	. . . . . . . . . . 11 |- 6 e. RR
18		6pos 5994	. . . . . . . . . . . 12 |- 0 < 6
19	17, 18	gt0ne0i 5617	. . . . . . . . . . 11 |- 6 =/= 0
20		redivclt 5800	. . . . . . . . . . 11 |- (((A^2) e. RR /\ 6 e. RR /\ 6 =/= 0) -> ((A^2) / 6) e. RR)
21	17, 19, 20	mp3an23 908	. . . . . . . . . 10 |- ((A^2) e. RR -> ((A^2) / 6) e. RR)
22	16, 21	syl 10	. . . . . . . . 9 |- ((A e. RR /\ 2 e. NN0) -> ((A^2) / 6) e. RR)
23	15, 22	mpan2 696	. . . . . . . 8 |- (A e. RR -> ((A^2) / 6) e. RR)
24	9, 23	syl 10	. . . . . . 7 |- (A e. (0(,]1) -> ((A^2) / 6) e. RR)
25		renegclt 5437	. . . . . . 7 |- (((A^2) / 6) e. RR -> -u((A^2) / 6) e. RR)
26	24, 25	syl 10	. . . . . 6 |- (A e. (0(,]1) -> -u((A^2) / 6) e. RR)
27	26	recnd 5315	. . . . 5 |- (A e. (0(,]1) -> -u((A^2) / 6) e. CC)
28	3, 14, 27	sylanc 471	. . . 4 |- (A e. (0(,]1) -> (1 - (((A^2) / 2) - -u((A^2) / 6))) = ((1 - ((A^2) / 2)) + -u((A^2) / 6)))
29		subnegt 5394	. . . . . . 7 |- ((((A^2) / 2) e. CC /\ ((A^2) / 6) e. CC) -> (((A^2) / 2) - -u((A^2) / 6)) = (((A^2) / 2) + ((A^2) / 6)))
30	24	recnd 5315	. . . . . . 7 |- (A e. (0(,]1) -> ((A^2) / 6) e. CC)
31	29, 14, 30	sylanc 471	. . . . . 6 |- (A e. (0(,]1) -> (((A^2) / 2) - -u((A^2) / 6)) = (((A^2) / 2) + ((A^2) / 6)))
32	11	recnd 5315	. . . . . . 7 |- (A e. (0(,]1) -> (A^2) e. CC)
33		2cn 5980	. . . . . . . . . 10 |- 2 e. CC
34		2ne0 5990	. . . . . . . . . 10 |- 2 =/= 0
35		divrect 5739	. . . . . . . . . 10 |- (((A^2) e. CC /\ 2 e. CC /\ 2 =/= 0) -> ((A^2) / 2) = ((A^2) x. (1 / 2)))
36	33, 34, 35	mp3an23 908	. . . . . . . . 9 |- ((A^2) e. CC -> ((A^2) / 2) = ((A^2) x. (1 / 2)))
37	17	recn 5314	. . . . . . . . . 10 |- 6 e. CC
38		divrect 5739	. . . . . . . . . 10 |- (((A^2) e. CC /\ 6 e. CC /\ 6 =/= 0) -> ((A^2) / 6) = ((A^2) x. (1 / 6)))
39	37, 19, 38	mp3an23 908	. . . . . . . . 9 |- ((A^2) e. CC -> ((A^2) / 6) = ((A^2) x. (1 / 6)))
40	36, 39	opreq12d 3978	. . . . . . . 8 |- ((A^2) e. CC -> (((A^2) / 2) + ((A^2) / 6)) = (((A^2) x. (1 / 2)) + ((A^2) x. (1 / 6))))
41	33, 34	reccl 5713	. . . . . . . . . 10 |- (1 / 2) e. CC
42	37, 19	reccl 5713	. . . . . . . . . 10 |- (1 / 6) e. CC
43		axdistr 5279	. . . . . . . . . 10 |- (((A^2) e. CC /\ (1 / 2) e. CC /\ (1 / 6) e. CC) -> ((A^2) x. ((1 / 2) + (1 / 6))) = (((A^2) x. (1 / 2)) + ((A^2) x. (1 / 6))))
44	41, 42, 43	mp3an23 908	. . . . . . . . 9 |- ((A^2) e. CC -> ((A^2) x. ((1 / 2) + (1 / 6))) = (((A^2) x. (1 / 2)) + ((A^2) x. (1 / 6))))
45		halfpm6th 6032	. . . . . . . . . . 11 |- (((1 / 2) - (1 / 6)) = (1 / 3) /\ ((1 / 2) + (1 / 6)) = (2 / 3))
46	45	pm3.27i 324	. . . . . . . . . 10 |- ((1 / 2) + (1 / 6)) = (2 / 3)
47	46	opreq2i 3972	. . . . . . . . 9 |- ((A^2) x. ((1 / 2) + (1 / 6))) = ((A^2) x. (2 / 3))
48	44, 47	syl5eqr 1521	. . . . . . . 8 |- ((A^2) e. CC -> ((A^2) x. (2 / 3)) = (((A^2) x. (1 / 2)) + ((A^2) x. (1 / 6))))
49		3re 5981	. . . . . . . . . 10 |- 3 e. RR
50	49	recn 5314	. . . . . . . . 9 |- 3 e. CC
51		3pos 5991	. . . . . . . . . . 11 |- 0 < 3
52	49, 51	gt0ne0i 5617	. . . . . . . . . 10 |- 3 =/= 0
53		div12t 5744	. . . . . . . . . 10 |- ((((A^2) e. CC /\ 2 e. CC /\ 3 e. CC) /\ 3 =/= 0) -> ((A^2) x. (2 / 3)) = (2 x. ((A^2) / 3)))
54	52, 53	mpan2 696	. . . . . . . . 9 |- (((A^2) e. CC /\ 2 e. CC /\ 3 e. CC) -> ((A^2) x. (2 / 3)) = (2 x. ((A^2) / 3)))
55	33, 50, 54	mp3an23 908	. . . . . . . 8 |- ((A^2) e. CC -> ((A^2) x. (2 / 3)) = (2 x. ((A^2) / 3)))
56	40, 48, 55	3eqtr2d 1513	. . . . . . 7 |- ((A^2) e. CC -> (((A^2) / 2) + ((A^2) / 6)) = (2 x. ((A^2) / 3)))
57	32, 56	syl 10	. . . . . 6 |- (A e. (0(,]1) -> (((A^2) / 2) + ((A^2) / 6)) = (2 x. ((A^2) / 3)))
58	31, 57	eqtrd 1507	. . . . 5 |- (A e. (0(,]1) -> (((A^2) / 2) - -u((A^2) / 6)) = (2 x. ((A^2) / 3)))
59	58	opreq2d 3976	. . . 4 |- (A e. (0(,]1) -> (1 - (((A^2) / 2) - -u((A^2) / 6))) = (1 - (2 x. ((A^2) / 3))))
60	28, 59	eqtr3d 1509	. . 3 |- (A e. (0(,]1) -> ((1 - ((A^2) / 2)) + -u((A^2) / 6)) = (1 - (2 x. ((A^2) / 3))))
61		sin01bndlem2.1	. . . . . . . 8 |- F = {<.j, y>. | (j e. NN0 /\ y = (((i x. A)^j) / (!` j)))}
62	61	cos01bndlem2 7470	. . . . . . 7 |- (A e. (0(,]1) -> (abs` (Re` sum_k e. (ZZ>` 4)(F` k))) < ((A^2) / 6))
63		absltt 6880	. . . . . . . 8 |- (((Re` sum_k e. (ZZ>` 4)(F` k)) e. RR /\ ((A^2) / 6) e. RR) -> ((abs` (Re` sum_k e. (ZZ>` 4)(F` k))) < ((A^2) / 6) <-> (-u((A^2) / 6) < (Re` sum_