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 ↾ ℝ ) ∈ ( ℝ –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 cncfcdm ⊢ ( ( ℝ ⊆ ℂ ∧ ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℂ ) ) → ( ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℝ ) ↔ ( sin ↾ ℝ ) : ℝ ⟶ ℝ ) )
17 4 15 16 mp2an ⊢ ( ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℝ ) ↔ ( sin ↾ ℝ ) : ℝ ⟶ ℝ )
18 12 17 mpbir ⊢ ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℝ )