dvfre

Description: The derivative of a real function is real. (Contributed by Mario Carneiro, 1-Sep-2014)

		Ref	Expression
	Assertion	dvfre	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$

Proof

Step	Hyp	Ref	Expression
1		dvf	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ$
2		ffn	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ \to F_{ℝ}^{'} Fn dom F_{ℝ}^{'}$
3	1 2	mp1i	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to F_{ℝ}^{'} Fn dom F_{ℝ}^{'}$
4	1	ffvelcdmi	$⊢ x \in dom F_{ℝ}^{'} \to F_{ℝ}^{'} (x) \in ℂ$
5	4	adantl	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land x \in dom F_{ℝ}^{'}) \to F_{ℝ}^{'} (x) \in ℂ$
6		simpr	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land x \in dom F_{ℝ}^{'}) \to x \in dom F_{ℝ}^{'}$
7		fvco3	$⊢ (F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ \land x \in dom F_{ℝ}^{'}) \to (* \circ F_{ℝ}^{'}) (x) = \overline{F_{ℝ}^{'} (x)}$
8	1 6 7	sylancr	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land x \in dom F_{ℝ}^{'}) \to (* \circ F_{ℝ}^{'}) (x) = \overline{F_{ℝ}^{'} (x)}$
9		ax-resscn	$⊢ ℝ \subseteq ℂ$
10		fss	$⊢ (F : A ⟶ ℝ \land ℝ \subseteq ℂ) \to F : A ⟶ ℂ$
11	9 10	mpan2	$⊢ F : A ⟶ ℝ \to F : A ⟶ ℂ$
12		dvcj	$⊢ (F : A ⟶ ℂ \land A \subseteq ℝ) \to ℝ D (* \circ F) = * \circ F_{ℝ}^{'}$
13	11 12	sylan	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to ℝ D (* \circ F) = * \circ F_{ℝ}^{'}$
14		ffvelcdm	$⊢ (F : A ⟶ ℝ \land y \in A) \to F (y) \in ℝ$
15	14	adantlr	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land y \in A) \to F (y) \in ℝ$
16	15	cjred	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land y \in A) \to \overline{F (y)} = F (y)$
17	16	mpteq2dva	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to (y \in A ⟼ \overline{F (y)}) = (y \in A ⟼ F (y))$
18	15	recnd	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land y \in A) \to F (y) \in ℂ$
19		simpl	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to F : A ⟶ ℝ$
20	19	feqmptd	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to F = (y \in A ⟼ F (y))$
21		cjf	$⊢ * : ℂ ⟶ ℂ$
22	21	a1i	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to * : ℂ ⟶ ℂ$
23	22	feqmptd	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to * = (z \in ℂ ⟼ \overline{z})$
24		fveq2	$⊢ z = F (y) \to \overline{z} = \overline{F (y)}$
25	18 20 23 24	fmptco	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to * \circ F = (y \in A ⟼ \overline{F (y)})$
26	17 25 20	3eqtr4d	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to * \circ F = F$
27	26	oveq2d	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to ℝ D (* \circ F) = ℝ D F$
28	13 27	eqtr3d	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to * \circ F_{ℝ}^{'} = ℝ D F$
29	28	fveq1d	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to (* \circ F_{ℝ}^{'}) (x) = F_{ℝ}^{'} (x)$
30	29	adantr	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land x \in dom F_{ℝ}^{'}) \to (* \circ F_{ℝ}^{'}) (x) = F_{ℝ}^{'} (x)$
31	8 30	eqtr3d	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land x \in dom F_{ℝ}^{'}) \to \overline{F_{ℝ}^{'} (x)} = F_{ℝ}^{'} (x)$
32	5 31	cjrebd	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land x \in dom F_{ℝ}^{'}) \to F_{ℝ}^{'} (x) \in ℝ$
33	32	ralrimiva	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to \forall x \in dom F_{ℝ}^{'} F_{ℝ}^{'} (x) \in ℝ$
34		ffnfv	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ \leftrightarrow (F_{ℝ}^{'} Fn dom F_{ℝ}^{'} \land \forall x \in dom F_{ℝ}^{'} F_{ℝ}^{'} (x) \in ℝ)$
35	3 33 34	sylanbrc	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$

Metamath Proof Explorer

Theorem dvfre

Proof