dvnfre

Description: The N -th derivative of a real function is real. (Contributed by Mario Carneiro, 1-Jan-2017)

		Ref	Expression
	Assertion	dvnfre	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ \land N \in ℕ_{0}) \to (ℝ D^{n} F) (N) : dom (ℝ D^{n} F) (N) ⟶ ℝ$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ x = 0 \to (ℝ D^{n} F) (x) = (ℝ D^{n} F) (0)$
2	1	dmeqd	$⊢ x = 0 \to dom (ℝ D^{n} F) (x) = dom (ℝ D^{n} F) (0)$
3	1 2	feq12d	$⊢ x = 0 \to ((ℝ D^{n} F) (x) : dom (ℝ D^{n} F) (x) ⟶ ℝ \leftrightarrow (ℝ D^{n} F) (0) : dom (ℝ D^{n} F) (0) ⟶ ℝ)$
4	3	imbi2d	$⊢ x = 0 \to (((F : A ⟶ ℝ \land A \subseteq ℝ) \to (ℝ D^{n} F) (x) : dom (ℝ D^{n} F) (x) ⟶ ℝ) \leftrightarrow ((F : A ⟶ ℝ \land A \subseteq ℝ) \to (ℝ D^{n} F) (0) : dom (ℝ D^{n} F) (0) ⟶ ℝ))$
5		fveq2	$⊢ x = n \to (ℝ D^{n} F) (x) = (ℝ D^{n} F) (n)$
6	5	dmeqd	$⊢ x = n \to dom (ℝ D^{n} F) (x) = dom (ℝ D^{n} F) (n)$
7	5 6	feq12d	$⊢ x = n \to ((ℝ D^{n} F) (x) : dom (ℝ D^{n} F) (x) ⟶ ℝ \leftrightarrow (ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ)$
8	7	imbi2d	$⊢ x = n \to (((F : A ⟶ ℝ \land A \subseteq ℝ) \to (ℝ D^{n} F) (x) : dom (ℝ D^{n} F) (x) ⟶ ℝ) \leftrightarrow ((F : A ⟶ ℝ \land A \subseteq ℝ) \to (ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ))$
9		fveq2	$⊢ x = n + 1 \to (ℝ D^{n} F) (x) = (ℝ D^{n} F) (n + 1)$
10	9	dmeqd	$⊢ x = n + 1 \to dom (ℝ D^{n} F) (x) = dom (ℝ D^{n} F) (n + 1)$
11	9 10	feq12d	$⊢ x = n + 1 \to ((ℝ D^{n} F) (x) : dom (ℝ D^{n} F) (x) ⟶ ℝ \leftrightarrow (ℝ D^{n} F) (n + 1) : dom (ℝ D^{n} F) (n + 1) ⟶ ℝ)$
12	11	imbi2d	$⊢ x = n + 1 \to (((F : A ⟶ ℝ \land A \subseteq ℝ) \to (ℝ D^{n} F) (x) : dom (ℝ D^{n} F) (x) ⟶ ℝ) \leftrightarrow ((F : A ⟶ ℝ \land A \subseteq ℝ) \to (ℝ D^{n} F) (n + 1) : dom (ℝ D^{n} F) (n + 1) ⟶ ℝ))$
13		fveq2	$⊢ x = N \to (ℝ D^{n} F) (x) = (ℝ D^{n} F) (N)$
14	13	dmeqd	$⊢ x = N \to dom (ℝ D^{n} F) (x) = dom (ℝ D^{n} F) (N)$
15	13 14	feq12d	$⊢ x = N \to ((ℝ D^{n} F) (x) : dom (ℝ D^{n} F) (x) ⟶ ℝ \leftrightarrow (ℝ D^{n} F) (N) : dom (ℝ D^{n} F) (N) ⟶ ℝ)$
16	15	imbi2d	$⊢ x = N \to (((F : A ⟶ ℝ \land A \subseteq ℝ) \to (ℝ D^{n} F) (x) : dom (ℝ D^{n} F) (x) ⟶ ℝ) \leftrightarrow ((F : A ⟶ ℝ \land A \subseteq ℝ) \to (ℝ D^{n} F) (N) : dom (ℝ D^{n} F) (N) ⟶ ℝ))$
17		simpl	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to F : A ⟶ ℝ$
18		ax-resscn	$⊢ ℝ \subseteq ℂ$
19		fss	$⊢ (F : A ⟶ ℝ \land ℝ \subseteq ℂ) \to F : A ⟶ ℂ$
20	18 19	mpan2	$⊢ F : A ⟶ ℝ \to F : A ⟶ ℂ$
21		cnex	$⊢ ℂ \in V$
22		reex	$⊢ ℝ \in V$
23		elpm2r	$⊢ ((ℂ \in V \land ℝ \in V) \land (F : A ⟶ ℂ \land A \subseteq ℝ)) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
24	21 22 23	mpanl12	$⊢ (F : A ⟶ ℂ \land A \subseteq ℝ) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
25	20 24	sylan	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
26		dvn0	$⊢ (ℝ \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} ℝ)) \to (ℝ D^{n} F) (0) = F$
27	18 25 26	sylancr	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to (ℝ D^{n} F) (0) = F$
28	27	dmeqd	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to dom (ℝ D^{n} F) (0) = dom F$
29		fdm	$⊢ F : A ⟶ ℝ \to dom F = A$
30	29	adantr	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to dom F = A$
31	28 30	eqtrd	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to dom (ℝ D^{n} F) (0) = A$
32	27 31	feq12d	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to ((ℝ D^{n} F) (0) : dom (ℝ D^{n} F) (0) ⟶ ℝ \leftrightarrow F : A ⟶ ℝ)$
33	17 32	mpbird	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to (ℝ D^{n} F) (0) : dom (ℝ D^{n} F) (0) ⟶ ℝ$
34		simprr	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land (n \in ℕ_{0} \land (ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ)) \to (ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ$
35	22	prid1	$⊢ ℝ \in \{ℝ, ℂ\}$
36		simprl	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land (n \in ℕ_{0} \land (ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ)) \to n \in ℕ_{0}$
37		dvnbss	$⊢ (ℝ \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℝ) \land n \in ℕ_{0}) \to dom (ℝ D^{n} F) (n) \subseteq dom F$
38	35 25 36 37	mp3an2ani	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land (n \in ℕ_{0} \land (ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ)) \to dom (ℝ D^{n} F) (n) \subseteq dom F$
39	30	adantr	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land (n \in ℕ_{0} \land (ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ)) \to dom F = A$
40	38 39	sseqtrd	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land (n \in ℕ_{0} \land (ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ)) \to dom (ℝ D^{n} F) (n) \subseteq A$
41		simplr	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land (n \in ℕ_{0} \land (ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ)) \to A \subseteq ℝ$
42	40 41	sstrd	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land (n \in ℕ_{0} \land (ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ)) \to dom (ℝ D^{n} F) (n) \subseteq ℝ$
43		dvfre	$⊢ ((ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ \land dom (ℝ D^{n} F) (n) \subseteq ℝ) \to {(ℝ D^{n} F) (n)}_{ℝ}^{'} : dom {(ℝ D^{n} F) (n)}_{ℝ}^{'} ⟶ ℝ$
44	34 42 43	syl2anc	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land (n \in ℕ_{0} \land (ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ)) \to {(ℝ D^{n} F) (n)}_{ℝ}^{'} : dom {(ℝ D^{n} F) (n)}_{ℝ}^{'} ⟶ ℝ$
45		dvnp1	$⊢ (ℝ \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} ℝ) \land n \in ℕ_{0}) \to (ℝ D^{n} F) (n + 1) = ℝ D (ℝ D^{n} F) (n)$
46	18 25 36 45	mp3an2ani	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land (n \in ℕ_{0} \land (ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ)) \to (ℝ D^{n} F) (n + 1) = ℝ D (ℝ D^{n} F) (n)$
47	46	dmeqd	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land (n \in ℕ_{0} \land (ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ)) \to dom (ℝ D^{n} F) (n + 1) = dom {(ℝ D^{n} F) (n)}_{ℝ}^{'}$
48	46 47	feq12d	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land (n \in ℕ_{0} \land (ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ)) \to ((ℝ D^{n} F) (n + 1) : dom (ℝ D^{n} F) (n + 1) ⟶ ℝ \leftrightarrow {(ℝ D^{n} F) (n)}_{ℝ}^{'} : dom {(ℝ D^{n} F) (n)}_{ℝ}^{'} ⟶ ℝ)$
49	44 48	mpbird	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land (n \in ℕ_{0} \land (ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ)) \to (ℝ D^{n} F) (n + 1) : dom (ℝ D^{n} F) (n + 1) ⟶ ℝ$
50	49	expr	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land n \in ℕ_{0}) \to ((ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ \to (ℝ D^{n} F) (n + 1) : dom (ℝ D^{n} F) (n + 1) ⟶ ℝ)$
51	50	expcom	$⊢ n \in ℕ_{0} \to ((F : A ⟶ ℝ \land A \subseteq ℝ) \to ((ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ \to (ℝ D^{n} F) (n + 1) : dom (ℝ D^{n} F) (n + 1) ⟶ ℝ))$
52	51	a2d	$⊢ n \in ℕ_{0} \to (((F : A ⟶ ℝ \land A \subseteq ℝ) \to (ℝ D^{n} F) (n) : dom (ℝ D^{n} F) (n) ⟶ ℝ) \to ((F : A ⟶ ℝ \land A \subseteq ℝ) \to (ℝ D^{n} F) (n + 1) : dom (ℝ D^{n} F) (n + 1) ⟶ ℝ))$
53	4 8 12 16 33 52	nn0ind	$⊢ N \in ℕ_{0} \to ((F : A ⟶ ℝ \land A \subseteq ℝ) \to (ℝ D^{n} F) (N) : dom (ℝ D^{n} F) (N) ⟶ ℝ)$
54	53	com12	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ) \to (N \in ℕ_{0} \to (ℝ D^{n} F) (N) : dom (ℝ D^{n} F) (N) ⟶ ℝ)$
55	54	3impia	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ \land N \in ℕ_{0}) \to (ℝ D^{n} F) (N) : dom (ℝ D^{n} F) (N) ⟶ ℝ$

Metamath Proof Explorer

Theorem dvnfre

Proof