Metamath Proof Explorer

Theorem 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 ⟶ ℝ ∧ A ⊆ ℝ ∧ N ∈ ℕ 0 → ℝ D n F ⁡ N : dom ⁡ ℝ D n F ⁡ N ⟶ ℝ

Proof

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