Step | Hyp | Ref
| Expression |
1 | | dvntaylp.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
2 | | nn0uz 11722 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
3 | 1, 2 | syl6eleq 2711 |
. . . 4
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
4 | | eluzfz2b 12350 |
. . . 4
⊢ (𝑀 ∈
(ℤ≥‘0) ↔ 𝑀 ∈ (0...𝑀)) |
5 | 3, 4 | sylib 208 |
. . 3
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) |
6 | | fveq2 6191 |
. . . . . 6
⊢ (𝑚 = 0 → ((ℂ
D𝑛 ((𝑁 +
𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑚) = ((ℂ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘0)) |
7 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑚 = 0 → ((𝑆 D𝑛 𝐹)‘𝑚) = ((𝑆 D𝑛 𝐹)‘0)) |
8 | 7 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑚 = 0 → (𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑚)) = (𝑆 Tayl ((𝑆 D𝑛 𝐹)‘0))) |
9 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑚 = 0 → (𝑀 − 𝑚) = (𝑀 − 0)) |
10 | 9 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑚 = 0 → (𝑁 + (𝑀 − 𝑚)) = (𝑁 + (𝑀 − 0))) |
11 | | eqidd 2623 |
. . . . . . 7
⊢ (𝑚 = 0 → 𝐵 = 𝐵) |
12 | 8, 10, 11 | oveq123d 6671 |
. . . . . 6
⊢ (𝑚 = 0 → ((𝑁 + (𝑀 − 𝑚))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑚))𝐵) = ((𝑁 + (𝑀 − 0))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘0))𝐵)) |
13 | 6, 12 | eqeq12d 2637 |
. . . . 5
⊢ (𝑚 = 0 → (((ℂ
D𝑛 ((𝑁 +
𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑚) = ((𝑁 + (𝑀 − 𝑚))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑚))𝐵) ↔ ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘0) = ((𝑁 + (𝑀 − 0))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘0))𝐵))) |
14 | 13 | imbi2d 330 |
. . . 4
⊢ (𝑚 = 0 → ((𝜑 → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑚) = ((𝑁 + (𝑀 − 𝑚))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑚))𝐵)) ↔ (𝜑 → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘0) = ((𝑁 + (𝑀 − 0))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘0))𝐵)))) |
15 | | fveq2 6191 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑚) = ((ℂ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑛)) |
16 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → ((𝑆 D𝑛 𝐹)‘𝑚) = ((𝑆 D𝑛 𝐹)‘𝑛)) |
17 | 16 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑚)) = (𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑛))) |
18 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (𝑀 − 𝑚) = (𝑀 − 𝑛)) |
19 | 18 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑁 + (𝑀 − 𝑚)) = (𝑁 + (𝑀 − 𝑛))) |
20 | | eqidd 2623 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → 𝐵 = 𝐵) |
21 | 17, 19, 20 | oveq123d 6671 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((𝑁 + (𝑀 − 𝑚))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑚))𝐵) = ((𝑁 + (𝑀 − 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑛))𝐵)) |
22 | 15, 21 | eqeq12d 2637 |
. . . . 5
⊢ (𝑚 = 𝑛 → (((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑚) = ((𝑁 + (𝑀 − 𝑚))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑚))𝐵) ↔ ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑛) = ((𝑁 + (𝑀 − 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑛))𝐵))) |
23 | 22 | imbi2d 330 |
. . . 4
⊢ (𝑚 = 𝑛 → ((𝜑 → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑚) = ((𝑁 + (𝑀 − 𝑚))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑚))𝐵)) ↔ (𝜑 → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑛) = ((𝑁 + (𝑀 − 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑛))𝐵)))) |
24 | | fveq2 6191 |
. . . . . 6
⊢ (𝑚 = (𝑛 + 1) → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑚) = ((ℂ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘(𝑛 + 1))) |
25 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 + 1) → ((𝑆 D𝑛 𝐹)‘𝑚) = ((𝑆 D𝑛 𝐹)‘(𝑛 + 1))) |
26 | 25 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑚 = (𝑛 + 1) → (𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑚)) = (𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑛 + 1)))) |
27 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 + 1) → (𝑀 − 𝑚) = (𝑀 − (𝑛 + 1))) |
28 | 27 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑚 = (𝑛 + 1) → (𝑁 + (𝑀 − 𝑚)) = (𝑁 + (𝑀 − (𝑛 + 1)))) |
29 | | eqidd 2623 |
. . . . . . 7
⊢ (𝑚 = (𝑛 + 1) → 𝐵 = 𝐵) |
30 | 26, 28, 29 | oveq123d 6671 |
. . . . . 6
⊢ (𝑚 = (𝑛 + 1) → ((𝑁 + (𝑀 − 𝑚))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑚))𝐵) = ((𝑁 + (𝑀 − (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑛 + 1)))𝐵)) |
31 | 24, 30 | eqeq12d 2637 |
. . . . 5
⊢ (𝑚 = (𝑛 + 1) → (((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑚) = ((𝑁 + (𝑀 − 𝑚))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑚))𝐵) ↔ ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘(𝑛 + 1)) = ((𝑁 + (𝑀 − (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑛 + 1)))𝐵))) |
32 | 31 | imbi2d 330 |
. . . 4
⊢ (𝑚 = (𝑛 + 1) → ((𝜑 → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑚) = ((𝑁 + (𝑀 − 𝑚))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑚))𝐵)) ↔ (𝜑 → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘(𝑛 + 1)) = ((𝑁 + (𝑀 − (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑛 + 1)))𝐵)))) |
33 | | fveq2 6191 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑚) = ((ℂ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑀)) |
34 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → ((𝑆 D𝑛 𝐹)‘𝑚) = ((𝑆 D𝑛 𝐹)‘𝑀)) |
35 | 34 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑚)) = (𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑀))) |
36 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (𝑀 − 𝑚) = (𝑀 − 𝑀)) |
37 | 36 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (𝑁 + (𝑀 − 𝑚)) = (𝑁 + (𝑀 − 𝑀))) |
38 | | eqidd 2623 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → 𝐵 = 𝐵) |
39 | 35, 37, 38 | oveq123d 6671 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ((𝑁 + (𝑀 − 𝑚))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑚))𝐵) = ((𝑁 + (𝑀 − 𝑀))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑀))𝐵)) |
40 | 33, 39 | eqeq12d 2637 |
. . . . 5
⊢ (𝑚 = 𝑀 → (((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑚) = ((𝑁 + (𝑀 − 𝑚))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑚))𝐵) ↔ ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑀) = ((𝑁 + (𝑀 − 𝑀))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑀))𝐵))) |
41 | 40 | imbi2d 330 |
. . . 4
⊢ (𝑚 = 𝑀 → ((𝜑 → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑚) = ((𝑁 + (𝑀 − 𝑚))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑚))𝐵)) ↔ (𝜑 → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑀) = ((𝑁 + (𝑀 − 𝑀))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑀))𝐵)))) |
42 | | ssid 3624 |
. . . . . . . 8
⊢ ℂ
⊆ ℂ |
43 | 42 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℂ ⊆
ℂ) |
44 | | mapsspm 7891 |
. . . . . . . 8
⊢ (ℂ
↑𝑚 ℂ) ⊆ (ℂ ↑pm
ℂ) |
45 | | dvntaylp.s |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
46 | | dvntaylp.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
47 | | dvntaylp.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
48 | | dvntaylp.n |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
49 | 48, 1 | nn0addcld 11355 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 + 𝑀) ∈
ℕ0) |
50 | | dvntaylp.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(𝑁 + 𝑀))) |
51 | | eqid 2622 |
. . . . . . . . . 10
⊢ ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵) = ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵) |
52 | 45, 46, 47, 49, 50, 51 | taylpf 24120 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵):ℂ⟶ℂ) |
53 | | cnex 10017 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
54 | 53, 53 | elmap 7886 |
. . . . . . . . 9
⊢ (((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵) ∈ (ℂ ↑𝑚
ℂ) ↔ ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵):ℂ⟶ℂ) |
55 | 52, 54 | sylibr 224 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵) ∈ (ℂ ↑𝑚
ℂ)) |
56 | 44, 55 | sseldi 3601 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵) ∈ (ℂ ↑pm
ℂ)) |
57 | | dvn0 23687 |
. . . . . . 7
⊢ ((ℂ
⊆ ℂ ∧ ((𝑁 +
𝑀)(𝑆 Tayl 𝐹)𝐵) ∈ (ℂ ↑pm
ℂ)) → ((ℂ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘0) = ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵)) |
58 | 43, 56, 57 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ((ℂ
D𝑛 ((𝑁 +
𝑀)(𝑆 Tayl 𝐹)𝐵))‘0) = ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵)) |
59 | | recnprss 23668 |
. . . . . . . . . 10
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
60 | 45, 59 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
61 | 53 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℂ ∈
V) |
62 | | elpm2r 7875 |
. . . . . . . . . 10
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
63 | 61, 45, 46, 47, 62 | syl22anc 1327 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
64 | | dvn0 23687 |
. . . . . . . . 9
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘0) = 𝐹) |
65 | 60, 63, 64 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘0) = 𝐹) |
66 | 65 | oveq2d 6666 |
. . . . . . 7
⊢ (𝜑 → (𝑆 Tayl ((𝑆 D𝑛 𝐹)‘0)) = (𝑆 Tayl 𝐹)) |
67 | 1 | nn0cnd 11353 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℂ) |
68 | 67 | subid1d 10381 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 − 0) = 𝑀) |
69 | 68 | oveq2d 6666 |
. . . . . . 7
⊢ (𝜑 → (𝑁 + (𝑀 − 0)) = (𝑁 + 𝑀)) |
70 | | eqidd 2623 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = 𝐵) |
71 | 66, 69, 70 | oveq123d 6671 |
. . . . . 6
⊢ (𝜑 → ((𝑁 + (𝑀 − 0))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘0))𝐵) = ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵)) |
72 | 58, 71 | eqtr4d 2659 |
. . . . 5
⊢ (𝜑 → ((ℂ
D𝑛 ((𝑁 +
𝑀)(𝑆 Tayl 𝐹)𝐵))‘0) = ((𝑁 + (𝑀 − 0))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘0))𝐵)) |
73 | 72 | a1i 11 |
. . . 4
⊢ (𝑀 ∈
(ℤ≥‘0) → (𝜑 → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘0) = ((𝑁 + (𝑀 − 0))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘0))𝐵))) |
74 | | oveq2 6658 |
. . . . . . 7
⊢
(((ℂ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑛) = ((𝑁 + (𝑀 − 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑛))𝐵) → (ℂ D ((ℂ
D𝑛 ((𝑁 +
𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑛)) = (ℂ D ((𝑁 + (𝑀 − 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑛))𝐵))) |
75 | 42 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → ℂ ⊆
ℂ) |
76 | 56 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵) ∈ (ℂ ↑pm
ℂ)) |
77 | | elfzouz 12474 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (0..^𝑀) → 𝑛 ∈
(ℤ≥‘0)) |
78 | 77 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → 𝑛 ∈
(ℤ≥‘0)) |
79 | 78, 2 | syl6eleqr 2712 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → 𝑛 ∈ ℕ0) |
80 | | dvnp1 23688 |
. . . . . . . . 9
⊢ ((ℂ
⊆ ℂ ∧ ((𝑁 +
𝑀)(𝑆 Tayl 𝐹)𝐵) ∈ (ℂ ↑pm
ℂ) ∧ 𝑛 ∈
ℕ0) → ((ℂ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘(𝑛 + 1)) = (ℂ D ((ℂ
D𝑛 ((𝑁 +
𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑛))) |
81 | 75, 76, 79, 80 | syl3anc 1326 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘(𝑛 + 1)) = (ℂ D ((ℂ
D𝑛 ((𝑁 +
𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑛))) |
82 | 45 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → 𝑆 ∈ {ℝ, ℂ}) |
83 | 63 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
84 | | dvnf 23690 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆) ∧ 𝑛 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑛):dom ((𝑆 D𝑛 𝐹)‘𝑛)⟶ℂ) |
85 | 82, 83, 79, 84 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → ((𝑆 D𝑛 𝐹)‘𝑛):dom ((𝑆 D𝑛 𝐹)‘𝑛)⟶ℂ) |
86 | | dvnbss 23691 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆) ∧ 𝑛 ∈ ℕ0) → dom
((𝑆 D𝑛
𝐹)‘𝑛) ⊆ dom 𝐹) |
87 | 82, 83, 79, 86 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → dom ((𝑆 D𝑛 𝐹)‘𝑛) ⊆ dom 𝐹) |
88 | | fdm 6051 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴) |
89 | 46, 88 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom 𝐹 = 𝐴) |
90 | 89 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → dom 𝐹 = 𝐴) |
91 | 87, 90 | sseqtrd 3641 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → dom ((𝑆 D𝑛 𝐹)‘𝑛) ⊆ 𝐴) |
92 | 47 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → 𝐴 ⊆ 𝑆) |
93 | 91, 92 | sstrd 3613 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → dom ((𝑆 D𝑛 𝐹)‘𝑛) ⊆ 𝑆) |
94 | 48 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → 𝑁 ∈
ℕ0) |
95 | | fzofzp1 12565 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (0..^𝑀) → (𝑛 + 1) ∈ (0...𝑀)) |
96 | 95 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (𝑛 + 1) ∈ (0...𝑀)) |
97 | | fznn0sub 12373 |
. . . . . . . . . . . 12
⊢ ((𝑛 + 1) ∈ (0...𝑀) → (𝑀 − (𝑛 + 1)) ∈
ℕ0) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (𝑀 − (𝑛 + 1)) ∈
ℕ0) |
99 | 94, 98 | nn0addcld 11355 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (𝑁 + (𝑀 − (𝑛 + 1))) ∈
ℕ0) |
100 | 50 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(𝑁 + 𝑀))) |
101 | | elfzofz 12485 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (0..^𝑀) → 𝑛 ∈ (0...𝑀)) |
102 | 101 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → 𝑛 ∈ (0...𝑀)) |
103 | | fznn0sub 12373 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (0...𝑀) → (𝑀 − 𝑛) ∈
ℕ0) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (𝑀 − 𝑛) ∈
ℕ0) |
105 | 94, 104 | nn0addcld 11355 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (𝑁 + (𝑀 − 𝑛)) ∈
ℕ0) |
106 | | dvnadd 23692 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (𝑛 ∈ ℕ0 ∧ (𝑁 + (𝑀 − 𝑛)) ∈ ℕ0)) →
((𝑆 D𝑛
((𝑆 D𝑛
𝐹)‘𝑛))‘(𝑁 + (𝑀 − 𝑛))) = ((𝑆 D𝑛 𝐹)‘(𝑛 + (𝑁 + (𝑀 − 𝑛))))) |
107 | 82, 83, 79, 105, 106 | syl22anc 1327 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑛))‘(𝑁 + (𝑀 − 𝑛))) = ((𝑆 D𝑛 𝐹)‘(𝑛 + (𝑁 + (𝑀 − 𝑛))))) |
108 | 48 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ ℂ) |
109 | 108 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → 𝑁 ∈ ℂ) |
110 | 98 | nn0cnd 11353 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (𝑀 − (𝑛 + 1)) ∈ ℂ) |
111 | | 1cnd 10056 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → 1 ∈ ℂ) |
112 | 109, 110,
111 | addassd 10062 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → ((𝑁 + (𝑀 − (𝑛 + 1))) + 1) = (𝑁 + ((𝑀 − (𝑛 + 1)) + 1))) |
113 | 67 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → 𝑀 ∈ ℂ) |
114 | 79 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → 𝑛 ∈ ℂ) |
115 | 113, 114,
111 | nppcan2d 10418 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → ((𝑀 − (𝑛 + 1)) + 1) = (𝑀 − 𝑛)) |
116 | 115 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (𝑁 + ((𝑀 − (𝑛 + 1)) + 1)) = (𝑁 + (𝑀 − 𝑛))) |
117 | 112, 116 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → ((𝑁 + (𝑀 − (𝑛 + 1))) + 1) = (𝑁 + (𝑀 − 𝑛))) |
118 | 117 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑛))‘((𝑁 + (𝑀 − (𝑛 + 1))) + 1)) = ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑛))‘(𝑁 + (𝑀 − 𝑛)))) |
119 | 114, 113 | pncan3d 10395 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (𝑛 + (𝑀 − 𝑛)) = 𝑀) |
120 | 119 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (𝑁 + (𝑛 + (𝑀 − 𝑛))) = (𝑁 + 𝑀)) |
121 | 113, 114 | subcld 10392 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (𝑀 − 𝑛) ∈ ℂ) |
122 | 109, 114,
121 | add12d 10262 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (𝑁 + (𝑛 + (𝑀 − 𝑛))) = (𝑛 + (𝑁 + (𝑀 − 𝑛)))) |
123 | 120, 122 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (𝑁 + 𝑀) = (𝑛 + (𝑁 + (𝑀 − 𝑛)))) |
124 | 123 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → ((𝑆 D𝑛 𝐹)‘(𝑁 + 𝑀)) = ((𝑆 D𝑛 𝐹)‘(𝑛 + (𝑁 + (𝑀 − 𝑛))))) |
125 | 107, 118,
124 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑛))‘((𝑁 + (𝑀 − (𝑛 + 1))) + 1)) = ((𝑆 D𝑛 𝐹)‘(𝑁 + 𝑀))) |
126 | 125 | dmeqd 5326 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑛))‘((𝑁 + (𝑀 − (𝑛 + 1))) + 1)) = dom ((𝑆 D𝑛 𝐹)‘(𝑁 + 𝑀))) |
127 | 100, 126 | eleqtrrd 2704 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → 𝐵 ∈ dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑛))‘((𝑁 + (𝑀 − (𝑛 + 1))) + 1))) |
128 | 82, 85, 93, 99, 127 | dvtaylp 24124 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (ℂ D (((𝑁 + (𝑀 − (𝑛 + 1))) + 1)(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑛))𝐵)) = ((𝑁 + (𝑀 − (𝑛 + 1)))(𝑆 Tayl (𝑆 D ((𝑆 D𝑛 𝐹)‘𝑛)))𝐵)) |
129 | 117 | oveq1d 6665 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (((𝑁 + (𝑀 − (𝑛 + 1))) + 1)(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑛))𝐵) = ((𝑁 + (𝑀 − 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑛))𝐵)) |
130 | 129 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (ℂ D (((𝑁 + (𝑀 − (𝑛 + 1))) + 1)(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑛))𝐵)) = (ℂ D ((𝑁 + (𝑀 − 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑛))𝐵))) |
131 | 60 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → 𝑆 ⊆ ℂ) |
132 | | dvnp1 23688 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆) ∧ 𝑛 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘(𝑛 + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘𝑛))) |
133 | 131, 83, 79, 132 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → ((𝑆 D𝑛 𝐹)‘(𝑛 + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘𝑛))) |
134 | 133 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑛 + 1))) = (𝑆 Tayl (𝑆 D ((𝑆 D𝑛 𝐹)‘𝑛)))) |
135 | 134 | eqcomd 2628 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (𝑆 Tayl (𝑆 D ((𝑆 D𝑛 𝐹)‘𝑛))) = (𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑛 + 1)))) |
136 | 135 | oveqd 6667 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → ((𝑁 + (𝑀 − (𝑛 + 1)))(𝑆 Tayl (𝑆 D ((𝑆 D𝑛 𝐹)‘𝑛)))𝐵) = ((𝑁 + (𝑀 − (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑛 + 1)))𝐵)) |
137 | 128, 130,
136 | 3eqtr3rd 2665 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → ((𝑁 + (𝑀 − (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑛 + 1)))𝐵) = (ℂ D ((𝑁 + (𝑀 − 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑛))𝐵))) |
138 | 81, 137 | eqeq12d 2637 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘(𝑛 + 1)) = ((𝑁 + (𝑀 − (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑛 + 1)))𝐵) ↔ (ℂ D ((ℂ
D𝑛 ((𝑁 +
𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑛)) = (ℂ D ((𝑁 + (𝑀 − 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑛))𝐵)))) |
139 | 74, 138 | syl5ibr 236 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑀)) → (((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑛) = ((𝑁 + (𝑀 − 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑛))𝐵) → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘(𝑛 + 1)) = ((𝑁 + (𝑀 − (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑛 + 1)))𝐵))) |
140 | 139 | expcom 451 |
. . . . 5
⊢ (𝑛 ∈ (0..^𝑀) → (𝜑 → (((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑛) = ((𝑁 + (𝑀 − 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑛))𝐵) → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘(𝑛 + 1)) = ((𝑁 + (𝑀 − (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑛 + 1)))𝐵)))) |
141 | 140 | a2d 29 |
. . . 4
⊢ (𝑛 ∈ (0..^𝑀) → ((𝜑 → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑛) = ((𝑁 + (𝑀 − 𝑛))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑛))𝐵)) → (𝜑 → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘(𝑛 + 1)) = ((𝑁 + (𝑀 − (𝑛 + 1)))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑛 + 1)))𝐵)))) |
142 | 14, 23, 32, 41, 73, 141 | fzind2 12586 |
. . 3
⊢ (𝑀 ∈ (0...𝑀) → (𝜑 → ((ℂ D𝑛
((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑀) = ((𝑁 + (𝑀 − 𝑀))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑀))𝐵))) |
143 | 5, 142 | mpcom 38 |
. 2
⊢ (𝜑 → ((ℂ
D𝑛 ((𝑁 +
𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑀) = ((𝑁 + (𝑀 − 𝑀))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑀))𝐵)) |
144 | 67 | subidd 10380 |
. . . . 5
⊢ (𝜑 → (𝑀 − 𝑀) = 0) |
145 | 144 | oveq2d 6666 |
. . . 4
⊢ (𝜑 → (𝑁 + (𝑀 − 𝑀)) = (𝑁 + 0)) |
146 | 108 | addid1d 10236 |
. . . 4
⊢ (𝜑 → (𝑁 + 0) = 𝑁) |
147 | 145, 146 | eqtrd 2656 |
. . 3
⊢ (𝜑 → (𝑁 + (𝑀 − 𝑀)) = 𝑁) |
148 | 147 | oveq1d 6665 |
. 2
⊢ (𝜑 → ((𝑁 + (𝑀 − 𝑀))(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑀))𝐵) = (𝑁(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑀))𝐵)) |
149 | 143, 148 | eqtrd 2656 |
1
⊢ (𝜑 → ((ℂ
D𝑛 ((𝑁 +
𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑀) = (𝑁(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑀))𝐵)) |