Step |
Hyp |
Ref |
Expression |
1 |
|
0p1e1 |
⊢ ( 0 + 1 ) = 1 |
2 |
1
|
fveq2i |
⊢ ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 0 + 1 ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 1 ) |
3 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
4 |
|
dvnp1 |
⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 0 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 0 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ) ) |
5 |
3 4
|
mp3an3 |
⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 0 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ) ) |
6 |
|
dvn0 |
⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) = 𝐹 ) |
7 |
6
|
oveq2d |
⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ) = ( 𝑆 D 𝐹 ) ) |
8 |
5 7
|
eqtrd |
⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 0 + 1 ) ) = ( 𝑆 D 𝐹 ) ) |
9 |
2 8
|
syl5eqr |
⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 1 ) = ( 𝑆 D 𝐹 ) ) |