Step | Hyp | Ref
| Expression |
1 | | ssid 3587 |
. . . 4
⊢ ℂ
⊆ ℂ |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → ℂ ⊆
ℂ) |
3 | | coeeu.4 |
. . . 4
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
4 | | coeeu.5 |
. . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
5 | 3, 4 | nn0addcld 11232 |
. . 3
⊢ (𝜑 → (𝑀 + 𝑁) ∈
ℕ0) |
6 | | subcl 10159 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 − 𝑦) ∈ ℂ) |
7 | 6 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 − 𝑦) ∈ ℂ) |
8 | | coeeu.2 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (ℂ ↑𝑚
ℕ0)) |
9 | | cnex 9896 |
. . . . . . . 8
⊢ ℂ
∈ V |
10 | | nn0ex 11175 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
11 | 9, 10 | elmap 7772 |
. . . . . . 7
⊢ (𝐴 ∈ (ℂ
↑𝑚 ℕ0) ↔ 𝐴:ℕ0⟶ℂ) |
12 | 8, 11 | sylib 207 |
. . . . . 6
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
13 | | coeeu.3 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (ℂ ↑𝑚
ℕ0)) |
14 | 9, 10 | elmap 7772 |
. . . . . . 7
⊢ (𝐵 ∈ (ℂ
↑𝑚 ℕ0) ↔ 𝐵:ℕ0⟶ℂ) |
15 | 13, 14 | sylib 207 |
. . . . . 6
⊢ (𝜑 → 𝐵:ℕ0⟶ℂ) |
16 | 10 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℕ0 ∈
V) |
17 | | inidm 3784 |
. . . . . 6
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 |
18 | 7, 12, 15, 16, 16, 17 | off 6810 |
. . . . 5
⊢ (𝜑 → (𝐴 ∘𝑓 − 𝐵):ℕ0⟶ℂ) |
19 | 9, 10 | elmap 7772 |
. . . . 5
⊢ ((𝐴 ∘𝑓
− 𝐵) ∈ (ℂ
↑𝑚 ℕ0) ↔ (𝐴 ∘𝑓 − 𝐵):ℕ0⟶ℂ) |
20 | 18, 19 | sylibr 223 |
. . . 4
⊢ (𝜑 → (𝐴 ∘𝑓 − 𝐵) ∈ (ℂ
↑𝑚 ℕ0)) |
21 | | 0cn 9911 |
. . . . . . 7
⊢ 0 ∈
ℂ |
22 | | snssi 4280 |
. . . . . . 7
⊢ (0 ∈
ℂ → {0} ⊆ ℂ) |
23 | 21, 22 | ax-mp 5 |
. . . . . 6
⊢ {0}
⊆ ℂ |
24 | | ssequn2 3748 |
. . . . . 6
⊢ ({0}
⊆ ℂ ↔ (ℂ ∪ {0}) = ℂ) |
25 | 23, 24 | mpbi 219 |
. . . . 5
⊢ (ℂ
∪ {0}) = ℂ |
26 | 25 | oveq1i 6559 |
. . . 4
⊢ ((ℂ
∪ {0}) ↑𝑚 ℕ0) = (ℂ
↑𝑚 ℕ0) |
27 | 20, 26 | syl6eleqr 2699 |
. . 3
⊢ (𝜑 → (𝐴 ∘𝑓 − 𝐵) ∈ ((ℂ ∪ {0})
↑𝑚 ℕ0)) |
28 | 5 | nn0red 11229 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 + 𝑁) ∈ ℝ) |
29 | | nn0re 11178 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
30 | | ltnle 9996 |
. . . . . . . 8
⊢ (((𝑀 + 𝑁) ∈ ℝ ∧ 𝑘 ∈ ℝ) → ((𝑀 + 𝑁) < 𝑘 ↔ ¬ 𝑘 ≤ (𝑀 + 𝑁))) |
31 | 28, 29, 30 | syl2an 493 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑀 + 𝑁) < 𝑘 ↔ ¬ 𝑘 ≤ (𝑀 + 𝑁))) |
32 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝐴:ℕ0⟶ℂ →
𝐴 Fn
ℕ0) |
33 | 12, 32 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 Fn ℕ0) |
34 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝐵:ℕ0⟶ℂ →
𝐵 Fn
ℕ0) |
35 | 15, 34 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 Fn ℕ0) |
36 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) = (𝐴‘𝑘)) |
37 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐵‘𝑘) = (𝐵‘𝑘)) |
38 | 33, 35, 16, 16, 17, 36, 37 | ofval 6804 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴 ∘𝑓
− 𝐵)‘𝑘) = ((𝐴‘𝑘) − (𝐵‘𝑘))) |
39 | 38 | adantrr 749 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → ((𝐴 ∘𝑓 − 𝐵)‘𝑘) = ((𝐴‘𝑘) − (𝐵‘𝑘))) |
40 | 3 | nn0red 11229 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℝ) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → 𝑀 ∈ ℝ) |
42 | 28 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → (𝑀 + 𝑁) ∈ ℝ) |
43 | 29 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℝ) |
44 | 43 | adantrr 749 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → 𝑘 ∈ ℝ) |
45 | 3 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ ℂ) |
46 | 4 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℂ) |
47 | 45, 46 | addcomd 10117 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀 + 𝑁) = (𝑁 + 𝑀)) |
48 | | nn0uz 11598 |
. . . . . . . . . . . . . . . . . . . 20
⊢
ℕ0 = (ℤ≥‘0) |
49 | 4, 48 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
50 | 3 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ ℤ) |
51 | | eluzadd 11592 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈
(ℤ≥‘0) ∧ 𝑀 ∈ ℤ) → (𝑁 + 𝑀) ∈ (ℤ≥‘(0 +
𝑀))) |
52 | 49, 50, 51 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑁 + 𝑀) ∈ (ℤ≥‘(0 +
𝑀))) |
53 | 47, 52 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 + 𝑁) ∈ (ℤ≥‘(0 +
𝑀))) |
54 | 45 | addid2d 10116 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (0 + 𝑀) = 𝑀) |
55 | 54 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(ℤ≥‘(0 + 𝑀)) = (ℤ≥‘𝑀)) |
56 | 53, 55 | eleqtrd 2690 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀 + 𝑁) ∈ (ℤ≥‘𝑀)) |
57 | | eluzle 11576 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 + 𝑁) ∈ (ℤ≥‘𝑀) → 𝑀 ≤ (𝑀 + 𝑁)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ≤ (𝑀 + 𝑁)) |
59 | 58 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → 𝑀 ≤ (𝑀 + 𝑁)) |
60 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → (𝑀 + 𝑁) < 𝑘) |
61 | 41, 42, 44, 59, 60 | lelttrd 10074 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → 𝑀 < 𝑘) |
62 | 41, 44 | ltnled 10063 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → (𝑀 < 𝑘 ↔ ¬ 𝑘 ≤ 𝑀)) |
63 | 61, 62 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → ¬ 𝑘 ≤ 𝑀) |
64 | | coeeu.6 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) |
65 | | plyco0 23752 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ0
∧ 𝐴:ℕ0⟶ℂ) →
((𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀))) |
66 | 3, 12, 65 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀))) |
67 | 64, 66 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀)) |
68 | 67 | r19.21bi 2916 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀)) |
69 | 68 | adantrr 749 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀)) |
70 | 69 | necon1bd 2800 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → (¬ 𝑘 ≤ 𝑀 → (𝐴‘𝑘) = 0)) |
71 | 63, 70 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → (𝐴‘𝑘) = 0) |
72 | 4 | nn0red 11229 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℝ) |
73 | 72 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → 𝑁 ∈ ℝ) |
74 | 3, 48 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
75 | 4 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℤ) |
76 | | eluzadd 11592 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈
(ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ (ℤ≥‘(0 +
𝑁))) |
77 | 74, 75, 76 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 + 𝑁) ∈ (ℤ≥‘(0 +
𝑁))) |
78 | 46 | addid2d 10116 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (0 + 𝑁) = 𝑁) |
79 | 78 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(ℤ≥‘(0 + 𝑁)) = (ℤ≥‘𝑁)) |
80 | 77, 79 | eleqtrd 2690 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀 + 𝑁) ∈ (ℤ≥‘𝑁)) |
81 | | eluzle 11576 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 + 𝑁) ∈ (ℤ≥‘𝑁) → 𝑁 ≤ (𝑀 + 𝑁)) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ≤ (𝑀 + 𝑁)) |
83 | 82 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → 𝑁 ≤ (𝑀 + 𝑁)) |
84 | 73, 42, 44, 83, 60 | lelttrd 10074 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → 𝑁 < 𝑘) |
85 | 73, 44 | ltnled 10063 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → (𝑁 < 𝑘 ↔ ¬ 𝑘 ≤ 𝑁)) |
86 | 84, 85 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → ¬ 𝑘 ≤ 𝑁) |
87 | | coeeu.7 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
88 | | plyco0 23752 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵:ℕ0⟶ℂ) →
((𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))) |
89 | 4, 15, 88 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))) |
90 | 87, 89 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 ((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
91 | 90 | r19.21bi 2916 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
92 | 91 | adantrr 749 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → ((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
93 | 92 | necon1bd 2800 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → (¬ 𝑘 ≤ 𝑁 → (𝐵‘𝑘) = 0)) |
94 | 86, 93 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → (𝐵‘𝑘) = 0) |
95 | 71, 94 | oveq12d 6567 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → ((𝐴‘𝑘) − (𝐵‘𝑘)) = (0 − 0)) |
96 | | 0m0e0 11007 |
. . . . . . . . . 10
⊢ (0
− 0) = 0 |
97 | 95, 96 | syl6eq 2660 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → ((𝐴‘𝑘) − (𝐵‘𝑘)) = 0) |
98 | 39, 97 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → ((𝐴 ∘𝑓 − 𝐵)‘𝑘) = 0) |
99 | 98 | expr 641 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑀 + 𝑁) < 𝑘 → ((𝐴 ∘𝑓 − 𝐵)‘𝑘) = 0)) |
100 | 31, 99 | sylbird 249 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (¬
𝑘 ≤ (𝑀 + 𝑁) → ((𝐴 ∘𝑓 − 𝐵)‘𝑘) = 0)) |
101 | 100 | necon1ad 2799 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘𝑓
− 𝐵)‘𝑘) ≠ 0 → 𝑘 ≤ (𝑀 + 𝑁))) |
102 | 101 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (((𝐴 ∘𝑓
− 𝐵)‘𝑘) ≠ 0 → 𝑘 ≤ (𝑀 + 𝑁))) |
103 | | plyco0 23752 |
. . . . 5
⊢ (((𝑀 + 𝑁) ∈ ℕ0 ∧ (𝐴 ∘𝑓
− 𝐵):ℕ0⟶ℂ) →
(((𝐴
∘𝑓 − 𝐵) “
(ℤ≥‘((𝑀 + 𝑁) + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
(((𝐴
∘𝑓 − 𝐵)‘𝑘) ≠ 0 → 𝑘 ≤ (𝑀 + 𝑁)))) |
104 | 5, 18, 103 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (((𝐴 ∘𝑓 − 𝐵) “
(ℤ≥‘((𝑀 + 𝑁) + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
(((𝐴
∘𝑓 − 𝐵)‘𝑘) ≠ 0 → 𝑘 ≤ (𝑀 + 𝑁)))) |
105 | 102, 104 | mpbird 246 |
. . 3
⊢ (𝜑 → ((𝐴 ∘𝑓 − 𝐵) “
(ℤ≥‘((𝑀 + 𝑁) + 1))) = {0}) |
106 | | df-0p 23243 |
. . . . 5
⊢
0𝑝 = (ℂ × {0}) |
107 | | fconstmpt 5085 |
. . . . 5
⊢ (ℂ
× {0}) = (𝑧 ∈
ℂ ↦ 0) |
108 | 106, 107 | eqtri 2632 |
. . . 4
⊢
0𝑝 = (𝑧 ∈ ℂ ↦ 0) |
109 | | elfznn0 12302 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...(𝑀 + 𝑁)) → 𝑘 ∈ ℕ0) |
110 | 38 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴 ∘𝑓
− 𝐵)‘𝑘) = ((𝐴‘𝑘) − (𝐵‘𝑘))) |
111 | 110 | oveq1d 6564 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘𝑓
− 𝐵)‘𝑘) · (𝑧↑𝑘)) = (((𝐴‘𝑘) − (𝐵‘𝑘)) · (𝑧↑𝑘))) |
112 | 12 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝐴:ℕ0⟶ℂ) |
113 | 112 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ) |
114 | 15 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝐵:ℕ0⟶ℂ) |
115 | 114 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐵‘𝑘) ∈ ℂ) |
116 | | expcl 12740 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑧↑𝑘) ∈
ℂ) |
117 | 116 | adantll 746 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ) |
118 | 113, 115,
117 | subdird 10366 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((𝐴‘𝑘) − (𝐵‘𝑘)) · (𝑧↑𝑘)) = (((𝐴‘𝑘) · (𝑧↑𝑘)) − ((𝐵‘𝑘) · (𝑧↑𝑘)))) |
119 | 111, 118 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘𝑓
− 𝐵)‘𝑘) · (𝑧↑𝑘)) = (((𝐴‘𝑘) · (𝑧↑𝑘)) − ((𝐵‘𝑘) · (𝑧↑𝑘)))) |
120 | 109, 119 | sylan2 490 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑀 + 𝑁))) → (((𝐴 ∘𝑓 − 𝐵)‘𝑘) · (𝑧↑𝑘)) = (((𝐴‘𝑘) · (𝑧↑𝑘)) − ((𝐵‘𝑘) · (𝑧↑𝑘)))) |
121 | 120 | sumeq2dv 14281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑀 + 𝑁))(((𝐴 ∘𝑓 − 𝐵)‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...(𝑀 + 𝑁))(((𝐴‘𝑘) · (𝑧↑𝑘)) − ((𝐵‘𝑘) · (𝑧↑𝑘)))) |
122 | | fzfid 12634 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...(𝑀 + 𝑁)) ∈ Fin) |
123 | 113, 117 | mulcld 9939 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
124 | 109, 123 | sylan2 490 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑀 + 𝑁))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
125 | 115, 117 | mulcld 9939 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
126 | 109, 125 | sylan2 490 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑀 + 𝑁))) → ((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
127 | 122, 124,
126 | fsumsub 14362 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑀 + 𝑁))(((𝐴‘𝑘) · (𝑧↑𝑘)) − ((𝐵‘𝑘) · (𝑧↑𝑘))) = (Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐴‘𝑘) · (𝑧↑𝑘)) − Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐵‘𝑘) · (𝑧↑𝑘)))) |
128 | 122, 124 | fsumcl 14311 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
129 | | coeeu.8 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
130 | | coeeu.9 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) |
131 | 129, 130 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) |
132 | 131 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑧) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))‘𝑧)) |
133 | 132 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑧) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))‘𝑧)) |
134 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ) |
135 | | sumex 14266 |
. . . . . . . . . 10
⊢
Σ𝑘 ∈
(0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ V |
136 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))) |
137 | 136 | fvmpt2 6200 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℂ ∧
Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ V) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑧) = Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))) |
138 | 134, 135,
137 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑧) = Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))) |
139 | | fzss2 12252 |
. . . . . . . . . . . 12
⊢ ((𝑀 + 𝑁) ∈ (ℤ≥‘𝑀) → (0...𝑀) ⊆ (0...(𝑀 + 𝑁))) |
140 | 56, 139 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (0...𝑀) ⊆ (0...(𝑀 + 𝑁))) |
141 | 140 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑀) ⊆ (0...(𝑀 + 𝑁))) |
142 | 141 | sselda 3568 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ (0...(𝑀 + 𝑁))) |
143 | 142, 124 | syldan 486 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
144 | | eldifn 3695 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀)) → ¬ 𝑘 ∈ (0...𝑀)) |
145 | 144 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → ¬ 𝑘 ∈ (0...𝑀)) |
146 | | eldifi 3694 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀)) → 𝑘 ∈ (0...(𝑀 + 𝑁))) |
147 | 146, 109 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀)) → 𝑘 ∈ ℕ0) |
148 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
149 | 148, 48 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
(ℤ≥‘0)) |
150 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈
ℤ) |
151 | | elfz5 12205 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈
(ℤ≥‘0) ∧ 𝑀 ∈ ℤ) → (𝑘 ∈ (0...𝑀) ↔ 𝑘 ≤ 𝑀)) |
152 | 149, 150,
151 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (0...𝑀) ↔ 𝑘 ≤ 𝑀)) |
153 | 68, 152 | sylibrd 248 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ∈ (0...𝑀))) |
154 | 153 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ∈ (0...𝑀))) |
155 | 154 | necon1bd 2800 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (¬
𝑘 ∈ (0...𝑀) → (𝐴‘𝑘) = 0)) |
156 | 147, 155 | sylan2 490 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (¬ 𝑘 ∈ (0...𝑀) → (𝐴‘𝑘) = 0)) |
157 | 145, 156 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝐴‘𝑘) = 0) |
158 | 157 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘))) |
159 | 134, 147,
116 | syl2an 493 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝑧↑𝑘) ∈ ℂ) |
160 | 159 | mul02d 10113 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (0 · (𝑧↑𝑘)) = 0) |
161 | 158, 160 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) = 0) |
162 | 141, 143,
161, 122 | fsumss 14303 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐴‘𝑘) · (𝑧↑𝑘))) |
163 | 138, 162 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑧) = Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐴‘𝑘) · (𝑧↑𝑘))) |
164 | | sumex 14266 |
. . . . . . . . . 10
⊢
Σ𝑘 ∈
(0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ V |
165 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))) |
166 | 165 | fvmpt2 6200 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℂ ∧
Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ V) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))‘𝑧) = Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))) |
167 | 134, 164,
166 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))‘𝑧) = Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))) |
168 | | fzss2 12252 |
. . . . . . . . . . . 12
⊢ ((𝑀 + 𝑁) ∈ (ℤ≥‘𝑁) → (0...𝑁) ⊆ (0...(𝑀 + 𝑁))) |
169 | 80, 168 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (0...𝑁) ⊆ (0...(𝑀 + 𝑁))) |
170 | 169 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑁) ⊆ (0...(𝑀 + 𝑁))) |
171 | 170 | sselda 3568 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ (0...(𝑀 + 𝑁))) |
172 | 171, 126 | syldan 486 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
173 | | eldifn 3695 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁)) → ¬ 𝑘 ∈ (0...𝑁)) |
174 | 173 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁))) → ¬ 𝑘 ∈ (0...𝑁)) |
175 | | eldifi 3694 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁)) → 𝑘 ∈ (0...(𝑀 + 𝑁))) |
176 | 175, 109 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁)) → 𝑘 ∈ ℕ0) |
177 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑁 ∈
ℤ) |
178 | | elfz5 12205 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈
(ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (0...𝑁) ↔ 𝑘 ≤ 𝑁)) |
179 | 149, 177,
178 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (0...𝑁) ↔ 𝑘 ≤ 𝑁)) |
180 | 91, 179 | sylibrd 248 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐵‘𝑘) ≠ 0 → 𝑘 ∈ (0...𝑁))) |
181 | 180 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐵‘𝑘) ≠ 0 → 𝑘 ∈ (0...𝑁))) |
182 | 181 | necon1bd 2800 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (¬
𝑘 ∈ (0...𝑁) → (𝐵‘𝑘) = 0)) |
183 | 176, 182 | sylan2 490 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁))) → (¬ 𝑘 ∈ (0...𝑁) → (𝐵‘𝑘) = 0)) |
184 | 174, 183 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁))) → (𝐵‘𝑘) = 0) |
185 | 184 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁))) → ((𝐵‘𝑘) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘))) |
186 | 134, 176,
116 | syl2an 493 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁))) → (𝑧↑𝑘) ∈ ℂ) |
187 | 186 | mul02d 10113 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁))) → (0 · (𝑧↑𝑘)) = 0) |
188 | 185, 187 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁))) → ((𝐵‘𝑘) · (𝑧↑𝑘)) = 0) |
189 | 170, 172,
188, 122 | fsumss 14303 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐵‘𝑘) · (𝑧↑𝑘))) |
190 | 167, 189 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))‘𝑧) = Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐵‘𝑘) · (𝑧↑𝑘))) |
191 | 133, 163,
190 | 3eqtr3d 2652 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐴‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐵‘𝑘) · (𝑧↑𝑘))) |
192 | 128, 191 | subeq0bd 10335 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐴‘𝑘) · (𝑧↑𝑘)) − Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐵‘𝑘) · (𝑧↑𝑘))) = 0) |
193 | 121, 127,
192 | 3eqtrrd 2649 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 0 = Σ𝑘 ∈ (0...(𝑀 + 𝑁))(((𝐴 ∘𝑓 − 𝐵)‘𝑘) · (𝑧↑𝑘))) |
194 | 193 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ 0) = (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...(𝑀 + 𝑁))(((𝐴 ∘𝑓 − 𝐵)‘𝑘) · (𝑧↑𝑘)))) |
195 | 108, 194 | syl5eq 2656 |
. . 3
⊢ (𝜑 → 0𝑝 =
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...(𝑀 + 𝑁))(((𝐴 ∘𝑓 − 𝐵)‘𝑘) · (𝑧↑𝑘)))) |
196 | 2, 5, 27, 105, 195 | plyeq0 23771 |
. 2
⊢ (𝜑 → (𝐴 ∘𝑓 − 𝐵) = (ℕ0 ×
{0})) |
197 | | ofsubeq0 10894 |
. . 3
⊢
((ℕ0 ∈ V ∧ 𝐴:ℕ0⟶ℂ ∧
𝐵:ℕ0⟶ℂ) →
((𝐴
∘𝑓 − 𝐵) = (ℕ0 × {0}) ↔
𝐴 = 𝐵)) |
198 | 16, 12, 15, 197 | syl3anc 1318 |
. 2
⊢ (𝜑 → ((𝐴 ∘𝑓 − 𝐵) = (ℕ0 ×
{0}) ↔ 𝐴 = 𝐵)) |
199 | 196, 198 | mpbid 221 |
1
⊢ (𝜑 → 𝐴 = 𝐵) |