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 φ F : 0
sinccvg.2 φ F 0
sinccvg.3 G = x 0 sin x x
sinccvg.4 H = x 1 x 2 3
sinccvg.5 φ M
sinccvg.6 φ k M F k < 1
Assertion sinccvglem φ G F 1

Proof

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