# Metamath Proof Explorer

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 𝑆 ) ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( ( 𝑆 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 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑛 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 𝑛 ) ) ) ↔ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 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 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑛 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 𝑛 ) ) ) ↔ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 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 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑛 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 𝑛 ) ) ) ↔ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 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 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑛 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 𝑛 ) ) ) ↔ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑁 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 𝑁 ) ) ) ) )
21 recnprss ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
22 21 ad2antrr ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → 𝑆 ⊆ ℂ )
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 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ℂ ↑pm dom 𝐹 ) ⊆ ( ℂ ↑pm 𝑆 ) )
33 dvnff ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( 𝑆 D𝑛 𝐹 ) : ℕ0 ⟶ ( ℂ ↑pm dom 𝐹 ) )
34 33 ffvelrnda ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ∈ ( ℂ ↑pm dom 𝐹 ) )
35 32 34 sseldd ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ∈ ( ℂ ↑pm 𝑆 ) )
36 dvn0 ( ( 𝑆 ⊆ ℂ ∧ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 0 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) )
37 22 35 36 syl2anc ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 0 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) )
38 nn0cn ( 𝑀 ∈ ℕ0𝑀 ∈ ℂ )
39 38 adantl ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℂ )
40 39 addid1d ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 + 0 ) = 𝑀 )
41 40 fveq2d ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 0 ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) )
42 37 41 eqtr4d ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 0 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 0 ) ) )
43 oveq2 ( ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) → ( 𝑆 D ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) ) )
44 22 adantr ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑆 ⊆ ℂ )
45 35 adantr ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ∈ ( ℂ ↑pm 𝑆 ) )
46 simpr ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
47 dvnp1 ( ( 𝑆 ⊆ ℂ ∧ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑘 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) ) )
48 44 45 46 47 syl3anc ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑘 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) ) )
49 39 adantr ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ ℂ )
50 nn0cn ( 𝑘 ∈ ℕ0𝑘 ∈ ℂ )
51 50 adantl ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℂ )
52 1cnd ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 1 ∈ ℂ )
53 49 51 52 addassd ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑀 + 𝑘 ) + 1 ) = ( 𝑀 + ( 𝑘 + 1 ) ) )
54 53 fveq2d ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( ( 𝑀 + 𝑘 ) + 1 ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑘 + 1 ) ) ) )
55 simpllr ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
56 nn0addcl ( ( 𝑀 ∈ ℕ0𝑘 ∈ ℕ0 ) → ( 𝑀 + 𝑘 ) ∈ ℕ0 )
57 56 adantll ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 + 𝑘 ) ∈ ℕ0 )
58 dvnp1 ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ ( 𝑀 + 𝑘 ) ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( ( 𝑀 + 𝑘 ) + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) ) )
59 44 55 57 58 syl3anc ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( ( 𝑀 + 𝑘 ) + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) ) )
60 54 59 eqtr3d ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑘 + 1 ) ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) ) )
61 48 60 eqeq12d ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑘 + 1 ) ) ) ↔ ( 𝑆 D ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) ) ) )
62 43 61 syl5ibr ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑘 + 1 ) ) ) ) )
63 62 expcom ( 𝑘 ∈ ℕ0 → ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑘 + 1 ) ) ) ) ) )
64 63 a2d ( 𝑘 ∈ ℕ0 → ( ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 𝑘 ) ) ) → ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + ( 𝑘 + 1 ) ) ) ) ) )
65 5 10 15 20 42 64 nn0ind ( 𝑁 ∈ ℕ0 → ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑁 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 𝑁 ) ) ) )
66 65 com12 ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 ∈ ℕ0 → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑁 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 𝑁 ) ) ) )
67 66 impr ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) ‘ 𝑁 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑀 + 𝑁 ) ) )