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 cncffvrn
 |-  ( ( 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 )