Metamath Proof Explorer

Theorem sincn

Description: Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007) (Revised by Mario Carneiro, 3-Sep-2014)

Ref Expression
Assertion sincn 
|- sin e. ( CC -cn-> CC )

Proof

Step Hyp Ref Expression
1 df-sin 
 |-  sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
2 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
3 2 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
4 3 a1i 
 |-  ( T. -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
5 efcn 
 |-  exp e. ( CC -cn-> CC )
6 5 a1i 
 |-  ( T. -> exp e. ( CC -cn-> CC ) )
7 ax-icn 
 |-  _i e. CC
8 eqid 
 |-  ( x e. CC |-> ( _i x. x ) ) = ( x e. CC |-> ( _i x. x ) )
9 8 mulc1cncf 
 |-  ( _i e. CC -> ( x e. CC |-> ( _i x. x ) ) e. ( CC -cn-> CC ) )
10 7 9 mp1i 
 |-  ( T. -> ( x e. CC |-> ( _i x. x ) ) e. ( CC -cn-> CC ) )
11 6 10 cncfmpt1f 
 |-  ( T. -> ( x e. CC |-> ( exp ` ( _i x. x ) ) ) e. ( CC -cn-> CC ) )
12 negicn 
 |-  -u _i e. CC
13 eqid 
 |-  ( x e. CC |-> ( -u _i x. x ) ) = ( x e. CC |-> ( -u _i x. x ) )
14 13 mulc1cncf 
 |-  ( -u _i e. CC -> ( x e. CC |-> ( -u _i x. x ) ) e. ( CC -cn-> CC ) )
15 12 14 mp1i 
 |-  ( T. -> ( x e. CC |-> ( -u _i x. x ) ) e. ( CC -cn-> CC ) )
16 6 15 cncfmpt1f 
 |-  ( T. -> ( x e. CC |-> ( exp ` ( -u _i x. x ) ) ) e. ( CC -cn-> CC ) )
17 2 4 11 16 cncfmpt2f 
 |-  ( T. -> ( x e. CC |-> ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) ) e. ( CC -cn-> CC ) )
18 cncff 
 |-  ( ( x e. CC |-> ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) ) e. ( CC -cn-> CC ) -> ( x e. CC |-> ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) ) : CC --> CC )
19 17 18 syl 
 |-  ( T. -> ( x e. CC |-> ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) ) : CC --> CC )
20 eqid 
 |-  ( x e. CC |-> ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) ) = ( x e. CC |-> ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) )
21 20 fmpt 
 |-  ( A. x e. CC ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) e. CC <-> ( x e. CC |-> ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) ) : CC --> CC )
22 19 21 sylibr 
 |-  ( T. -> A. x e. CC ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) e. CC )
23 eqidd 
 |-  ( T. -> ( x e. CC |-> ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) ) = ( x e. CC |-> ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) ) )
24 eqidd 
 |-  ( T. -> ( y e. CC |-> ( y / ( 2 x. _i ) ) ) = ( y e. CC |-> ( y / ( 2 x. _i ) ) ) )
25 oveq1 
 |-  ( y = ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) -> ( y / ( 2 x. _i ) ) = ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
26 22 23 24 25 fmptcof 
 |-  ( T. -> ( ( y e. CC |-> ( y / ( 2 x. _i ) ) ) o. ( x e. CC |-> ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) ) ) = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) ) )
27 2mulicn 
 |-  ( 2 x. _i ) e. CC
28 2muline0 
 |-  ( 2 x. _i ) =/= 0
29 eqid 
 |-  ( y e. CC |-> ( y / ( 2 x. _i ) ) ) = ( y e. CC |-> ( y / ( 2 x. _i ) ) )
30 29 divccncf 
 |-  ( ( ( 2 x. _i ) e. CC /\ ( 2 x. _i ) =/= 0 ) -> ( y e. CC |-> ( y / ( 2 x. _i ) ) ) e. ( CC -cn-> CC ) )
31 27 28 30 mp2an 
 |-  ( y e. CC |-> ( y / ( 2 x. _i ) ) ) e. ( CC -cn-> CC )
32 31 a1i 
 |-  ( T. -> ( y e. CC |-> ( y / ( 2 x. _i ) ) ) e. ( CC -cn-> CC ) )
33 17 32 cncfco 
 |-  ( T. -> ( ( y e. CC |-> ( y / ( 2 x. _i ) ) ) o. ( x e. CC |-> ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) ) ) e. ( CC -cn-> CC ) )
34 26 33 eqeltrrd 
 |-  ( T. -> ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) ) e. ( CC -cn-> CC ) )
35 34 mptru 
 |-  ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) ) e. ( CC -cn-> CC )
36 1 35 eqeltri 
 |-  sin e. ( CC -cn-> CC )