Theorem sin01bndlem2 7418

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
sin01bndlem2	|- (A e. (0(,]1) -> (abs` (Im` sum_k e. (ZZ>` 4)(F` k))) < ((A^3) / 6))

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

Proof of Theorem sin01bndlem2

Step	Hyp	Ref	Expression
1		0re 5420	. . . . . . . . 9 |- 0 e. RR
2		1re 5415	. . . . . . . . 9 |- 1 e. RR
3		elioc2t 6330	. . . . . . . . 9 |- ((0 e. RR /\ 1 e. RR) -> (A e. (0(,]1) <-> (A e. RR /\ 0 < A /\ A <_ 1)))
4	1, 2, 3	mp2an 696	. . . . . . . 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 793	. . . . . 6 |- (A e. (0(,]1) -> A e. RR)
7	6	recnd 5295	. . . . 5 |- (A e. (0(,]1) -> A e. CC)
8		axicn 5250	. . . . . 6 |- i e. CC
9		axmulcl 5253	. . . . . 6 |- ((i e. CC /\ A e. CC) -> (i x. A) e. CC)
10	8, 9	mpan 694	. . . . 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 5957	. . . . 5 |- 4 e. NN
13		sin01bndlem2.1	. . . . . 6 |- F = {<.j, y>. | (j e. NN0 /\ y = (((i x. A)^j) / (!` j)))}
14	13	eftlclt 7329	. . . . 5 |- (((i x. A) e. CC /\ 4 e. NN) -> sum_k e. (ZZ>` 4)(F` k) e. CC)
15	12, 14	mpan2 695	. . . 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		imclt 6697	. . . 4 |- (sum_k e. (ZZ>` 4)(F` k) e. CC -> (Im` sum_k e. (ZZ>` 4)(F` k)) e. RR)
18	17	recnd 5295	. . 3 |- (sum_k e. (ZZ>` 4)(F` k) e. CC -> (Im` sum_k e. (ZZ>` 4)(F` k)) e. CC)
19		absclt 6776	. . 3 |- ((Im` sum_k e. (ZZ>` 4)(F` k)) e. CC -> (abs` (Im` sum_k e. (ZZ>` 4)(F` k))) e. RR)
20	16, 18, 19	3syl 20	. 2 |- (A e. (0(,]1) -> (abs` (Im` sum_k e. (ZZ>` 4)(F` k))) e. RR)
21	12	nnnn0 6062	. . . 4 |- 4 e. NN0
22		reexpclt 6520	. . . 4 |- ((A e. RR /\ 4 e. NN0) -> (A^4) e. RR)
23	21, 22	mpan2 695	. . 3 |- (A e. RR -> (A^4) e. RR)
24		df-5 5928	. . . . . 6 |- 5 = (4 + 1)
25	24	opreq1i 3962	. . . . 5 |- (5 / ((!` 4) x. 4)) = ((4 + 1) / ((!` 4) x. 4))
26		eftlubclt 7326	. . . . . 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 1541	. . . 4 |- (5 / ((!` 4) x. 4)) e. RR
29		axmulrcl 5254	. . . 4 |- (((A^4) e. RR /\ (5 / ((!` 4) x. 4)) e. RR) -> ((A^4) x. (5 / ((!` 4) x. 4))) e. RR)
30	28, 29	mpan2 695	. . 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		3nn 5955	. . . . 5 |- 3 e. NN
33	32	nnnn0 6062	. . . 4 |- 3 e. NN0
34		reexpclt 6520	. . . 4 |- ((A e. RR /\ 3 e. NN0) -> (A^3) e. RR)
35	33, 34	mpan2 695	. . 3 |- (A e. RR -> (A^3) e. RR)
36		6re 5939	. . . 4 |- 6 e. RR
37		6pos 5949	. . . . 5 |- 0 < 6
38	36, 37	gt0ne0i 5599	. . . 4 |- 6 =/= 0
39		redivclt 5764	. . . 4 |- (((A^3) e. RR /\ 6 e. RR /\ 6 =/= 0) -> ((A^3) / 6) e. RR)
40	36, 38, 39	mp3an23 906	. . 3 |- ((A^3) e. RR -> ((A^3) / 6) e. RR)
41	6, 35, 40	3syl 20	. 2 |- (A e. (0(,]1) -> ((A^3) / 6) e. RR)
42		eqid 1473	. . . . . 6 |- Im = Im
43	42	olci 271	. . . . 5 |- (Im = Re \/ Im = Im)
44	13, 43	abspef01tlub 7344	. . . 4 |- ((A e. (0(,]1) /\ 4 e. NN) -> (abs` (Im` sum_k e. (ZZ>` 4)(F` k))) <_ ((A^4) x. ((4 + 1) / ((!` 4) x. 4))))
45	12, 44	mpan2 695	. . 3 |- (A e. (0(,]1) -> (abs` (Im` sum_k e. (ZZ>` 4)(F` k))) <_ ((A^4) x. ((4 + 1) / ((!` 4) x. 4))))
46	25	opreq2i 3963	. . 3 |- ((A^4) x. (5 / ((!` 4) x. 4))) = ((A^4) x. ((4 + 1) / ((!` 4) x. 4)))
47	45, 46	syl6breqr 2650	. 2 |- (A e. (0(,]1) -> (abs` (Im` sum_k e. (ZZ>` 4)(F` k))) <_ ((A^4) x. (5 / ((!` 4) x. 4))))
48	6, 23	syl 10	. . . 4 |- (A e. (0(,]1) -> (A^4) e. RR)
49	36, 38	rereccl 5765	. . . . 5 |- (1 / 6) e. RR
50		axmulrcl 5254	. . . . 5 |- (((A^4) e. RR /\ (1 / 6) e. RR) -> ((A^4) x. (1 / 6)) e. RR)
51	49, 50	mpan2 695	. . . 4 |- ((A^4) e. RR -> ((A^4) x. (1 / 6)) e. RR)
52	48, 51	syl 10	. . 3 |- (A e. (0(,]1) -> ((A^4) x. (1 / 6)) e. RR)
53		sin01bndlem1 7417	. . . . . . 7 |- (5 / ((!` 4) x. 4)) < (1 / 6)
54		ltmul2t 5795	. . . . . . 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))))
55	53, 54	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)))
56	55	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))))
57	28, 49, 56	mp3an12 904	. . . 4 |- ((A^4) e. RR -> (0 < (A^4) -> ((A^4) x. (5 / ((!` 4) x. 4))) < ((A^4) x. (1 / 6))))
58		expgt0t 6528	. . . . . 6 |- ((A e. RR /\ 4 e. NN0 /\ 0 < A) -> 0 < (A^4))
59	21, 58	mp3an2 902	. . . . 5 |- ((A e. RR /\ 0 < A) -> 0 < (A^4))
60	5	3simp2d 794	. . . . 5 |- (A e. (0(,]1) -> 0 < A)
61	59, 6, 60	sylanc 471	. . . 4 |- (A e. (0(,]1) -> 0 < (A^4))
62	57, 48, 61	sylc 68	. . 3 |- (A e. (0(,]1) -> ((A^4) x. (5 / ((!` 4) x. 4))) < ((A^4) x. (1 / 6)))
63		3re 5936	. . . . . . . . . . . 12 |- 3 e. RR
64	63	ltp1 5777	. . . . . . . . . . 11 |- 3 < (3 + 1)
65		df-4 5927	. . . . . . . . . . 11 |- 4 = (3 + 1)
66	64, 65	breqtrr 2635	. . . . . . . . . 10 |- 3 < 4
67		expword2it 6544	. . . . . . . . . . 11 |- (((A e. RR /\ 3 e. NN0 /\ 4 e. NN0) /\ (0 < A /\ A <_ 1 /\ 3 < 4)) -> (A^4) <_ (A^3))
68	67	expcom 374	. . . . . . . . . 10 |- ((0 < A /\ A <_ 1 /\ 3 < 4) -> ((A e. RR /\ 3 e. NN0 /\ 4 e. NN0) -> (A^4) <_ (A^3)))
69	66, 68	mp3an3 903	. . . . . . . . 9 |- ((0 < A /\ A <_ 1) -> ((A e. RR /\ 3 e. NN0 /\ 4 e. NN0) -> (A^4) <_ (A^3)))
70	69	com12 11	. . . . . . . 8 |- ((A e. RR /\ 3 e. NN0 /\ 4 e. NN0) -> ((0 < A /\ A <_ 1) -> (A^4) <_ (A^3)))
71	33, 21, 70	mp3an23 906	. . . . . . 7 |- (A e. RR -> ((0 < A /\ A <_ 1) -> (A^4) <_ (A^3)))
72	71	3impib 830	. . . . . 6 |- ((A e. RR /\ 0 < A /\ A <_ 1) -> (A^4) <_ (A^3)