resincncf

Description: sin restricted to reals is continuous from reals to reals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	resincncf	$⊢ ({\sin ↾}_{ℝ}) : ℝ \underset{cn}{⟶} ℝ$

Step	Hyp	Ref	Expression
1		sinf	$⊢ \sin : ℂ ⟶ ℂ$
2		ffn	$⊢ \sin : ℂ ⟶ ℂ \to \sin Fn ℂ$
3	1 2	ax-mp	$⊢ \sin Fn ℂ$
4		ax-resscn	$⊢ ℝ \subseteq ℂ$
5		fnssres	$⊢ (\sin Fn ℂ \land ℝ \subseteq ℂ) \to ({\sin ↾}_{ℝ}) Fn ℝ$
6	3 4 5	mp2an	$⊢ ({\sin ↾}_{ℝ}) Fn ℝ$
7		fvres	$⊢ x \in ℝ \to ({\sin ↾}_{ℝ}) (x) = \sin x$
8		resincl	$⊢ x \in ℝ \to \sin x \in ℝ$
9	7 8	eqeltrd	$⊢ x \in ℝ \to ({\sin ↾}_{ℝ}) (x) \in ℝ$
10	9	rgen	$⊢ \forall x \in ℝ ({\sin ↾}_{ℝ}) (x) \in ℝ$
11		ffnfv	$⊢ ({\sin ↾}_{ℝ}) : ℝ ⟶ ℝ \leftrightarrow (({\sin ↾}_{ℝ}) Fn ℝ \land \forall x \in ℝ ({\sin ↾}_{ℝ}) (x) \in ℝ)$
12	6 10 11	mpbir2an	$⊢ ({\sin ↾}_{ℝ}) : ℝ ⟶ ℝ$
13		sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$
14		rescncf	$⊢ ℝ \subseteq ℂ \to (\sin : ℂ \underset{cn}{⟶} ℂ \to ({\sin ↾}_{ℝ}) : ℝ \underset{cn}{⟶} ℂ)$
15	4 13 14	mp2	$⊢ ({\sin ↾}_{ℝ}) : ℝ \underset{cn}{⟶} ℂ$
16		cncfcdm	$⊢ (ℝ \subseteq ℂ \land ({\sin ↾}_{ℝ}) : ℝ \underset{cn}{⟶} ℂ) \to (({\sin ↾}_{ℝ}) : ℝ \underset{cn}{⟶} ℝ \leftrightarrow ({\sin ↾}_{ℝ}) : ℝ ⟶ ℝ)$
17	4 15 16	mp2an	$⊢ ({\sin ↾}_{ℝ}) : ℝ \underset{cn}{⟶} ℝ \leftrightarrow ({\sin ↾}_{ℝ}) : ℝ ⟶ ℝ$
18	12 17	mpbir	$⊢ ({\sin ↾}_{ℝ}) : ℝ \underset{cn}{⟶} ℝ$

Metamath Proof Explorer