Metamath Proof Explorer

Theorem coscn

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

Ref Expression
Assertion coscn 
|- cos e. ( CC -cn-> CC )

Proof

Step Hyp Ref Expression
1 df-cos 
 |-  cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
2 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
3 2 addcn 
 |-  + 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 ) ) = ( y e. CC |-> ( y / 2 ) ) )
25 oveq1 
 |-  ( y = ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) -> ( y / 2 ) = ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
26 22 23 24 25 fmptcof 
 |-  ( T. -> ( ( y e. CC |-> ( y / 2 ) ) 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 ) ) )
27 2cn 
 |-  2 e. CC
28 2ne0 
 |-  2 =/= 0
29 eqid 
 |-  ( y e. CC |-> ( y / 2 ) ) = ( y e. CC |-> ( y / 2 ) )
30 29 divccncf 
 |-  ( ( 2 e. CC /\ 2 =/= 0 ) -> ( y e. CC |-> ( y / 2 ) ) e. ( CC -cn-> CC ) )
31 27 28 30 mp2an 
 |-  ( y e. CC |-> ( y / 2 ) ) e. ( CC -cn-> CC )
32 31 a1i 
 |-  ( T. -> ( y e. CC |-> ( y / 2 ) ) e. ( CC -cn-> CC ) )
33 17 32 cncfco 
 |-  ( T. -> ( ( y e. CC |-> ( y / 2 ) ) 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 ) ) e. ( CC -cn-> CC ) )
35 34 mptru 
 |-  ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) ) e. ( CC -cn-> CC )
36 1 35 eqeltri 
 |-  cos e. ( CC -cn-> CC )