dvnadd

Description: The N -th derivative of the M -th derivative of F is the same as the M + N -th derivative of F . (Contributed by Mario Carneiro, 11-Feb-2015)

		Ref	Expression
	Assertion	dvnadd	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ ( 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ) ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑁 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑛 = 0 → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑛 ) = ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 0 ) )
2		oveq2	⊢ ( 𝑛 = 0 → ( 𝑀 + 𝑛 ) = ( 𝑀 + 0 ) )
3	2	fveq2d	⊢ ( 𝑛 = 0 → ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑛 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 0 ) ) )
4	1 3	eqeq12d	⊢ ( 𝑛 = 0 → ( ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑛 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑛 ) ) ↔ ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 0 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 0 ) ) ) )
5	4	imbi2d	⊢ ( 𝑛 = 0 → ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑛 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑛 ) ) ) ↔ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 0 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 0 ) ) ) ) )
6		fveq2	⊢ ( 𝑛 = 𝑘 → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑛 ) = ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) )
7		oveq2	⊢ ( 𝑛 = 𝑘 → ( 𝑀 + 𝑛 ) = ( 𝑀 + 𝑘 ) )
8	7	fveq2d	⊢ ( 𝑛 = 𝑘 → ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑛 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) )
9	6 8	eqeq12d	⊢ ( 𝑛 = 𝑘 → ( ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑛 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑛 ) ) ↔ ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) ) )
10	9	imbi2d	⊢ ( 𝑛 = 𝑘 → ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑛 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑛 ) ) ) ↔ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) ) ) )
11		fveq2	⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑛 ) = ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑘 + 1 ) ) )
12		oveq2	⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑀 + 𝑛 ) = ( 𝑀 + ( 𝑘 + 1 ) ) )
13	12	fveq2d	⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑛 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑘 + 1 ) ) ) )
14	11 13	eqeq12d	⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑛 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑛 ) ) ↔ ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑘 + 1 ) ) ) ) )
15	14	imbi2d	⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑛 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑛 ) ) ) ↔ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑘 + 1 ) ) ) ) ) )
16		fveq2	⊢ ( 𝑛 = 𝑁 → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑛 ) = ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑁 ) )
17		oveq2	⊢ ( 𝑛 = 𝑁 → ( 𝑀 + 𝑛 ) = ( 𝑀 + 𝑁 ) )
18	17	fveq2d	⊢ ( 𝑛 = 𝑁 → ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑛 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑁 ) ) )
19	16 18	eqeq12d	⊢ ( 𝑛 = 𝑁 → ( ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑛 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑛 ) ) ↔ ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑁 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑁 ) ) ) )
20	19	imbi2d	⊢ ( 𝑛 = 𝑁 → ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑛 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑛 ) ) ) ↔ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑁 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑁 ) ) ) ) )
21		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
22	21	ad2antrr	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → 𝑆 ⊆ ℂ )
23		ssidd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) → ℂ ⊆ ℂ )
24		cnex	⊢ ℂ ∈ V
25		elpm2g	⊢ ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) → ( 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ 𝑆 ) ) )
26	24 25	mpan	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ 𝑆 ) ) )
27	26	simplbda	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) → dom 𝐹 ⊆ 𝑆 )
28	24	a1i	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) → ℂ ∈ V )
29		simpl	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) → 𝑆 ∈ { ℝ , ℂ } )
30		pmss12g	⊢ ( ( ( ℂ ⊆ ℂ ∧ dom 𝐹 ⊆ 𝑆 ) ∧ ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) ) → ( ℂ ↑_pm dom 𝐹 ) ⊆ ( ℂ ↑_pm 𝑆 ) )
31	23 27 28 29 30	syl22anc	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) → ( ℂ ↑_pm dom 𝐹 ) ⊆ ( ℂ ↑_pm 𝑆 ) )
32	31	adantr	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ℂ ↑_pm dom 𝐹 ) ⊆ ( ℂ ↑_pm 𝑆 ) )
33		dvnff	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) → ( 𝑆 D^𝑛 𝐹 ) : ℕ₀ ⟶ ( ℂ ↑_pm dom 𝐹 ) )
34	33	ffvelcdmda	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ∈ ( ℂ ↑_pm dom 𝐹 ) )
35	32 34	sseldd	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ∈ ( ℂ ↑_pm 𝑆 ) )
36		dvn0	⊢ ( ( 𝑆 ⊆ ℂ ∧ ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ∈ ( ℂ ↑_pm 𝑆 ) ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 0 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) )
37	22 35 36	syl2anc	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 0 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) )
38		nn0cn	⊢ ( 𝑀 ∈ ℕ₀ → 𝑀 ∈ ℂ )
39	38	adantl	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → 𝑀 ∈ ℂ )
40	39	addridd	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( 𝑀 + 0 ) = 𝑀 )
41	40	fveq2d	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 0 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) )
42	37 41	eqtr4d	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 0 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 0 ) ) )
43		oveq2	⊢ ( ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) → ( 𝑆 D ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) ) = ( 𝑆 D ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) ) )
44	22	adantr	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑆 ⊆ ℂ )
45	35	adantr	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ∈ ( ℂ ↑_pm 𝑆 ) )
46		simpr	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑘 ∈ ℕ₀ )
47		dvnp1	⊢ ( ( 𝑆 ⊆ ℂ ∧ ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑘 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) ) )
48	44 45 46 47	syl3anc	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑘 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) ) )
49	39	adantr	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑀 ∈ ℂ )
50		nn0cn	⊢ ( 𝑘 ∈ ℕ₀ → 𝑘 ∈ ℂ )
51	50	adantl	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑘 ∈ ℂ )
52		1cnd	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → 1 ∈ ℂ )
53	49 51 52	addassd	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝑀 + 𝑘 ) + 1 ) = ( 𝑀 + ( 𝑘 + 1 ) ) )
54	53	fveq2d	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( ( 𝑀 + 𝑘 ) + 1 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑘 + 1 ) ) ) )
55		simpllr	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) )
56		nn0addcl	⊢ ( ( 𝑀 ∈ ℕ₀ ∧ 𝑘 ∈ ℕ₀ ) → ( 𝑀 + 𝑘 ) ∈ ℕ₀ )
57	56	adantll	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝑀 + 𝑘 ) ∈ ℕ₀ )
58		dvnp1	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ ( 𝑀 + 𝑘 ) ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( ( 𝑀 + 𝑘 ) + 1 ) ) = ( 𝑆 D ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) ) )
59	44 55 57 58	syl3anc	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( ( 𝑀 + 𝑘 ) + 1 ) ) = ( 𝑆 D ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) ) )
60	54 59	eqtr3d	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑘 + 1 ) ) ) = ( 𝑆 D ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) ) )
61	48 60	eqeq12d	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑘 + 1 ) ) ) ↔ ( 𝑆 D ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) ) = ( 𝑆 D ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) ) ) )
62	43 61	imbitrrid	⊢ ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑘 + 1 ) ) ) ) )
63	62	expcom	⊢ ( 𝑘 ∈ ℕ₀ → ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑘 + 1 ) ) ) ) ) )
64	63	a2d	⊢ ( 𝑘 ∈ ℕ₀ → ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) ) → ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑘 + 1 ) ) ) ) ) )
65	5 10 15 20 42 64	nn0ind	⊢ ( 𝑁 ∈ ℕ₀ → ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑁 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑁 ) ) ) )
66	65	com12	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ₀ ) → ( 𝑁 ∈ ℕ₀ → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑁 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑁 ) ) ) )
67	66	impr	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ ( 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ) ) → ( ( 𝑆 D^𝑛 ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑁 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ ( 𝑀 + 𝑁 ) ) )

Metamath Proof Explorer

Theorem dvnadd

Proof