Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . 6
⊢ (𝑛 = 0 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘0)) |
2 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑛 = 0 → (𝑀 + 𝑛) = (𝑀 + 0)) |
3 | 2 | fveq2d 6195 |
. . . . . 6
⊢ (𝑛 = 0 → ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 0))) |
4 | 1, 3 | eqeq12d 2637 |
. . . . 5
⊢ (𝑛 = 0 → (((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛)) ↔ ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘0) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 0)))) |
5 | 4 | imbi2d 330 |
. . . 4
⊢ (𝑛 = 0 → ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛))) ↔ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘0) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 0))))) |
6 | | fveq2 6191 |
. . . . . 6
⊢ (𝑛 = 𝑘 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘)) |
7 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑀 + 𝑛) = (𝑀 + 𝑘)) |
8 | 7 | fveq2d 6195 |
. . . . . 6
⊢ (𝑛 = 𝑘 → ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘))) |
9 | 6, 8 | eqeq12d 2637 |
. . . . 5
⊢ (𝑛 = 𝑘 → (((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛)) ↔ ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘)))) |
10 | 9 | imbi2d 330 |
. . . 4
⊢ (𝑛 = 𝑘 → ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛))) ↔ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘))))) |
11 | | fveq2 6191 |
. . . . . 6
⊢ (𝑛 = (𝑘 + 1) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘(𝑘 + 1))) |
12 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑛 = (𝑘 + 1) → (𝑀 + 𝑛) = (𝑀 + (𝑘 + 1))) |
13 | 12 | fveq2d 6195 |
. . . . . 6
⊢ (𝑛 = (𝑘 + 1) → ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + (𝑘 + 1)))) |
14 | 11, 13 | eqeq12d 2637 |
. . . . 5
⊢ (𝑛 = (𝑘 + 1) → (((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛)) ↔ ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘(𝑘 + 1)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + (𝑘 + 1))))) |
15 | 14 | imbi2d 330 |
. . . 4
⊢ (𝑛 = (𝑘 + 1) → ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛))) ↔ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘(𝑘 + 1)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + (𝑘 + 1)))))) |
16 | | fveq2 6191 |
. . . . . 6
⊢ (𝑛 = 𝑁 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑁)) |
17 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝑀 + 𝑛) = (𝑀 + 𝑁)) |
18 | 17 | fveq2d 6195 |
. . . . . 6
⊢ (𝑛 = 𝑁 → ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑁))) |
19 | 16, 18 | eqeq12d 2637 |
. . . . 5
⊢ (𝑛 = 𝑁 → (((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛)) ↔ ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑁) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑁)))) |
20 | 19 | imbi2d 330 |
. . . 4
⊢ (𝑛 = 𝑁 → ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛))) ↔ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑁) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑁))))) |
21 | | recnprss 23668 |
. . . . . . 7
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
22 | 21 | ad2antrr 762 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → 𝑆 ⊆
ℂ) |
23 | | ssid 3624 |
. . . . . . . . . 10
⊢ ℂ
⊆ ℂ |
24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) → ℂ ⊆
ℂ) |
25 | | cnex 10017 |
. . . . . . . . . . 11
⊢ ℂ
∈ V |
26 | | elpm2g 7874 |
. . . . . . . . . . 11
⊢ ((ℂ
∈ V ∧ 𝑆 ∈
{ℝ, ℂ}) → (𝐹 ∈ (ℂ ↑pm
𝑆) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆))) |
27 | 25, 26 | mpan 706 |
. . . . . . . . . 10
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝐹 ∈ (ℂ
↑pm 𝑆) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆))) |
28 | 27 | simplbda 654 |
. . . . . . . . 9
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) → dom 𝐹 ⊆ 𝑆) |
29 | 25 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) → ℂ ∈ V) |
30 | | simpl 473 |
. . . . . . . . 9
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) → 𝑆 ∈ {ℝ, ℂ}) |
31 | | pmss12g 7884 |
. . . . . . . . 9
⊢
(((ℂ ⊆ ℂ ∧ dom 𝐹 ⊆ 𝑆) ∧ (ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}))
→ (ℂ ↑pm dom 𝐹) ⊆ (ℂ
↑pm 𝑆)) |
32 | 24, 28, 29, 30, 31 | syl22anc 1327 |
. . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) → (ℂ
↑pm dom 𝐹) ⊆ (ℂ
↑pm 𝑆)) |
33 | 32 | adantr 481 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → (ℂ
↑pm dom 𝐹) ⊆ (ℂ
↑pm 𝑆)) |
34 | | dvnff 23686 |
. . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) → (𝑆 D𝑛 𝐹):ℕ0⟶(ℂ
↑pm dom 𝐹)) |
35 | 34 | ffvelrnda 6359 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑀) ∈ (ℂ ↑pm
dom 𝐹)) |
36 | 33, 35 | sseldd 3604 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑀) ∈ (ℂ ↑pm
𝑆)) |
37 | | dvn0 23687 |
. . . . . 6
⊢ ((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝐹)‘𝑀) ∈ (ℂ ↑pm
𝑆)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘0) = ((𝑆 D𝑛 𝐹)‘𝑀)) |
38 | 22, 36, 37 | syl2anc 693 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘0) = ((𝑆 D𝑛 𝐹)‘𝑀)) |
39 | | nn0cn 11302 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℂ) |
40 | 39 | adantl 482 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈
ℂ) |
41 | 40 | addid1d 10236 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → (𝑀 + 0) = 𝑀) |
42 | 41 | fveq2d 6195 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘(𝑀 + 0)) = ((𝑆 D𝑛 𝐹)‘𝑀)) |
43 | 38, 42 | eqtr4d 2659 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘0) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 0))) |
44 | | oveq2 6658 |
. . . . . . 7
⊢ (((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘)) → (𝑆 D ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘)))) |
45 | 22 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑆 ⊆
ℂ) |
46 | 36 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑆
D𝑛 𝐹)‘𝑀) ∈ (ℂ ↑pm
𝑆)) |
47 | | simpr 477 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℕ0) |
48 | | dvnp1 23688 |
. . . . . . . . 9
⊢ ((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝐹)‘𝑀) ∈ (ℂ ↑pm
𝑆) ∧ 𝑘 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘(𝑘 + 1)) = (𝑆 D ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘))) |
49 | 45, 46, 47, 48 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑆
D𝑛 ((𝑆
D𝑛 𝐹)‘𝑀))‘(𝑘 + 1)) = (𝑆 D ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘))) |
50 | 40 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑀 ∈
ℂ) |
51 | | nn0cn 11302 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
52 | 51 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℂ) |
53 | | 1cnd 10056 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 1 ∈ ℂ) |
54 | 50, 52, 53 | addassd 10062 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑀 + 𝑘) + 1) = (𝑀 + (𝑘 + 1))) |
55 | 54 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑆
D𝑛 𝐹)‘((𝑀 + 𝑘) + 1)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + (𝑘 + 1)))) |
56 | | simpllr 799 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝐹 ∈ (ℂ
↑pm 𝑆)) |
57 | | nn0addcl 11328 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑀 + 𝑘) ∈
ℕ0) |
58 | 57 | adantll 750 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝑀 + 𝑘) ∈
ℕ0) |
59 | | dvnp1 23688 |
. . . . . . . . . 10
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆) ∧ (𝑀 + 𝑘) ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘((𝑀 + 𝑘) + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘)))) |
60 | 45, 56, 58, 59 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑆
D𝑛 𝐹)‘((𝑀 + 𝑘) + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘)))) |
61 | 55, 60 | eqtr3d 2658 |
. . . . . . . 8
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑆
D𝑛 𝐹)‘(𝑀 + (𝑘 + 1))) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘)))) |
62 | 49, 61 | eqeq12d 2637 |
. . . . . . 7
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (((𝑆
D𝑛 ((𝑆
D𝑛 𝐹)‘𝑀))‘(𝑘 + 1)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + (𝑘 + 1))) ↔ (𝑆 D ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘))))) |
63 | 44, 62 | syl5ibr 236 |
. . . . . 6
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (((𝑆
D𝑛 ((𝑆
D𝑛 𝐹)‘𝑀))‘𝑘) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘(𝑘 + 1)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + (𝑘 + 1))))) |
64 | 63 | expcom 451 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ (((𝑆 ∈
{ℝ, ℂ} ∧ 𝐹
∈ (ℂ ↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → (((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘(𝑘 + 1)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + (𝑘 + 1)))))) |
65 | 64 | a2d 29 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ ((((𝑆 ∈
{ℝ, ℂ} ∧ 𝐹
∈ (ℂ ↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘))) → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘(𝑘 + 1)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + (𝑘 + 1)))))) |
66 | 5, 10, 15, 20, 43, 65 | nn0ind 11472 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (((𝑆 ∈
{ℝ, ℂ} ∧ 𝐹
∈ (ℂ ↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑁) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑁)))) |
67 | 66 | com12 32 |
. 2
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → (𝑁 ∈ ℕ0
→ ((𝑆
D𝑛 ((𝑆
D𝑛 𝐹)‘𝑀))‘𝑁) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑁)))) |
68 | 67 | impr 649 |
1
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))
→ ((𝑆
D𝑛 ((𝑆
D𝑛 𝐹)‘𝑀))‘𝑁) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑁))) |