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 ⊢ x ∈ ℝ → sin ↾ ℝ ⁡ x = sin ⁡ x
8 resincl ⊢ x ∈ ℝ → sin ⁡ x ∈ ℝ
9 7 8 eqeltrd ⊢ x ∈ ℝ → sin ↾ ℝ ⁡ x ∈ ℝ
10 9 rgen ⊢ ∀ x ∈ ℝ sin ↾ ℝ ⁡ x ∈ ℝ
11 ffnfv ⊢ sin ↾ ℝ : ℝ ⟶ ℝ ↔ sin ↾ ℝ Fn ℝ ∧ ∀ x ∈ ℝ sin ↾ ℝ ⁡ x ∈ ℝ
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 ℝ