Metamath Proof Explorer

Theorem ef01bndlem

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

Ref Expression
Hypothesis ef01bnd.1 
|- F = ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) )
Assertion ef01bndlem 
|- ( A e. ( 0 (,] 1 ) -> ( abs ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) < ( ( A ^ 4 ) / 6 ) )

Proof

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