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 ↾ ℝ ) ∈ ( ℝ –cn→ ℝ )

Proof

Step	Hyp	Ref	Expression
1		sinf	⊢ sin : ℂ ⟶ ℂ
2		ffn	⊢ ( sin : ℂ ⟶ ℂ → sin Fn ℂ )
3	1 2	ax-mp	⊢ sin Fn ℂ
4		ax-resscn	⊢ ℝ ⊆ ℂ
5		fnssres	⊢ ( ( sin Fn ℂ ∧ ℝ ⊆ ℂ ) → ( sin ↾ ℝ ) Fn ℝ )
6	3 4 5	mp2an	⊢ ( sin ↾ ℝ ) Fn ℝ
7		fvres	⊢ ( 𝑥 ∈ ℝ → ( ( sin ↾ ℝ ) ‘ 𝑥 ) = ( sin ‘ 𝑥 ) )
8		resincl	⊢ ( 𝑥 ∈ ℝ → ( sin ‘ 𝑥 ) ∈ ℝ )
9	7 8	eqeltrd	⊢ ( 𝑥 ∈ ℝ → ( ( sin ↾ ℝ ) ‘ 𝑥 ) ∈ ℝ )
10	9	rgen	⊢ ∀ 𝑥 ∈ ℝ ( ( sin ↾ ℝ ) ‘ 𝑥 ) ∈ ℝ
11		ffnfv	⊢ ( ( sin ↾ ℝ ) : ℝ ⟶ ℝ ↔ ( ( sin ↾ ℝ ) Fn ℝ ∧ ∀ 𝑥 ∈ ℝ ( ( sin ↾ ℝ ) ‘ 𝑥 ) ∈ ℝ ) )
12	6 10 11	mpbir2an	⊢ ( sin ↾ ℝ ) : ℝ ⟶ ℝ
13		sincn	⊢ sin ∈ ( ℂ –cn→ ℂ )
14		rescncf	⊢ ( ℝ ⊆ ℂ → ( sin ∈ ( ℂ –cn→ ℂ ) → ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℂ ) ) )
15	4 13 14	mp2	⊢ ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℂ )
16		cncffvrn	⊢ ( ( ℝ ⊆ ℂ ∧ ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℂ ) ) → ( ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℝ ) ↔ ( sin ↾ ℝ ) : ℝ ⟶ ℝ ) )
17	4 15 16	mp2an	⊢ ( ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℝ ) ↔ ( sin ↾ ℝ ) : ℝ ⟶ ℝ )
18	12 17	mpbir	⊢ ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℝ )