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 )