Metamath Proof Explorer

Theorem sinccvglem

Description: ( ( sinx ) / x ) ~> 1 as (real) x ~> 0 . (Contributed by Paul Chapman, 10-Nov-2012) (Revised by Mario Carneiro, 21-May-2014)

Ref Expression
Hypotheses sinccvg.1 
|- ( ph -> F : NN --> ( RR \ { 0 } ) )
sinccvg.2 
|- ( ph -> F ~~> 0 )
sinccvg.3 
|- G = ( x e. ( RR \ { 0 } ) |-> ( ( sin ` x ) / x ) )
sinccvg.4 
|- H = ( x e. CC |-> ( 1 - ( ( x ^ 2 ) / 3 ) ) )
sinccvg.5 
|- ( ph -> M e. NN )
sinccvg.6 
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( abs ` ( F ` k ) ) < 1 )
Assertion sinccvglem 
|- ( ph -> ( G o. F ) ~~> 1 )

Proof

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 eqtrid 
 |-  ( ( 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 )