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 : NN --> ( RR \ { 0 } ) /\ F ~~> 0 ) -> ( ( x e. ( RR \ { 0 } ) |-> ( ( sin ` x ) / x ) ) o. F ) ~~> 1 )

Proof

Step Hyp Ref Expression
1 nnuz 
 |-  NN = ( ZZ>= ` 1 )
2 1zzd 
 |-  ( ( F : NN --> ( RR \ { 0 } ) /\ F ~~> 0 ) -> 1 e. ZZ )
3 1rp 
 |-  1 e. RR+
4 3 a1i 
 |-  ( ( F : NN --> ( RR \ { 0 } ) /\ F ~~> 0 ) -> 1 e. RR+ )
5 eqidd 
 |-  ( ( ( F : NN --> ( RR \ { 0 } ) /\ F ~~> 0 ) /\ k e. NN ) -> ( F ` k ) = ( F ` k ) )
6 simpr 
 |-  ( ( F : NN --> ( RR \ { 0 } ) /\ F ~~> 0 ) -> F ~~> 0 )
7 1 2 4 5 6 climi0 
 |-  ( ( F : NN --> ( RR \ { 0 } ) /\ F ~~> 0 ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < 1 )
8 simpll 
 |-  ( ( ( F : NN --> ( RR \ { 0 } ) /\ F ~~> 0 ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < 1 ) ) -> F : NN --> ( RR \ { 0 } ) )
9 simplr 
 |-  ( ( ( F : NN --> ( RR \ { 0 } ) /\ F ~~> 0 ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < 1 ) ) -> F ~~> 0 )
10 eqid 
 |-  ( x e. ( RR \ { 0 } ) |-> ( ( sin ` x ) / x ) ) = ( x e. ( RR \ { 0 } ) |-> ( ( sin ` x ) / x ) )
11 eqid 
 |-  ( x e. CC |-> ( 1 - ( ( x ^ 2 ) / 3 ) ) ) = ( x e. CC |-> ( 1 - ( ( x ^ 2 ) / 3 ) ) )
12 simprl 
 |-  ( ( ( F : NN --> ( RR \ { 0 } ) /\ F ~~> 0 ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < 1 ) ) -> j e. NN )
13 simprr 
 |-  ( ( ( F : NN --> ( RR \ { 0 } ) /\ F ~~> 0 ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < 1 ) ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < 1 )
14 2fveq3 
 |-  ( k = n -> ( abs ` ( F ` k ) ) = ( abs ` ( F ` n ) ) )
15 14 breq1d 
 |-  ( k = n -> ( ( abs ` ( F ` k ) ) < 1 <-> ( abs ` ( F ` n ) ) < 1 ) )
16 15 rspccva 
 |-  ( ( A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < 1 /\ n e. ( ZZ>= ` j ) ) -> ( abs ` ( F ` n ) ) < 1 )
17 13 16 sylan 
 |-  ( ( ( ( F : NN --> ( RR \ { 0 } ) /\ F ~~> 0 ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < 1 ) ) /\ n e. ( ZZ>= ` j ) ) -> ( abs ` ( F ` n ) ) < 1 )
18 8 9 10 11 12 17 sinccvglem 
 |-  ( ( ( F : NN --> ( RR \ { 0 } ) /\ F ~~> 0 ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < 1 ) ) -> ( ( x e. ( RR \ { 0 } ) |-> ( ( sin ` x ) / x ) ) o. F ) ~~> 1 )
19 7 18 rexlimddv 
 |-  ( ( F : NN --> ( RR \ { 0 } ) /\ F ~~> 0 ) -> ( ( x e. ( RR \ { 0 } ) |-> ( ( sin ` x ) / x ) ) o. F ) ~~> 1 )