Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
⊢ ( 𝑥 = 0 → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) = ( ( ℂ D𝑛 𝐹 ) ‘ 0 ) ) |
2 |
1
|
eleq1d |
⊢ ( 𝑥 = 0 → ( ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) ∈ ( Poly ‘ 𝑆 ) ↔ ( ( ℂ D𝑛 𝐹 ) ‘ 0 ) ∈ ( Poly ‘ 𝑆 ) ) ) |
3 |
2
|
imbi2d |
⊢ ( 𝑥 = 0 → ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) ∈ ( Poly ‘ 𝑆 ) ) ↔ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 0 ) ∈ ( Poly ‘ 𝑆 ) ) ) ) |
4 |
|
fveq2 |
⊢ ( 𝑥 = 𝑛 → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) = ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ) |
5 |
4
|
eleq1d |
⊢ ( 𝑥 = 𝑛 → ( ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) ∈ ( Poly ‘ 𝑆 ) ↔ ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) ) ) |
6 |
5
|
imbi2d |
⊢ ( 𝑥 = 𝑛 → ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) ∈ ( Poly ‘ 𝑆 ) ) ↔ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) ) ) ) |
7 |
|
fveq2 |
⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) = ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) |
8 |
7
|
eleq1d |
⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) ∈ ( Poly ‘ 𝑆 ) ↔ ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ ( Poly ‘ 𝑆 ) ) ) |
9 |
8
|
imbi2d |
⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) ∈ ( Poly ‘ 𝑆 ) ) ↔ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ ( Poly ‘ 𝑆 ) ) ) ) |
10 |
|
fveq2 |
⊢ ( 𝑥 = 𝑁 → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) = ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ) |
11 |
10
|
eleq1d |
⊢ ( 𝑥 = 𝑁 → ( ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) ∈ ( Poly ‘ 𝑆 ) ↔ ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ 𝑆 ) ) ) |
12 |
11
|
imbi2d |
⊢ ( 𝑥 = 𝑁 → ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑥 ) ∈ ( Poly ‘ 𝑆 ) ) ↔ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ 𝑆 ) ) ) ) |
13 |
|
ssid |
⊢ ℂ ⊆ ℂ |
14 |
|
cnex |
⊢ ℂ ∈ V |
15 |
|
plyf |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ ) |
16 |
15
|
adantl |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 : ℂ ⟶ ℂ ) |
17 |
|
fpmg |
⊢ ( ( ℂ ∈ V ∧ ℂ ∈ V ∧ 𝐹 : ℂ ⟶ ℂ ) → 𝐹 ∈ ( ℂ ↑pm ℂ ) ) |
18 |
14 14 16 17
|
mp3an12i |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 ∈ ( ℂ ↑pm ℂ ) ) |
19 |
|
dvn0 |
⊢ ( ( ℂ ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm ℂ ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 0 ) = 𝐹 ) |
20 |
13 18 19
|
sylancr |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 0 ) = 𝐹 ) |
21 |
|
simpr |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) ) |
22 |
20 21
|
eqeltrd |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 0 ) ∈ ( Poly ‘ 𝑆 ) ) |
23 |
|
dvply2g |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) ) → ( ℂ D ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ) ∈ ( Poly ‘ 𝑆 ) ) |
24 |
23
|
ex |
⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → ( ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) → ( ℂ D ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ) ∈ ( Poly ‘ 𝑆 ) ) ) |
25 |
24
|
ad2antrr |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) → ( ℂ D ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ) ∈ ( Poly ‘ 𝑆 ) ) ) |
26 |
|
dvnp1 |
⊢ ( ( ℂ ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ℂ D ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ) ) |
27 |
13 26
|
mp3an1 |
⊢ ( ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ℂ D ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ) ) |
28 |
18 27
|
sylan |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ℂ D ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ) ) |
29 |
28
|
eleq1d |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ ( Poly ‘ 𝑆 ) ↔ ( ℂ D ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ) ∈ ( Poly ‘ 𝑆 ) ) ) |
30 |
25 29
|
sylibrd |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) → ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ ( Poly ‘ 𝑆 ) ) ) |
31 |
30
|
expcom |
⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) → ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ ( Poly ‘ 𝑆 ) ) ) ) |
32 |
31
|
a2d |
⊢ ( 𝑛 ∈ ℕ0 → ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑛 ) ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ ( Poly ‘ 𝑆 ) ) ) ) |
33 |
3 6 9 12 22 32
|
nn0ind |
⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ 𝑆 ) ) ) |
34 |
33
|
impcom |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ 𝑆 ) ) |
35 |
34
|
3impa |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ℂ D𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( Poly ‘ 𝑆 ) ) |