Step | Hyp | Ref
| Expression |
1 | | fveq2 6717 |
. . . . . 6
⊢ (𝑛 = 0 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘0)) |
2 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑛 = 0 → (𝑀 + 𝑛) = (𝑀 + 0)) |
3 | 2 | fveq2d 6721 |
. . . . . 6
⊢ (𝑛 = 0 → ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 0))) |
4 | 1, 3 | eqeq12d 2753 |
. . . . 5
⊢ (𝑛 = 0 → (((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛)) ↔ ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘0) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 0)))) |
5 | 4 | imbi2d 344 |
. . . 4
⊢ (𝑛 = 0 → ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛))) ↔ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘0) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 0))))) |
6 | | fveq2 6717 |
. . . . . 6
⊢ (𝑛 = 𝑘 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘)) |
7 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑀 + 𝑛) = (𝑀 + 𝑘)) |
8 | 7 | fveq2d 6721 |
. . . . . 6
⊢ (𝑛 = 𝑘 → ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘))) |
9 | 6, 8 | eqeq12d 2753 |
. . . . 5
⊢ (𝑛 = 𝑘 → (((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛)) ↔ ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘)))) |
10 | 9 | imbi2d 344 |
. . . 4
⊢ (𝑛 = 𝑘 → ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛))) ↔ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘))))) |
11 | | fveq2 6717 |
. . . . . 6
⊢ (𝑛 = (𝑘 + 1) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘(𝑘 + 1))) |
12 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑛 = (𝑘 + 1) → (𝑀 + 𝑛) = (𝑀 + (𝑘 + 1))) |
13 | 12 | fveq2d 6721 |
. . . . . 6
⊢ (𝑛 = (𝑘 + 1) → ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + (𝑘 + 1)))) |
14 | 11, 13 | eqeq12d 2753 |
. . . . 5
⊢ (𝑛 = (𝑘 + 1) → (((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛)) ↔ ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘(𝑘 + 1)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + (𝑘 + 1))))) |
15 | 14 | imbi2d 344 |
. . . 4
⊢ (𝑛 = (𝑘 + 1) → ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛))) ↔ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘(𝑘 + 1)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + (𝑘 + 1)))))) |
16 | | fveq2 6717 |
. . . . . 6
⊢ (𝑛 = 𝑁 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑁)) |
17 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝑀 + 𝑛) = (𝑀 + 𝑁)) |
18 | 17 | fveq2d 6721 |
. . . . . 6
⊢ (𝑛 = 𝑁 → ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑁))) |
19 | 16, 18 | eqeq12d 2753 |
. . . . 5
⊢ (𝑛 = 𝑁 → (((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛)) ↔ ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑁) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑁)))) |
20 | 19 | imbi2d 344 |
. . . 4
⊢ (𝑛 = 𝑁 → ((((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑛) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑛))) ↔ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑁) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑁))))) |
21 | | recnprss 24801 |
. . . . . . 7
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
22 | 21 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → 𝑆 ⊆ ℂ) |
23 | | ssidd 3924 |
. . . . . . . . 9
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
→ ℂ ⊆ ℂ) |
24 | | cnex 10810 |
. . . . . . . . . . 11
⊢ ℂ
∈ V |
25 | | elpm2g 8525 |
. . . . . . . . . . 11
⊢ ((ℂ
∈ V ∧ 𝑆 ∈
{ℝ, ℂ}) → (𝐹 ∈ (ℂ ↑pm 𝑆) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆))) |
26 | 24, 25 | mpan 690 |
. . . . . . . . . 10
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝐹 ∈ (ℂ
↑pm 𝑆)
↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ 𝑆))) |
27 | 26 | simplbda 503 |
. . . . . . . . 9
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
→ dom 𝐹 ⊆ 𝑆) |
28 | 24 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
→ ℂ ∈ V) |
29 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
→ 𝑆 ∈ {ℝ,
ℂ}) |
30 | | pmss12g 8550 |
. . . . . . . . 9
⊢
(((ℂ ⊆ ℂ ∧ dom 𝐹 ⊆ 𝑆) ∧ (ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}))
→ (ℂ ↑pm dom 𝐹) ⊆ (ℂ ↑pm 𝑆)) |
31 | 23, 27, 28, 29, 30 | syl22anc 839 |
. . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
→ (ℂ ↑pm dom 𝐹) ⊆ (ℂ ↑pm 𝑆)) |
32 | 31 | adantr 484 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → (ℂ ↑pm dom 𝐹) ⊆ (ℂ ↑pm 𝑆)) |
33 | | dvnff 24820 |
. . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
→ (𝑆
D𝑛 𝐹):ℕ0⟶(ℂ
↑pm dom 𝐹)) |
34 | 33 | ffvelrnda 6904 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑀) ∈ (ℂ ↑pm dom
𝐹)) |
35 | 32, 34 | sseldd 3902 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑀) ∈ (ℂ ↑pm 𝑆)) |
36 | | dvn0 24821 |
. . . . . 6
⊢ ((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝐹)‘𝑀) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘0) = ((𝑆 D𝑛 𝐹)‘𝑀)) |
37 | 22, 35, 36 | syl2anc 587 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘0) = ((𝑆 D𝑛 𝐹)‘𝑀)) |
38 | | nn0cn 12100 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℂ) |
39 | 38 | adantl 485 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → 𝑀 ∈ ℂ) |
40 | 39 | addid1d 11032 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → (𝑀 + 0) = 𝑀) |
41 | 40 | fveq2d 6721 |
. . . . 5
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → ((𝑆 D𝑛 𝐹)‘(𝑀 + 0)) = ((𝑆 D𝑛 𝐹)‘𝑀)) |
42 | 37, 41 | eqtr4d 2780 |
. . . 4
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘0) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 0))) |
43 | | oveq2 7221 |
. . . . . . 7
⊢ (((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘)) → (𝑆 D ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘)))) |
44 | 22 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑆 ⊆
ℂ) |
45 | 35 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑀) ∈ (ℂ ↑pm 𝑆)) |
46 | | simpr 488 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
47 | | dvnp1 24822 |
. . . . . . . . 9
⊢ ((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝐹)‘𝑀) ∈ (ℂ ↑pm 𝑆) ∧ 𝑘 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘(𝑘 + 1)) = (𝑆 D ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘))) |
48 | 44, 45, 46, 47 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘(𝑘 + 1)) = (𝑆 D ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘))) |
49 | 39 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈
ℂ) |
50 | | nn0cn 12100 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
51 | 50 | adantl 485 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℂ) |
52 | | 1cnd 10828 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ ℕ0) → 1 ∈
ℂ) |
53 | 49, 51, 52 | addassd 10855 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ ℕ0) → ((𝑀 + 𝑘) + 1) = (𝑀 + (𝑘 + 1))) |
54 | 53 | fveq2d 6721 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘((𝑀 + 𝑘) + 1)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + (𝑘 + 1)))) |
55 | | simpllr 776 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝐹 ∈ (ℂ
↑pm 𝑆)) |
56 | | nn0addcl 12125 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑀 + 𝑘) ∈
ℕ0) |
57 | 56 | adantll 714 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑀 + 𝑘) ∈
ℕ0) |
58 | | dvnp1 24822 |
. . . . . . . . . 10
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)
∧ (𝑀 + 𝑘) ∈ ℕ0)
→ ((𝑆
D𝑛 𝐹)‘((𝑀 + 𝑘) + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘)))) |
59 | 44, 55, 57, 58 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘((𝑀 + 𝑘) + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘)))) |
60 | 54, 59 | eqtr3d 2779 |
. . . . . . . 8
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘(𝑀 + (𝑘 + 1))) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘)))) |
61 | 48, 60 | eqeq12d 2753 |
. . . . . . 7
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ ℕ0) → (((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘(𝑘 + 1)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + (𝑘 + 1))) ↔ (𝑆 D ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘))))) |
62 | 43, 61 | syl5ibr 249 |
. . . . . 6
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ ℕ0) → (((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘(𝑘 + 1)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + (𝑘 + 1))))) |
63 | 62 | expcom 417 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ (((𝑆 ∈
{ℝ, ℂ} ∧ 𝐹
∈ (ℂ ↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → (((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘(𝑘 + 1)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + (𝑘 + 1)))))) |
64 | 63 | a2d 29 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ ((((𝑆 ∈
{ℝ, ℂ} ∧ 𝐹
∈ (ℂ ↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑘) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑘))) → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘(𝑘 + 1)) = ((𝑆 D𝑛 𝐹)‘(𝑀 + (𝑘 + 1)))))) |
65 | 5, 10, 15, 20, 42, 64 | nn0ind 12272 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (((𝑆 ∈
{ℝ, ℂ} ∧ 𝐹
∈ (ℂ ↑pm 𝑆)) ∧ 𝑀 ∈ ℕ0) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑁) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑁)))) |
66 | 65 | com12 32 |
. 2
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑀 ∈
ℕ0) → (𝑁 ∈ ℕ0 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑁) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑁)))) |
67 | 66 | impr 458 |
1
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑀))‘𝑁) = ((𝑆 D𝑛 𝐹)‘(𝑀 + 𝑁))) |