This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resincncf

Description: sin restricted to reals is continuous from reals to reals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion resincncf 
|- ( sin |` RR ) e. ( RR -cn-> RR )

Proof

Step Hyp Ref Expression
1 sinf 
 |-  sin : CC --> CC
2 ffn 
 |-  ( sin : CC --> CC -> sin Fn CC )
3 1 2 ax-mp 
 |-  sin Fn CC
4 ax-resscn 
 |-  RR C_ CC
5 fnssres 
 |-  ( ( sin Fn CC /\ RR C_ CC ) -> ( sin |` RR ) Fn RR )
6 3 4 5 mp2an 
 |-  ( sin |` RR ) Fn RR
7 fvres 
 |-  ( x e. RR -> ( ( sin |` RR ) ` x ) = ( sin ` x ) )
8 resincl 
 |-  ( x e. RR -> ( sin ` x ) e. RR )
9 7 8 eqeltrd 
 |-  ( x e. RR -> ( ( sin |` RR ) ` x ) e. RR )
10 9 rgen 
 |-  A. x e. RR ( ( sin |` RR ) ` x ) e. RR
11 ffnfv 
 |-  ( ( sin |` RR ) : RR --> RR <-> ( ( sin |` RR ) Fn RR /\ A. x e. RR ( ( sin |` RR ) ` x ) e. RR ) )
12 6 10 11 mpbir2an 
 |-  ( sin |` RR ) : RR --> RR
13 sincn 
 |-  sin e. ( CC -cn-> CC )
14 rescncf 
 |-  ( RR C_ CC -> ( sin e. ( CC -cn-> CC ) -> ( sin |` RR ) e. ( RR -cn-> CC ) ) )
15 4 13 14 mp2 
 |-  ( sin |` RR ) e. ( RR -cn-> CC )
16 cncfcdm 
 |-  ( ( RR C_ CC /\ ( sin |` RR ) e. ( RR -cn-> CC ) ) -> ( ( sin |` RR ) e. ( RR -cn-> RR ) <-> ( sin |` RR ) : RR --> RR ) )
17 4 15 16 mp2an 
 |-  ( ( sin |` RR ) e. ( RR -cn-> RR ) <-> ( sin |` RR ) : RR --> RR )
18 12 17 mpbir 
 |-  ( sin |` RR ) e. ( RR -cn-> RR )