Metamath Proof Explorer


Theorem sinccvg

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

Ref Expression
Assertion sinccvg F : 0 F 0 x 0 sin x x F 1

Proof

Step Hyp Ref Expression
1 nnuz = 1
2 1zzd F : 0 F 0 1
3 1rp 1 +
4 3 a1i F : 0 F 0 1 +
5 eqidd F : 0 F 0 k F k = F k
6 simpr F : 0 F 0 F 0
7 1 2 4 5 6 climi0 F : 0 F 0 j k j F k < 1
8 simpll F : 0 F 0 j k j F k < 1 F : 0
9 simplr F : 0 F 0 j k j F k < 1 F 0
10 eqid x 0 sin x x = x 0 sin x x
11 eqid x 1 x 2 3 = x 1 x 2 3
12 simprl F : 0 F 0 j k j F k < 1 j
13 simprr F : 0 F 0 j k j F k < 1 k j F k < 1
14 2fveq3 k = n F k = F n
15 14 breq1d k = n F k < 1 F n < 1
16 15 rspccva k j F k < 1 n j F n < 1
17 13 16 sylan F : 0 F 0 j k j F k < 1 n j F n < 1
18 8 9 10 11 12 17 sinccvglem F : 0 F 0 j k j F k < 1 x 0 sin x x F 1
19 7 18 rexlimddv F : 0 F 0 x 0 sin x x F 1