dvn2bss

Description: An N-times differentiable point is an M-times differentiable point, if M <_ N . (Contributed by Mario Carneiro, 30-Dec-2016)

		Ref	Expression
	Assertion	dvn2bss	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 𝑆 ∈ { ℝ , ℂ } )
2		simp2	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) )
3		elfznn0	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ℕ₀ )
4	3	3ad2ant3	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 𝑀 ∈ ℕ₀ )
5		elfzuz3	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) )
6	5	3ad2ant3	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) )
7		uznn0sub	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) → ( 𝑁 − 𝑀 ) ∈ ℕ₀ )
8	6 7	syl	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝑀 ) ∈ ℕ₀ )
9		dvnadd	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ ( 𝑀 ∈ ℕ₀ ∧ ( 𝑁 − 𝑀 ) ∈ ℕ₀ ) ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑁 − 𝑀 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑁 − 𝑀 ) ) ) )
10	1 2 4 8 9	syl22anc	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑁 − 𝑀 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑁 − 𝑀 ) ) ) )
11	4	nn0cnd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 𝑀 ∈ ℂ )
12		elfzuz2	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ( ℤ_≥ ‘ 0 ) )
13	12	3ad2ant3	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ_≥ ‘ 0 ) )
14		nn0uz	⊢ ℕ₀ = ( ℤ_≥ ‘ 0 )
15	13 14	eleqtrrdi	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℕ₀ )
16	15	nn0cnd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℂ )
17	11 16	pncan3d	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( 𝑀 + ( 𝑁 − 𝑀 ) ) = 𝑁 )
18	17	fveq2d	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑁 − 𝑀 ) ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) )
19	10 18	eqtrd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑁 − 𝑀 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) )
20	19	dmeqd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → dom ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑁 − 𝑀 ) ) = dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) )
21		cnex	⊢ ℂ ∈ V
22	21	a1i	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ℂ ∈ V )
23		dvnf	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) : dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ⟶ ℂ )
24	3 23	syl3an3	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) : dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ⟶ ℂ )
25		dvnbss	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ℕ₀ ) → dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ⊆ dom 𝐹 )
26	3 25	syl3an3	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ⊆ dom 𝐹 )
27		elpmi	⊢ ( 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ 𝑆 ) )
28	27	3ad2ant2	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ 𝑆 ) )
29	28	simprd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → dom 𝐹 ⊆ 𝑆 )
30	26 29	sstrd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ⊆ 𝑆 )
31		elpm2r	⊢ ( ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) ∧ ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) : dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ⟶ ℂ ∧ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ⊆ 𝑆 ) ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ∈ ( ℂ ↑_pm 𝑆 ) )
32	22 1 24 30 31	syl22anc	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ∈ ( ℂ ↑_pm 𝑆 ) )
33		dvnbss	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( 𝑁 − 𝑀 ) ∈ ℕ₀ ) → dom ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑁 − 𝑀 ) ) ⊆ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) )
34	1 32 8 33	syl3anc	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → dom ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑁 − 𝑀 ) ) ⊆ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) )
35	20 34	eqsstrrd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) )

Metamath Proof Explorer

Theorem dvn2bss

Proof