Theorem sin01bndlem3 7419

Description: Lemma for sin01bnd 7422.

Hypothesis

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

Assertion

Ref	Expression
sin01bndlem3	|- (A e. (0(,]1) -> ((A - ((A^3) / 3)) < (sin` A) /\ (sin` A) < A))

Distinct variable group:   A,j,y

Proof of Theorem sin01bndlem3

Step	Hyp	Ref	Expression
1		subsubt 5442	. . . . 5 |- ((A e. CC /\ ((A^3) / 6) e. CC /\ -u((A^3) / 6) e. CC) -> (A - (((A^3) / 6) - -u((A^3) / 6))) = ((A - ((A^3) / 6)) + -u((A^3) / 6)))
2		0re 5420	. . . . . . . . 9 |- 0 e. RR
3		1re 5415	. . . . . . . . 9 |- 1 e. RR
4		elioc2t 6330	. . . . . . . . 9 |- ((0 e. RR /\ 1 e. RR) -> (A e. (0(,]1) <-> (A e. RR /\ 0 < A /\ A <_ 1)))
5	2, 3, 4	mp2an 696	. . . . . . . 8 |- (A e. (0(,]1) <-> (A e. RR /\ 0 < A /\ A <_ 1))
6	5	biimp 151	. . . . . . 7 |- (A e. (0(,]1) -> (A e. RR /\ 0 < A /\ A <_ 1))
7	6	3simp1d 793	. . . . . 6 |- (A e. (0(,]1) -> A e. RR)
8	7	recnd 5295	. . . . 5 |- (A e. (0(,]1) -> A e. CC)
9		3nn 5955	. . . . . . . . 9 |- 3 e. NN
10	9	nnnn0 6062	. . . . . . . 8 |- 3 e. NN0
11		reexpclt 6520	. . . . . . . . 9 |- ((A e. RR /\ 3 e. NN0) -> (A^3) e. RR)
12		6re 5939	. . . . . . . . . 10 |- 6 e. RR
13		6pos 5949	. . . . . . . . . . 11 |- 0 < 6
14	12, 13	gt0ne0i 5599	. . . . . . . . . 10 |- 6 =/= 0
15		redivclt 5764	. . . . . . . . . 10 |- (((A^3) e. RR /\ 6 e. RR /\ 6 =/= 0) -> ((A^3) / 6) e. RR)
16	12, 14, 15	mp3an23 906	. . . . . . . . 9 |- ((A^3) e. RR -> ((A^3) / 6) e. RR)
17	11, 16	syl 10	. . . . . . . 8 |- ((A e. RR /\ 3 e. NN0) -> ((A^3) / 6) e. RR)
18	10, 17	mpan2 695	. . . . . . 7 |- (A e. RR -> ((A^3) / 6) e. RR)
19	7, 18	syl 10	. . . . . 6 |- (A e. (0(,]1) -> ((A^3) / 6) e. RR)
20	19	recnd 5295	. . . . 5 |- (A e. (0(,]1) -> ((A^3) / 6) e. CC)
21		renegclt 5417	. . . . . . 7 |- (((A^3) / 6) e. RR -> -u((A^3) / 6) e. RR)
22	19, 21	syl 10	. . . . . 6 |- (A e. (0(,]1) -> -u((A^3) / 6) e. RR)
23	22	recnd 5295	. . . . 5 |- (A e. (0(,]1) -> -u((A^3) / 6) e. CC)
24	1, 8, 20, 23	syl3anc 857	. . . 4 |- (A e. (0(,]1) -> (A - (((A^3) / 6) - -u((A^3) / 6))) = ((A - ((A^3) / 6)) + -u((A^3) / 6)))
25		subnegt 5374	. . . . . . 7 |- ((((A^3) / 6) e. CC /\ ((A^3) / 6) e. CC) -> (((A^3) / 6) - -u((A^3) / 6)) = (((A^3) / 6) + ((A^3) / 6)))
26	25, 20, 20	sylanc 471	. . . . . 6 |- (A e. (0(,]1) -> (((A^3) / 6) - -u((A^3) / 6)) = (((A^3) / 6) + ((A^3) / 6)))
27		2timest 5959	. . . . . . 7 |- (((A^3) / 6) e. CC -> (2 x. ((A^3) / 6)) = (((A^3) / 6) + ((A^3) / 6)))
28	20, 27	syl 10	. . . . . 6 |- (A e. (0(,]1) -> (2 x. ((A^3) / 6)) = (((A^3) / 6) + ((A^3) / 6)))
29		2cn 5935	. . . . . . . . . . 11 |- 2 e. CC
30	29	mulid1 5312	. . . . . . . . . 10 |- (2 x. 1) = 2
31		3re 5936	. . . . . . . . . . . . 13 |- 3 e. RR
32	31	recn 5294	. . . . . . . . . . . 12 |- 3 e. CC
33	32, 29	mulcom 5303	. . . . . . . . . . 11 |- (3 x. 2) = (2 x. 3)
34		3t2e6 5978	. . . . . . . . . . 11 |- (3 x. 2) = 6
35	33, 34	eqtr3 1494	. . . . . . . . . 10 |- (2 x. 3) = 6
36	30, 35	opreq12i 3964	. . . . . . . . 9 |- ((2 x. 1) / (2 x. 3)) = (2 / 6)
37		2ne0 5945	. . . . . . . . . 10 |- 2 =/= 0
38		3pos 5946	. . . . . . . . . . . 12 |- 0 < 3
39	31, 38	gt0ne0i 5599	. . . . . . . . . . 11 |- 3 =/= 0
40		ax1cn 5249	. . . . . . . . . . . 12 |- 1 e. CC
41		divcan5t 5745	. . . . . . . . . . . 12 |- ((1 e. CC /\ (3 e. CC /\ 3 =/= 0) /\ (2 e. CC /\ 2 =/= 0)) -> ((2 x. 1) / (2 x. 3)) = (1 / 3))
42	40, 41	mp3an1 901	. . . . . . . . . . 11 |- (((3 e. CC /\ 3 =/= 0) /\ (2 e. CC /\ 2 =/= 0)) -> ((2 x. 1) / (2 x. 3)) = (1 / 3))
43	32, 39, 42	mpanl12 707	. . . . . . . . . 10 |- ((2 e. CC /\ 2 =/= 0) -> ((2 x. 1) / (2 x. 3)) = (1 / 3))
44	29, 37, 43	mp2an 696	. . . . . . . . 9 |- ((2 x. 1) / (2 x. 3)) = (1 / 3)
45	36, 44	eqtr3 1494	. . . . . . . 8 |- (2 / 6) = (1 / 3)
46	45	opreq2i 3963	. . . . . . 7 |- ((A^3) x. (2 / 6)) = ((A^3) x. (1 / 3))
47	10, 11	mpan2 695	. . . . . . . . . 10 |- (A e. RR -> (A^3) e. RR)
48	7, 47	syl 10	. . . . . . . . 9 |- (A e. (0(,]1) -> (A^3) e. RR)
49	48	recnd 5295	. . . . . . . 8 |- (A e. (0(,]1) -> (A^3) e. CC)
50	12	recn 5294	. . . . . . . . 9 |- 6 e. CC
51		div12t 5715	. . . . . . . . . 10 |- (((2 e. CC /\ (A^3) e. CC /\ 6 e. CC) /\ 6 =/= 0) -> (2 x. ((A^3) / 6)) = ((A^3) x. (2 / 6)))
52	14, 51	mpan2 695	. . . . . . . . 9 |- ((2 e. CC /\ (A^3) e. CC /\ 6 e. CC) -> (2 x. ((A^3) / 6)) = ((A^3) x. (2 / 6)))
53	29, 50, 52	mp3an13 905	. . . . . . . 8 |- ((A^3) e. CC -> (2 x. ((A^3) / 6)) = ((A^3) x. (2 / 6)))
54	49, 53	syl 10	. . . . . . 7 |- (A e. (0(,]1) -> (2 x. ((A^3) / 6)) = ((A^3) x. (2 / 6)))
55		divrect 5710	. . . . . . . . 9 |- (((A^3) e. CC /\ 3 e. CC /\ 3 =/= 0) -> ((A^3) / 3) = ((A^3) x. (1 / 3)))
56	32, 39, 55	mp3an23 906	. . . . . . . 8 |- ((A^3) e. CC -> ((A^3) / 3) = ((A^3) x. (1 / 3)))
57	49, 56	syl 10	. . . . . . 7 |- (A e. (0(,]1) -> ((A^3) / 3) = ((A^3) x. (1 / 3)))
58	46, 54, 57	3eqtr4a 1529	. . . . . 6 |- (A e. (0(,]1) -> (2 x. ((A^3) / 6)) = ((A^3) / 3))
59	26, 28, 58	3eqtr2d 1510	. . . . 5 |- (A e. (0(,]1) -> (((A^3) / 6) - -u((A^3) / 6)) = ((A^3) / 3))
60	59	opreq2d 3967	. . . 4 |- (A e. (0(,]1) -> (A - (((A^3) / 6) - -u((A^3) / 6))) = (A - ((A^3) / 3)))
61	24, 60	eqtr3d 1506	. . 3 |- (A e. (0(,]1) -> ((A - ((A^3) / 6)) + -u((A^3) / 6)) = (A - ((A^3) / 3)))
62		sin01bndlem2.1	. . . . . . . 8 |- F = {<.j, y>. | (j e. NN0 /\ y = (((i x. A)^j) / (!` j)))}
63	62	sin01bndlem2 7418	. . . . . . 7 |- (A e. (0(,]1) -> (abs` (Im` sum_k e. (ZZ>` 4)(F` k))) < ((A^3) / 6))
64		absltt 6825	. . . . . . . 8 |- (((Im` sum_k e. (ZZ>` 4)(F` k)) e. RR /\ ((A^3) / 6) e. RR) -> ((abs` (Im` sum_k e. (ZZ>` 4)(F` k))) < ((A^3) / 6) <-> (-u((A^3) / 6) < (Im` sum_k e. (ZZ>` 4)(F` k)) /\ (Im` sum_k e. (ZZ>` 4)(F` k)) < ((A^3) / 6))))
65		axicn 5250	. . . . . . . . . . . 12 |- i e. CC
66		axmulcl 5253	. . . . . . . . . . . 12 |- ((i e. CC /\ A e. CC) -> (i x. A) e. CC)
67	65, 66	mpan 694	. . . . . . . . . . 11 |- (A e. CC -> (i x. A) e. CC)
68	8, 67	syl 10	. . . . . . . . . 10 |- (A e. (0(,]1) -> (i x. A) e. CC)
69		4nn 5957	. . . . . . . . . . 11 |- 4 e. NN
70	62	eftlclt 7329	. . . . . . . . . . 11 |- (((i x. A) e. CC /\ 4 e. NN) -> sum_k e. (ZZ>` 4)(F` k) e. CC)
71	69, 70	mpan2 695	. . . . . . . . . 10 |- ((i x. A) e. CC -> sum_k e. (ZZ>` 4)(F` k) e. CC)
72	68, 71	syl 10	. . . . . . . . 9 |- (A e. (0(,]1) -> sum_k e. (ZZ>` 4)(F` k) e. CC)
73		imclt 6697	. . . . . . . . 9 |- (sum_k e. (ZZ>` 4)(F` k) e. CC -> (Im` sum_k e. (ZZ>` 4