Step |
Hyp |
Ref |
Expression |
1 |
|
sinccvg.1 |
|- ( ph -> F : NN --> ( RR \ { 0 } ) ) |
2 |
|
sinccvg.2 |
|- ( ph -> F ~~> 0 ) |
3 |
|
sinccvg.3 |
|- G = ( x e. ( RR \ { 0 } ) |-> ( ( sin ` x ) / x ) ) |
4 |
|
sinccvg.4 |
|- H = ( x e. CC |-> ( 1 - ( ( x ^ 2 ) / 3 ) ) ) |
5 |
|
sinccvg.5 |
|- ( ph -> M e. NN ) |
6 |
|
sinccvg.6 |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( abs ` ( F ` k ) ) < 1 ) |
7 |
|
eqid |
|- ( ZZ>= ` M ) = ( ZZ>= ` M ) |
8 |
5
|
nnzd |
|- ( ph -> M e. ZZ ) |
9 |
4
|
funmpt2 |
|- Fun H |
10 |
|
nnex |
|- NN e. _V |
11 |
|
fex |
|- ( ( F : NN --> ( RR \ { 0 } ) /\ NN e. _V ) -> F e. _V ) |
12 |
1 10 11
|
sylancl |
|- ( ph -> F e. _V ) |
13 |
|
cofunexg |
|- ( ( Fun H /\ F e. _V ) -> ( H o. F ) e. _V ) |
14 |
9 12 13
|
sylancr |
|- ( ph -> ( H o. F ) e. _V ) |
15 |
1
|
adantr |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> F : NN --> ( RR \ { 0 } ) ) |
16 |
|
eluznn |
|- ( ( M e. NN /\ k e. ( ZZ>= ` M ) ) -> k e. NN ) |
17 |
5 16
|
sylan |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> k e. NN ) |
18 |
15 17
|
ffvelrnd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. ( RR \ { 0 } ) ) |
19 |
|
eldifsn |
|- ( ( F ` k ) e. ( RR \ { 0 } ) <-> ( ( F ` k ) e. RR /\ ( F ` k ) =/= 0 ) ) |
20 |
18 19
|
sylib |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( F ` k ) e. RR /\ ( F ` k ) =/= 0 ) ) |
21 |
20
|
simpld |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. RR ) |
22 |
21
|
recnd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. CC ) |
23 |
|
ax-1cn |
|- 1 e. CC |
24 |
|
sqcl |
|- ( x e. CC -> ( x ^ 2 ) e. CC ) |
25 |
|
3cn |
|- 3 e. CC |
26 |
|
3ne0 |
|- 3 =/= 0 |
27 |
|
divcl |
|- ( ( ( x ^ 2 ) e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> ( ( x ^ 2 ) / 3 ) e. CC ) |
28 |
25 26 27
|
mp3an23 |
|- ( ( x ^ 2 ) e. CC -> ( ( x ^ 2 ) / 3 ) e. CC ) |
29 |
24 28
|
syl |
|- ( x e. CC -> ( ( x ^ 2 ) / 3 ) e. CC ) |
30 |
|
subcl |
|- ( ( 1 e. CC /\ ( ( x ^ 2 ) / 3 ) e. CC ) -> ( 1 - ( ( x ^ 2 ) / 3 ) ) e. CC ) |
31 |
23 29 30
|
sylancr |
|- ( x e. CC -> ( 1 - ( ( x ^ 2 ) / 3 ) ) e. CC ) |
32 |
4 31
|
fmpti |
|- H : CC --> CC |
33 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
34 |
33
|
cnfldtopon |
|- ( TopOpen ` CCfld ) e. ( TopOn ` CC ) |
35 |
34
|
a1i |
|- ( T. -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) |
36 |
|
1cnd |
|- ( T. -> 1 e. CC ) |
37 |
35 35 36
|
cnmptc |
|- ( T. -> ( x e. CC |-> 1 ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) ) |
38 |
33
|
sqcn |
|- ( x e. CC |-> ( x ^ 2 ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) |
39 |
38
|
a1i |
|- ( T. -> ( x e. CC |-> ( x ^ 2 ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) ) |
40 |
33
|
divccn |
|- ( ( 3 e. CC /\ 3 =/= 0 ) -> ( y e. CC |-> ( y / 3 ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) ) |
41 |
25 26 40
|
mp2an |
|- ( y e. CC |-> ( y / 3 ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) |
42 |
41
|
a1i |
|- ( T. -> ( y e. CC |-> ( y / 3 ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) ) |
43 |
|
oveq1 |
|- ( y = ( x ^ 2 ) -> ( y / 3 ) = ( ( x ^ 2 ) / 3 ) ) |
44 |
35 39 35 42 43
|
cnmpt11 |
|- ( T. -> ( x e. CC |-> ( ( x ^ 2 ) / 3 ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) ) |
45 |
33
|
subcn |
|- - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) |
46 |
45
|
a1i |
|- ( T. -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) ) |
47 |
35 37 44 46
|
cnmpt12f |
|- ( T. -> ( x e. CC |-> ( 1 - ( ( x ^ 2 ) / 3 ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) ) |
48 |
47
|
mptru |
|- ( x e. CC |-> ( 1 - ( ( x ^ 2 ) / 3 ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) |
49 |
33
|
cncfcn1 |
|- ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) |
50 |
48 4 49
|
3eltr4i |
|- H e. ( CC -cn-> CC ) |
51 |
|
cncfi |
|- ( ( H e. ( CC -cn-> CC ) /\ 0 e. CC /\ y e. RR+ ) -> E. z e. RR+ A. w e. CC ( ( abs ` ( w - 0 ) ) < z -> ( abs ` ( ( H ` w ) - ( H ` 0 ) ) ) < y ) ) |
52 |
50 51
|
mp3an1 |
|- ( ( 0 e. CC /\ y e. RR+ ) -> E. z e. RR+ A. w e. CC ( ( abs ` ( w - 0 ) ) < z -> ( abs ` ( ( H ` w ) - ( H ` 0 ) ) ) < y ) ) |
53 |
|
fvco3 |
|- ( ( F : NN --> ( RR \ { 0 } ) /\ k e. NN ) -> ( ( H o. F ) ` k ) = ( H ` ( F ` k ) ) ) |
54 |
1 53
|
sylan |
|- ( ( ph /\ k e. NN ) -> ( ( H o. F ) ` k ) = ( H ` ( F ` k ) ) ) |
55 |
17 54
|
syldan |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( H o. F ) ` k ) = ( H ` ( F ` k ) ) ) |
56 |
7 2 14 8 22 32 52 55
|
climcn1lem |
|- ( ph -> ( H o. F ) ~~> ( H ` 0 ) ) |
57 |
|
0cn |
|- 0 e. CC |
58 |
|
sq0i |
|- ( x = 0 -> ( x ^ 2 ) = 0 ) |
59 |
58
|
oveq1d |
|- ( x = 0 -> ( ( x ^ 2 ) / 3 ) = ( 0 / 3 ) ) |
60 |
25 26
|
div0i |
|- ( 0 / 3 ) = 0 |
61 |
59 60
|
eqtrdi |
|- ( x = 0 -> ( ( x ^ 2 ) / 3 ) = 0 ) |
62 |
61
|
oveq2d |
|- ( x = 0 -> ( 1 - ( ( x ^ 2 ) / 3 ) ) = ( 1 - 0 ) ) |
63 |
|
1m0e1 |
|- ( 1 - 0 ) = 1 |
64 |
62 63
|
eqtrdi |
|- ( x = 0 -> ( 1 - ( ( x ^ 2 ) / 3 ) ) = 1 ) |
65 |
|
1ex |
|- 1 e. _V |
66 |
64 4 65
|
fvmpt |
|- ( 0 e. CC -> ( H ` 0 ) = 1 ) |
67 |
57 66
|
ax-mp |
|- ( H ` 0 ) = 1 |
68 |
56 67
|
breqtrdi |
|- ( ph -> ( H o. F ) ~~> 1 ) |
69 |
3
|
funmpt2 |
|- Fun G |
70 |
|
cofunexg |
|- ( ( Fun G /\ F e. _V ) -> ( G o. F ) e. _V ) |
71 |
69 12 70
|
sylancr |
|- ( ph -> ( G o. F ) e. _V ) |
72 |
|
oveq1 |
|- ( x = ( F ` k ) -> ( x ^ 2 ) = ( ( F ` k ) ^ 2 ) ) |
73 |
72
|
oveq1d |
|- ( x = ( F ` k ) -> ( ( x ^ 2 ) / 3 ) = ( ( ( F ` k ) ^ 2 ) / 3 ) ) |
74 |
73
|
oveq2d |
|- ( x = ( F ` k ) -> ( 1 - ( ( x ^ 2 ) / 3 ) ) = ( 1 - ( ( ( F ` k ) ^ 2 ) / 3 ) ) ) |
75 |
|
ovex |
|- ( 1 - ( ( ( F ` k ) ^ 2 ) / 3 ) ) e. _V |
76 |
74 4 75
|
fvmpt |
|- ( ( F ` k ) e. CC -> ( H ` ( F ` k ) ) = ( 1 - ( ( ( F ` k ) ^ 2 ) / 3 ) ) ) |
77 |
22 76
|
syl |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( H ` ( F ` k ) ) = ( 1 - ( ( ( F ` k ) ^ 2 ) / 3 ) ) ) |
78 |
55 77
|
eqtrd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( H o. F ) ` k ) = ( 1 - ( ( ( F ` k ) ^ 2 ) / 3 ) ) ) |
79 |
|
1re |
|- 1 e. RR |
80 |
21
|
resqcld |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( F ` k ) ^ 2 ) e. RR ) |
81 |
|
3nn |
|- 3 e. NN |
82 |
|
nndivre |
|- ( ( ( ( F ` k ) ^ 2 ) e. RR /\ 3 e. NN ) -> ( ( ( F ` k ) ^ 2 ) / 3 ) e. RR ) |
83 |
80 81 82
|
sylancl |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( ( F ` k ) ^ 2 ) / 3 ) e. RR ) |
84 |
|
resubcl |
|- ( ( 1 e. RR /\ ( ( ( F ` k ) ^ 2 ) / 3 ) e. RR ) -> ( 1 - ( ( ( F ` k ) ^ 2 ) / 3 ) ) e. RR ) |
85 |
79 83 84
|
sylancr |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( 1 - ( ( ( F ` k ) ^ 2 ) / 3 ) ) e. RR ) |
86 |
78 85
|
eqeltrd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( H o. F ) ` k ) e. RR ) |
87 |
|
fvco3 |
|- ( ( F : NN --> ( RR \ { 0 } ) /\ k e. NN ) -> ( ( G o. F ) ` k ) = ( G ` ( F ` k ) ) ) |
88 |
1 87
|
sylan |
|- ( ( ph /\ k e. NN ) -> ( ( G o. F ) ` k ) = ( G ` ( F ` k ) ) ) |
89 |
17 88
|
syldan |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( G o. F ) ` k ) = ( G ` ( F ` k ) ) ) |
90 |
|
fveq2 |
|- ( x = ( F ` k ) -> ( sin ` x ) = ( sin ` ( F ` k ) ) ) |
91 |
|
id |
|- ( x = ( F ` k ) -> x = ( F ` k ) ) |
92 |
90 91
|
oveq12d |
|- ( x = ( F ` k ) -> ( ( sin ` x ) / x ) = ( ( sin ` ( F ` k ) ) / ( F ` k ) ) ) |
93 |
|
ovex |
|- ( ( sin ` ( F ` k ) ) / ( F ` k ) ) e. _V |
94 |
92 3 93
|
fvmpt |
|- ( ( F ` k ) e. ( RR \ { 0 } ) -> ( G ` ( F ` k ) ) = ( ( sin ` ( F ` k ) ) / ( F ` k ) ) ) |
95 |
18 94
|
syl |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` ( F ` k ) ) = ( ( sin ` ( F ` k ) ) / ( F ` k ) ) ) |
96 |
89 95
|
eqtrd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( G o. F ) ` k ) = ( ( sin ` ( F ` k ) ) / ( F ` k ) ) ) |
97 |
21
|
resincld |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( sin ` ( F ` k ) ) e. RR ) |
98 |
20
|
simprd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) =/= 0 ) |
99 |
97 21 98
|
redivcld |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( sin ` ( F ` k ) ) / ( F ` k ) ) e. RR ) |
100 |
96 99
|
eqeltrd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( G o. F ) ` k ) e. RR ) |
101 |
|
1cnd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> 1 e. CC ) |
102 |
83
|
recnd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( ( F ` k ) ^ 2 ) / 3 ) e. CC ) |
103 |
22
|
abscld |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( abs ` ( F ` k ) ) e. RR ) |
104 |
103
|
recnd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( abs ` ( F ` k ) ) e. CC ) |
105 |
101 102 104
|
subdird |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( 1 - ( ( ( F ` k ) ^ 2 ) / 3 ) ) x. ( abs ` ( F ` k ) ) ) = ( ( 1 x. ( abs ` ( F ` k ) ) ) - ( ( ( ( F ` k ) ^ 2 ) / 3 ) x. ( abs ` ( F ` k ) ) ) ) ) |
106 |
104
|
mulid2d |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( 1 x. ( abs ` ( F ` k ) ) ) = ( abs ` ( F ` k ) ) ) |
107 |
|
df-3 |
|- 3 = ( 2 + 1 ) |
108 |
107
|
oveq2i |
|- ( ( abs ` ( F ` k ) ) ^ 3 ) = ( ( abs ` ( F ` k ) ) ^ ( 2 + 1 ) ) |
109 |
|
2nn0 |
|- 2 e. NN0 |
110 |
|
expp1 |
|- ( ( ( abs ` ( F ` k ) ) e. CC /\ 2 e. NN0 ) -> ( ( abs ` ( F ` k ) ) ^ ( 2 + 1 ) ) = ( ( ( abs ` ( F ` k ) ) ^ 2 ) x. ( abs ` ( F ` k ) ) ) ) |
111 |
104 109 110
|
sylancl |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( abs ` ( F ` k ) ) ^ ( 2 + 1 ) ) = ( ( ( abs ` ( F ` k ) ) ^ 2 ) x. ( abs ` ( F ` k ) ) ) ) |
112 |
|
absresq |
|- ( ( F ` k ) e. RR -> ( ( abs ` ( F ` k ) ) ^ 2 ) = ( ( F ` k ) ^ 2 ) ) |
113 |
21 112
|
syl |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( abs ` ( F ` k ) ) ^ 2 ) = ( ( F ` k ) ^ 2 ) ) |
114 |
113
|
oveq1d |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( ( abs ` ( F ` k ) ) ^ 2 ) x. ( abs ` ( F ` k ) ) ) = ( ( ( F ` k ) ^ 2 ) x. ( abs ` ( F ` k ) ) ) ) |
115 |
111 114
|
eqtrd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( abs ` ( F ` k ) ) ^ ( 2 + 1 ) ) = ( ( ( F ` k ) ^ 2 ) x. ( abs ` ( F ` k ) ) ) ) |
116 |
108 115
|
syl5eq |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( abs ` ( F ` k ) ) ^ 3 ) = ( ( ( F ` k ) ^ 2 ) x. ( abs ` ( F ` k ) ) ) ) |
117 |
116
|
oveq1d |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( ( abs ` ( F ` k ) ) ^ 3 ) / 3 ) = ( ( ( ( F ` k ) ^ 2 ) x. ( abs ` ( F ` k ) ) ) / 3 ) ) |
118 |
80
|
recnd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( F ` k ) ^ 2 ) e. CC ) |
119 |
25
|
a1i |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> 3 e. CC ) |
120 |
26
|
a1i |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> 3 =/= 0 ) |
121 |
118 104 119 120
|
div23d |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( ( ( F ` k ) ^ 2 ) x. ( abs ` ( F ` k ) ) ) / 3 ) = ( ( ( ( F ` k ) ^ 2 ) / 3 ) x. ( abs ` ( F ` k ) ) ) ) |
122 |
117 121
|
eqtr2d |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( ( ( F ` k ) ^ 2 ) / 3 ) x. ( abs ` ( F ` k ) ) ) = ( ( ( abs ` ( F ` k ) ) ^ 3 ) / 3 ) ) |
123 |
106 122
|
oveq12d |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( 1 x. ( abs ` ( F ` k ) ) ) - ( ( ( ( F ` k ) ^ 2 ) / 3 ) x. ( abs ` ( F ` k ) ) ) ) = ( ( abs ` ( F ` k ) ) - ( ( ( abs ` ( F ` k ) ) ^ 3 ) / 3 ) ) ) |
124 |
105 123
|
eqtrd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( 1 - ( ( ( F ` k ) ^ 2 ) / 3 ) ) x. ( abs ` ( F ` k ) ) ) = ( ( abs ` ( F ` k ) ) - ( ( ( abs ` ( F ` k ) ) ^ 3 ) / 3 ) ) ) |
125 |
22 98
|
absrpcld |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( abs ` ( F ` k ) ) e. RR+ ) |
126 |
125
|
rpgt0d |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> 0 < ( abs ` ( F ` k ) ) ) |
127 |
|
ltle |
|- ( ( ( abs ` ( F ` k ) ) e. RR /\ 1 e. RR ) -> ( ( abs ` ( F ` k ) ) < 1 -> ( abs ` ( F ` k ) ) <_ 1 ) ) |
128 |
103 79 127
|
sylancl |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( abs ` ( F ` k ) ) < 1 -> ( abs ` ( F ` k ) ) <_ 1 ) ) |
129 |
6 128
|
mpd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( abs ` ( F ` k ) ) <_ 1 ) |
130 |
|
0xr |
|- 0 e. RR* |
131 |
|
elioc2 |
|- ( ( 0 e. RR* /\ 1 e. RR ) -> ( ( abs ` ( F ` k ) ) e. ( 0 (,] 1 ) <-> ( ( abs ` ( F ` k ) ) e. RR /\ 0 < ( abs ` ( F ` k ) ) /\ ( abs ` ( F ` k ) ) <_ 1 ) ) ) |
132 |
130 79 131
|
mp2an |
|- ( ( abs ` ( F ` k ) ) e. ( 0 (,] 1 ) <-> ( ( abs ` ( F ` k ) ) e. RR /\ 0 < ( abs ` ( F ` k ) ) /\ ( abs ` ( F ` k ) ) <_ 1 ) ) |
133 |
103 126 129 132
|
syl3anbrc |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( abs ` ( F ` k ) ) e. ( 0 (,] 1 ) ) |
134 |
|
sin01bnd |
|- ( ( abs ` ( F ` k ) ) e. ( 0 (,] 1 ) -> ( ( ( abs ` ( F ` k ) ) - ( ( ( abs ` ( F ` k ) ) ^ 3 ) / 3 ) ) < ( sin ` ( abs ` ( F ` k ) ) ) /\ ( sin ` ( abs ` ( F ` k ) ) ) < ( abs ` ( F ` k ) ) ) ) |
135 |
133 134
|
syl |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( ( abs ` ( F ` k ) ) - ( ( ( abs ` ( F ` k ) ) ^ 3 ) / 3 ) ) < ( sin ` ( abs ` ( F ` k ) ) ) /\ ( sin ` ( abs ` ( F ` k ) ) ) < ( abs ` ( F ` k ) ) ) ) |
136 |
135
|
simpld |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( abs ` ( F ` k ) ) - ( ( ( abs ` ( F ` k ) ) ^ 3 ) / 3 ) ) < ( sin ` ( abs ` ( F ` k ) ) ) ) |
137 |
124 136
|
eqbrtrd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( 1 - ( ( ( F ` k ) ^ 2 ) / 3 ) ) x. ( abs ` ( F ` k ) ) ) < ( sin ` ( abs ` ( F ` k ) ) ) ) |
138 |
103
|
resincld |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( sin ` ( abs ` ( F ` k ) ) ) e. RR ) |
139 |
85 138 125
|
ltmuldivd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( ( 1 - ( ( ( F ` k ) ^ 2 ) / 3 ) ) x. ( abs ` ( F ` k ) ) ) < ( sin ` ( abs ` ( F ` k ) ) ) <-> ( 1 - ( ( ( F ` k ) ^ 2 ) / 3 ) ) < ( ( sin ` ( abs ` ( F ` k ) ) ) / ( abs ` ( F ` k ) ) ) ) ) |
140 |
137 139
|
mpbid |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( 1 - ( ( ( F ` k ) ^ 2 ) / 3 ) ) < ( ( sin ` ( abs ` ( F ` k ) ) ) / ( abs ` ( F ` k ) ) ) ) |
141 |
|
fveq2 |
|- ( ( abs ` ( F ` k ) ) = ( F ` k ) -> ( sin ` ( abs ` ( F ` k ) ) ) = ( sin ` ( F ` k ) ) ) |
142 |
|
id |
|- ( ( abs ` ( F ` k ) ) = ( F ` k ) -> ( abs ` ( F ` k ) ) = ( F ` k ) ) |
143 |
141 142
|
oveq12d |
|- ( ( abs ` ( F ` k ) ) = ( F ` k ) -> ( ( sin ` ( abs ` ( F ` k ) ) ) / ( abs ` ( F ` k ) ) ) = ( ( sin ` ( F ` k ) ) / ( F ` k ) ) ) |
144 |
143
|
a1i |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( abs ` ( F ` k ) ) = ( F ` k ) -> ( ( sin ` ( abs ` ( F ` k ) ) ) / ( abs ` ( F ` k ) ) ) = ( ( sin ` ( F ` k ) ) / ( F ` k ) ) ) ) |
145 |
|
sinneg |
|- ( ( F ` k ) e. CC -> ( sin ` -u ( F ` k ) ) = -u ( sin ` ( F ` k ) ) ) |
146 |
22 145
|
syl |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( sin ` -u ( F ` k ) ) = -u ( sin ` ( F ` k ) ) ) |
147 |
146
|
oveq1d |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( sin ` -u ( F ` k ) ) / -u ( F ` k ) ) = ( -u ( sin ` ( F ` k ) ) / -u ( F ` k ) ) ) |
148 |
97
|
recnd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( sin ` ( F ` k ) ) e. CC ) |
149 |
148 22 98
|
div2negd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( -u ( sin ` ( F ` k ) ) / -u ( F ` k ) ) = ( ( sin ` ( F ` k ) ) / ( F ` k ) ) ) |
150 |
147 149
|
eqtrd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( sin ` -u ( F ` k ) ) / -u ( F ` k ) ) = ( ( sin ` ( F ` k ) ) / ( F ` k ) ) ) |
151 |
|
fveq2 |
|- ( ( abs ` ( F ` k ) ) = -u ( F ` k ) -> ( sin ` ( abs ` ( F ` k ) ) ) = ( sin ` -u ( F ` k ) ) ) |
152 |
|
id |
|- ( ( abs ` ( F ` k ) ) = -u ( F ` k ) -> ( abs ` ( F ` k ) ) = -u ( F ` k ) ) |
153 |
151 152
|
oveq12d |
|- ( ( abs ` ( F ` k ) ) = -u ( F ` k ) -> ( ( sin ` ( abs ` ( F ` k ) ) ) / ( abs ` ( F ` k ) ) ) = ( ( sin ` -u ( F ` k ) ) / -u ( F ` k ) ) ) |
154 |
153
|
eqeq1d |
|- ( ( abs ` ( F ` k ) ) = -u ( F ` k ) -> ( ( ( sin ` ( abs ` ( F ` k ) ) ) / ( abs ` ( F ` k ) ) ) = ( ( sin ` ( F ` k ) ) / ( F ` k ) ) <-> ( ( sin ` -u ( F ` k ) ) / -u ( F ` k ) ) = ( ( sin ` ( F ` k ) ) / ( F ` k ) ) ) ) |
155 |
150 154
|
syl5ibrcom |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( abs ` ( F ` k ) ) = -u ( F ` k ) -> ( ( sin ` ( abs ` ( F ` k ) ) ) / ( abs ` ( F ` k ) ) ) = ( ( sin ` ( F ` k ) ) / ( F ` k ) ) ) ) |
156 |
21
|
absord |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( abs ` ( F ` k ) ) = ( F ` k ) \/ ( abs ` ( F ` k ) ) = -u ( F ` k ) ) ) |
157 |
144 155 156
|
mpjaod |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( sin ` ( abs ` ( F ` k ) ) ) / ( abs ` ( F ` k ) ) ) = ( ( sin ` ( F ` k ) ) / ( F ` k ) ) ) |
158 |
140 157
|
breqtrd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( 1 - ( ( ( F ` k ) ^ 2 ) / 3 ) ) < ( ( sin ` ( F ` k ) ) / ( F ` k ) ) ) |
159 |
85 99 158
|
ltled |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( 1 - ( ( ( F ` k ) ^ 2 ) / 3 ) ) <_ ( ( sin ` ( F ` k ) ) / ( F ` k ) ) ) |
160 |
159 78 96
|
3brtr4d |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( H o. F ) ` k ) <_ ( ( G o. F ) ` k ) ) |
161 |
79
|
a1i |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> 1 e. RR ) |
162 |
135
|
simprd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( sin ` ( abs ` ( F ` k ) ) ) < ( abs ` ( F ` k ) ) ) |
163 |
104
|
mulid1d |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( abs ` ( F ` k ) ) x. 1 ) = ( abs ` ( F ` k ) ) ) |
164 |
162 163
|
breqtrrd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( sin ` ( abs ` ( F ` k ) ) ) < ( ( abs ` ( F ` k ) ) x. 1 ) ) |
165 |
138 161 125
|
ltdivmuld |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( ( sin ` ( abs ` ( F ` k ) ) ) / ( abs ` ( F ` k ) ) ) < 1 <-> ( sin ` ( abs ` ( F ` k ) ) ) < ( ( abs ` ( F ` k ) ) x. 1 ) ) ) |
166 |
164 165
|
mpbird |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( sin ` ( abs ` ( F ` k ) ) ) / ( abs ` ( F ` k ) ) ) < 1 ) |
167 |
157 166
|
eqbrtrrd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( sin ` ( F ` k ) ) / ( F ` k ) ) < 1 ) |
168 |
99 161 167
|
ltled |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( sin ` ( F ` k ) ) / ( F ` k ) ) <_ 1 ) |
169 |
96 168
|
eqbrtrd |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( G o. F ) ` k ) <_ 1 ) |
170 |
7 8 68 71 86 100 160 169
|
climsqz |
|- ( ph -> ( G o. F ) ~~> 1 ) |