dvnfre

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

		Ref	Expression
	Assertion	dvnfre	⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑁 ∈ ℕ₀ ) → ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑁 ) : dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑁 ) ⟶ ℝ )

Proof

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

Metamath Proof Explorer

Theorem dvnfre

Proof