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