| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ssidd 4006 | . . 3
⊢ (𝜑 → ℂ ⊆
ℂ) | 
| 2 |  | coeeu.4 | . . . 4
⊢ (𝜑 → 𝑀 ∈
ℕ0) | 
| 3 |  | coeeu.5 | . . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 4 | 2, 3 | nn0addcld 12593 | . . 3
⊢ (𝜑 → (𝑀 + 𝑁) ∈
ℕ0) | 
| 5 |  | subcl 11508 | . . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 − 𝑦) ∈ ℂ) | 
| 6 | 5 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 − 𝑦) ∈ ℂ) | 
| 7 |  | coeeu.2 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (ℂ ↑m
ℕ0)) | 
| 8 |  | cnex 11237 | . . . . . . . 8
⊢ ℂ
∈ V | 
| 9 |  | nn0ex 12534 | . . . . . . . 8
⊢
ℕ0 ∈ V | 
| 10 | 8, 9 | elmap 8912 | . . . . . . 7
⊢ (𝐴 ∈ (ℂ
↑m ℕ0) ↔ 𝐴:ℕ0⟶ℂ) | 
| 11 | 7, 10 | sylib 218 | . . . . . 6
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) | 
| 12 |  | coeeu.3 | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (ℂ ↑m
ℕ0)) | 
| 13 | 8, 9 | elmap 8912 | . . . . . . 7
⊢ (𝐵 ∈ (ℂ
↑m ℕ0) ↔ 𝐵:ℕ0⟶ℂ) | 
| 14 | 12, 13 | sylib 218 | . . . . . 6
⊢ (𝜑 → 𝐵:ℕ0⟶ℂ) | 
| 15 | 9 | a1i 11 | . . . . . 6
⊢ (𝜑 → ℕ0 ∈
V) | 
| 16 |  | inidm 4226 | . . . . . 6
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 | 
| 17 | 6, 11, 14, 15, 15, 16 | off 7716 | . . . . 5
⊢ (𝜑 → (𝐴 ∘f − 𝐵):ℕ0⟶ℂ) | 
| 18 | 8, 9 | elmap 8912 | . . . . 5
⊢ ((𝐴 ∘f −
𝐵) ∈ (ℂ
↑m ℕ0) ↔ (𝐴 ∘f − 𝐵):ℕ0⟶ℂ) | 
| 19 | 17, 18 | sylibr 234 | . . . 4
⊢ (𝜑 → (𝐴 ∘f − 𝐵) ∈ (ℂ
↑m ℕ0)) | 
| 20 |  | 0cn 11254 | . . . . . . 7
⊢ 0 ∈
ℂ | 
| 21 |  | snssi 4807 | . . . . . . 7
⊢ (0 ∈
ℂ → {0} ⊆ ℂ) | 
| 22 | 20, 21 | ax-mp 5 | . . . . . 6
⊢ {0}
⊆ ℂ | 
| 23 |  | ssequn2 4188 | . . . . . 6
⊢ ({0}
⊆ ℂ ↔ (ℂ ∪ {0}) = ℂ) | 
| 24 | 22, 23 | mpbi 230 | . . . . 5
⊢ (ℂ
∪ {0}) = ℂ | 
| 25 | 24 | oveq1i 7442 | . . . 4
⊢ ((ℂ
∪ {0}) ↑m ℕ0) = (ℂ
↑m ℕ0) | 
| 26 | 19, 25 | eleqtrrdi 2851 | . . 3
⊢ (𝜑 → (𝐴 ∘f − 𝐵) ∈ ((ℂ ∪ {0})
↑m ℕ0)) | 
| 27 | 4 | nn0red 12590 | . . . . . . . 8
⊢ (𝜑 → (𝑀 + 𝑁) ∈ ℝ) | 
| 28 |  | nn0re 12537 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) | 
| 29 |  | ltnle 11341 | . . . . . . . 8
⊢ (((𝑀 + 𝑁) ∈ ℝ ∧ 𝑘 ∈ ℝ) → ((𝑀 + 𝑁) < 𝑘 ↔ ¬ 𝑘 ≤ (𝑀 + 𝑁))) | 
| 30 | 27, 28, 29 | syl2an 596 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑀 + 𝑁) < 𝑘 ↔ ¬ 𝑘 ≤ (𝑀 + 𝑁))) | 
| 31 | 11 | ffnd 6736 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 Fn ℕ0) | 
| 32 | 14 | ffnd 6736 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 Fn ℕ0) | 
| 33 |  | eqidd 2737 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) = (𝐴‘𝑘)) | 
| 34 |  | eqidd 2737 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐵‘𝑘) = (𝐵‘𝑘)) | 
| 35 | 31, 32, 15, 15, 16, 33, 34 | ofval 7709 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴 ∘f −
𝐵)‘𝑘) = ((𝐴‘𝑘) − (𝐵‘𝑘))) | 
| 36 | 35 | adantrr 717 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → ((𝐴 ∘f − 𝐵)‘𝑘) = ((𝐴‘𝑘) − (𝐵‘𝑘))) | 
| 37 | 2 | nn0red 12590 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 38 | 37 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → 𝑀 ∈ ℝ) | 
| 39 | 27 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → (𝑀 + 𝑁) ∈ ℝ) | 
| 40 | 28 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℝ) | 
| 41 | 40 | adantrr 717 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → 𝑘 ∈ ℝ) | 
| 42 | 2 | nn0cnd 12591 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ ℂ) | 
| 43 | 3 | nn0cnd 12591 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 44 | 42, 43 | addcomd 11464 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀 + 𝑁) = (𝑁 + 𝑀)) | 
| 45 |  | nn0uz 12921 | . . . . . . . . . . . . . . . . . . . 20
⊢
ℕ0 = (ℤ≥‘0) | 
| 46 | 3, 45 | eleqtrdi 2850 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) | 
| 47 | 2 | nn0zd 12641 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 48 |  | eluzadd 12908 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈
(ℤ≥‘0) ∧ 𝑀 ∈ ℤ) → (𝑁 + 𝑀) ∈ (ℤ≥‘(0 +
𝑀))) | 
| 49 | 46, 47, 48 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑁 + 𝑀) ∈ (ℤ≥‘(0 +
𝑀))) | 
| 50 | 44, 49 | eqeltrd 2840 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 + 𝑁) ∈ (ℤ≥‘(0 +
𝑀))) | 
| 51 | 42 | addlidd 11463 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (0 + 𝑀) = 𝑀) | 
| 52 | 51 | fveq2d 6909 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(ℤ≥‘(0 + 𝑀)) = (ℤ≥‘𝑀)) | 
| 53 | 50, 52 | eleqtrd 2842 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀 + 𝑁) ∈ (ℤ≥‘𝑀)) | 
| 54 |  | eluzle 12892 | . . . . . . . . . . . . . . . 16
⊢ ((𝑀 + 𝑁) ∈ (ℤ≥‘𝑀) → 𝑀 ≤ (𝑀 + 𝑁)) | 
| 55 | 53, 54 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ≤ (𝑀 + 𝑁)) | 
| 56 | 55 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → 𝑀 ≤ (𝑀 + 𝑁)) | 
| 57 |  | simprr 772 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → (𝑀 + 𝑁) < 𝑘) | 
| 58 | 38, 39, 41, 56, 57 | lelttrd 11420 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → 𝑀 < 𝑘) | 
| 59 | 38, 41 | ltnled 11409 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → (𝑀 < 𝑘 ↔ ¬ 𝑘 ≤ 𝑀)) | 
| 60 | 58, 59 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → ¬ 𝑘 ≤ 𝑀) | 
| 61 |  | coeeu.6 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) | 
| 62 |  | plyco0 26232 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ0
∧ 𝐴:ℕ0⟶ℂ) →
((𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀))) | 
| 63 | 2, 11, 62 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀))) | 
| 64 | 61, 63 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀)) | 
| 65 | 64 | r19.21bi 3250 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀)) | 
| 66 | 65 | adantrr 717 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀)) | 
| 67 | 66 | necon1bd 2957 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → (¬ 𝑘 ≤ 𝑀 → (𝐴‘𝑘) = 0)) | 
| 68 | 60, 67 | mpd 15 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → (𝐴‘𝑘) = 0) | 
| 69 | 3 | nn0red 12590 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 70 | 69 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → 𝑁 ∈ ℝ) | 
| 71 | 2, 45 | eleqtrdi 2850 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) | 
| 72 | 3 | nn0zd 12641 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 73 |  | eluzadd 12908 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈
(ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ (ℤ≥‘(0 +
𝑁))) | 
| 74 | 71, 72, 73 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 + 𝑁) ∈ (ℤ≥‘(0 +
𝑁))) | 
| 75 | 43 | addlidd 11463 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (0 + 𝑁) = 𝑁) | 
| 76 | 75 | fveq2d 6909 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(ℤ≥‘(0 + 𝑁)) = (ℤ≥‘𝑁)) | 
| 77 | 74, 76 | eleqtrd 2842 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀 + 𝑁) ∈ (ℤ≥‘𝑁)) | 
| 78 |  | eluzle 12892 | . . . . . . . . . . . . . . . 16
⊢ ((𝑀 + 𝑁) ∈ (ℤ≥‘𝑁) → 𝑁 ≤ (𝑀 + 𝑁)) | 
| 79 | 77, 78 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ≤ (𝑀 + 𝑁)) | 
| 80 | 79 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → 𝑁 ≤ (𝑀 + 𝑁)) | 
| 81 | 70, 39, 41, 80, 57 | lelttrd 11420 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → 𝑁 < 𝑘) | 
| 82 | 70, 41 | ltnled 11409 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → (𝑁 < 𝑘 ↔ ¬ 𝑘 ≤ 𝑁)) | 
| 83 | 81, 82 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → ¬ 𝑘 ≤ 𝑁) | 
| 84 |  | coeeu.7 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0}) | 
| 85 |  | plyco0 26232 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵:ℕ0⟶ℂ) →
((𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))) | 
| 86 | 3, 14, 85 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))) | 
| 87 | 84, 86 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 ((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) | 
| 88 | 87 | r19.21bi 3250 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) | 
| 89 | 88 | adantrr 717 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → ((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) | 
| 90 | 89 | necon1bd 2957 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → (¬ 𝑘 ≤ 𝑁 → (𝐵‘𝑘) = 0)) | 
| 91 | 83, 90 | mpd 15 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → (𝐵‘𝑘) = 0) | 
| 92 | 68, 91 | oveq12d 7450 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → ((𝐴‘𝑘) − (𝐵‘𝑘)) = (0 − 0)) | 
| 93 |  | 0m0e0 12387 | . . . . . . . . . 10
⊢ (0
− 0) = 0 | 
| 94 | 92, 93 | eqtrdi 2792 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → ((𝐴‘𝑘) − (𝐵‘𝑘)) = 0) | 
| 95 | 36, 94 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ (𝑀 + 𝑁) < 𝑘)) → ((𝐴 ∘f − 𝐵)‘𝑘) = 0) | 
| 96 | 95 | expr 456 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑀 + 𝑁) < 𝑘 → ((𝐴 ∘f − 𝐵)‘𝑘) = 0)) | 
| 97 | 30, 96 | sylbird 260 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (¬
𝑘 ≤ (𝑀 + 𝑁) → ((𝐴 ∘f − 𝐵)‘𝑘) = 0)) | 
| 98 | 97 | necon1ad 2956 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘f −
𝐵)‘𝑘) ≠ 0 → 𝑘 ≤ (𝑀 + 𝑁))) | 
| 99 | 98 | ralrimiva 3145 | . . . 4
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (((𝐴 ∘f −
𝐵)‘𝑘) ≠ 0 → 𝑘 ≤ (𝑀 + 𝑁))) | 
| 100 |  | plyco0 26232 | . . . . 5
⊢ (((𝑀 + 𝑁) ∈ ℕ0 ∧ (𝐴 ∘f −
𝐵):ℕ0⟶ℂ) →
(((𝐴 ∘f
− 𝐵) “
(ℤ≥‘((𝑀 + 𝑁) + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
(((𝐴 ∘f
− 𝐵)‘𝑘) ≠ 0 → 𝑘 ≤ (𝑀 + 𝑁)))) | 
| 101 | 4, 17, 100 | syl2anc 584 | . . . 4
⊢ (𝜑 → (((𝐴 ∘f − 𝐵) “
(ℤ≥‘((𝑀 + 𝑁) + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
(((𝐴 ∘f
− 𝐵)‘𝑘) ≠ 0 → 𝑘 ≤ (𝑀 + 𝑁)))) | 
| 102 | 99, 101 | mpbird 257 | . . 3
⊢ (𝜑 → ((𝐴 ∘f − 𝐵) “
(ℤ≥‘((𝑀 + 𝑁) + 1))) = {0}) | 
| 103 |  | df-0p 25706 | . . . . 5
⊢
0𝑝 = (ℂ × {0}) | 
| 104 |  | fconstmpt 5746 | . . . . 5
⊢ (ℂ
× {0}) = (𝑧 ∈
ℂ ↦ 0) | 
| 105 | 103, 104 | eqtri 2764 | . . . 4
⊢
0𝑝 = (𝑧 ∈ ℂ ↦ 0) | 
| 106 |  | elfznn0 13661 | . . . . . . . 8
⊢ (𝑘 ∈ (0...(𝑀 + 𝑁)) → 𝑘 ∈ ℕ0) | 
| 107 | 35 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴 ∘f −
𝐵)‘𝑘) = ((𝐴‘𝑘) − (𝐵‘𝑘))) | 
| 108 | 107 | oveq1d 7447 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘f −
𝐵)‘𝑘) · (𝑧↑𝑘)) = (((𝐴‘𝑘) − (𝐵‘𝑘)) · (𝑧↑𝑘))) | 
| 109 | 11 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝐴:ℕ0⟶ℂ) | 
| 110 | 109 | ffvelcdmda 7103 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ) | 
| 111 | 14 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝐵:ℕ0⟶ℂ) | 
| 112 | 111 | ffvelcdmda 7103 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐵‘𝑘) ∈ ℂ) | 
| 113 |  | expcl 14121 | . . . . . . . . . . 11
⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑧↑𝑘) ∈
ℂ) | 
| 114 | 113 | adantll 714 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ) | 
| 115 | 110, 112,
114 | subdird 11721 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((𝐴‘𝑘) − (𝐵‘𝑘)) · (𝑧↑𝑘)) = (((𝐴‘𝑘) · (𝑧↑𝑘)) − ((𝐵‘𝑘) · (𝑧↑𝑘)))) | 
| 116 | 108, 115 | eqtrd 2776 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘f −
𝐵)‘𝑘) · (𝑧↑𝑘)) = (((𝐴‘𝑘) · (𝑧↑𝑘)) − ((𝐵‘𝑘) · (𝑧↑𝑘)))) | 
| 117 | 106, 116 | sylan2 593 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑀 + 𝑁))) → (((𝐴 ∘f − 𝐵)‘𝑘) · (𝑧↑𝑘)) = (((𝐴‘𝑘) · (𝑧↑𝑘)) − ((𝐵‘𝑘) · (𝑧↑𝑘)))) | 
| 118 | 117 | sumeq2dv 15739 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑀 + 𝑁))(((𝐴 ∘f − 𝐵)‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...(𝑀 + 𝑁))(((𝐴‘𝑘) · (𝑧↑𝑘)) − ((𝐵‘𝑘) · (𝑧↑𝑘)))) | 
| 119 |  | fzfid 14015 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...(𝑀 + 𝑁)) ∈ Fin) | 
| 120 | 110, 114 | mulcld 11282 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) | 
| 121 | 106, 120 | sylan2 593 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑀 + 𝑁))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) | 
| 122 | 112, 114 | mulcld 11282 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) | 
| 123 | 106, 122 | sylan2 593 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑀 + 𝑁))) → ((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) | 
| 124 | 119, 121,
123 | fsumsub 15825 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑀 + 𝑁))(((𝐴‘𝑘) · (𝑧↑𝑘)) − ((𝐵‘𝑘) · (𝑧↑𝑘))) = (Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐴‘𝑘) · (𝑧↑𝑘)) − Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐵‘𝑘) · (𝑧↑𝑘)))) | 
| 125 | 119, 121 | fsumcl 15770 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) | 
| 126 |  | coeeu.8 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))) | 
| 127 |  | coeeu.9 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) | 
| 128 | 126, 127 | eqtr3d 2778 | . . . . . . . . . 10
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) | 
| 129 | 128 | fveq1d 6907 | . . . . . . . . 9
⊢ (𝜑 → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑧) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))‘𝑧)) | 
| 130 | 129 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑧) = ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))‘𝑧)) | 
| 131 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ) | 
| 132 |  | sumex 15725 | . . . . . . . . . 10
⊢
Σ𝑘 ∈
(0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ V | 
| 133 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))) | 
| 134 | 133 | fvmpt2 7026 | . . . . . . . . . 10
⊢ ((𝑧 ∈ ℂ ∧
Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ V) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑧) = Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))) | 
| 135 | 131, 132,
134 | sylancl 586 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑧) = Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))) | 
| 136 |  | fzss2 13605 | . . . . . . . . . . . 12
⊢ ((𝑀 + 𝑁) ∈ (ℤ≥‘𝑀) → (0...𝑀) ⊆ (0...(𝑀 + 𝑁))) | 
| 137 | 53, 136 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (0...𝑀) ⊆ (0...(𝑀 + 𝑁))) | 
| 138 | 137 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑀) ⊆ (0...(𝑀 + 𝑁))) | 
| 139 | 138 | sselda 3982 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ (0...(𝑀 + 𝑁))) | 
| 140 | 139, 121 | syldan 591 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) | 
| 141 |  | eldifn 4131 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀)) → ¬ 𝑘 ∈ (0...𝑀)) | 
| 142 | 141 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → ¬ 𝑘 ∈ (0...𝑀)) | 
| 143 |  | eldifi 4130 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀)) → 𝑘 ∈ (0...(𝑀 + 𝑁))) | 
| 144 | 143, 106 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀)) → 𝑘 ∈ ℕ0) | 
| 145 |  | simpr 484 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) | 
| 146 | 145, 45 | eleqtrdi 2850 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
(ℤ≥‘0)) | 
| 147 | 47 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈
ℤ) | 
| 148 |  | elfz5 13557 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈
(ℤ≥‘0) ∧ 𝑀 ∈ ℤ) → (𝑘 ∈ (0...𝑀) ↔ 𝑘 ≤ 𝑀)) | 
| 149 | 146, 147,
148 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (0...𝑀) ↔ 𝑘 ≤ 𝑀)) | 
| 150 | 65, 149 | sylibrd 259 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ∈ (0...𝑀))) | 
| 151 | 150 | adantlr 715 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ∈ (0...𝑀))) | 
| 152 | 151 | necon1bd 2957 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (¬
𝑘 ∈ (0...𝑀) → (𝐴‘𝑘) = 0)) | 
| 153 | 144, 152 | sylan2 593 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (¬ 𝑘 ∈ (0...𝑀) → (𝐴‘𝑘) = 0)) | 
| 154 | 142, 153 | mpd 15 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝐴‘𝑘) = 0) | 
| 155 | 154 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘))) | 
| 156 | 131, 144,
113 | syl2an 596 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝑧↑𝑘) ∈ ℂ) | 
| 157 | 156 | mul02d 11460 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (0 · (𝑧↑𝑘)) = 0) | 
| 158 | 155, 157 | eqtrd 2776 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) = 0) | 
| 159 | 138, 140,
158, 119 | fsumss 15762 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐴‘𝑘) · (𝑧↑𝑘))) | 
| 160 | 135, 159 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))‘𝑧) = Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐴‘𝑘) · (𝑧↑𝑘))) | 
| 161 |  | sumex 15725 | . . . . . . . . . 10
⊢
Σ𝑘 ∈
(0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ V | 
| 162 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))) | 
| 163 | 162 | fvmpt2 7026 | . . . . . . . . . 10
⊢ ((𝑧 ∈ ℂ ∧
Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ V) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))‘𝑧) = Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))) | 
| 164 | 131, 161,
163 | sylancl 586 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))‘𝑧) = Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))) | 
| 165 |  | fzss2 13605 | . . . . . . . . . . . 12
⊢ ((𝑀 + 𝑁) ∈ (ℤ≥‘𝑁) → (0...𝑁) ⊆ (0...(𝑀 + 𝑁))) | 
| 166 | 77, 165 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (0...𝑁) ⊆ (0...(𝑀 + 𝑁))) | 
| 167 | 166 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑁) ⊆ (0...(𝑀 + 𝑁))) | 
| 168 | 167 | sselda 3982 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ (0...(𝑀 + 𝑁))) | 
| 169 | 168, 123 | syldan 591 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) | 
| 170 |  | eldifn 4131 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁)) → ¬ 𝑘 ∈ (0...𝑁)) | 
| 171 | 170 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁))) → ¬ 𝑘 ∈ (0...𝑁)) | 
| 172 |  | eldifi 4130 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁)) → 𝑘 ∈ (0...(𝑀 + 𝑁))) | 
| 173 | 172, 106 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁)) → 𝑘 ∈ ℕ0) | 
| 174 | 72 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑁 ∈
ℤ) | 
| 175 |  | elfz5 13557 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈
(ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (0...𝑁) ↔ 𝑘 ≤ 𝑁)) | 
| 176 | 146, 174,
175 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (0...𝑁) ↔ 𝑘 ≤ 𝑁)) | 
| 177 | 88, 176 | sylibrd 259 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐵‘𝑘) ≠ 0 → 𝑘 ∈ (0...𝑁))) | 
| 178 | 177 | adantlr 715 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐵‘𝑘) ≠ 0 → 𝑘 ∈ (0...𝑁))) | 
| 179 | 178 | necon1bd 2957 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (¬
𝑘 ∈ (0...𝑁) → (𝐵‘𝑘) = 0)) | 
| 180 | 173, 179 | sylan2 593 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁))) → (¬ 𝑘 ∈ (0...𝑁) → (𝐵‘𝑘) = 0)) | 
| 181 | 171, 180 | mpd 15 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁))) → (𝐵‘𝑘) = 0) | 
| 182 | 181 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁))) → ((𝐵‘𝑘) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘))) | 
| 183 | 131, 173,
113 | syl2an 596 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁))) → (𝑧↑𝑘) ∈ ℂ) | 
| 184 | 183 | mul02d 11460 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁))) → (0 · (𝑧↑𝑘)) = 0) | 
| 185 | 182, 184 | eqtrd 2776 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑁))) → ((𝐵‘𝑘) · (𝑧↑𝑘)) = 0) | 
| 186 | 167, 169,
185, 119 | fsumss 15762 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐵‘𝑘) · (𝑧↑𝑘))) | 
| 187 | 164, 186 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))‘𝑧) = Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐵‘𝑘) · (𝑧↑𝑘))) | 
| 188 | 130, 160,
187 | 3eqtr3d 2784 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐴‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐵‘𝑘) · (𝑧↑𝑘))) | 
| 189 | 125, 188 | subeq0bd 11690 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐴‘𝑘) · (𝑧↑𝑘)) − Σ𝑘 ∈ (0...(𝑀 + 𝑁))((𝐵‘𝑘) · (𝑧↑𝑘))) = 0) | 
| 190 | 118, 124,
189 | 3eqtrrd 2781 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 0 = Σ𝑘 ∈ (0...(𝑀 + 𝑁))(((𝐴 ∘f − 𝐵)‘𝑘) · (𝑧↑𝑘))) | 
| 191 | 190 | mpteq2dva 5241 | . . . 4
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ 0) = (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...(𝑀 + 𝑁))(((𝐴 ∘f − 𝐵)‘𝑘) · (𝑧↑𝑘)))) | 
| 192 | 105, 191 | eqtrid 2788 | . . 3
⊢ (𝜑 → 0𝑝 =
(𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...(𝑀 + 𝑁))(((𝐴 ∘f − 𝐵)‘𝑘) · (𝑧↑𝑘)))) | 
| 193 | 1, 4, 26, 102, 192 | plyeq0 26251 | . 2
⊢ (𝜑 → (𝐴 ∘f − 𝐵) = (ℕ0 ×
{0})) | 
| 194 |  | ofsubeq0 12264 | . . 3
⊢
((ℕ0 ∈ V ∧ 𝐴:ℕ0⟶ℂ ∧
𝐵:ℕ0⟶ℂ) →
((𝐴 ∘f
− 𝐵) =
(ℕ0 × {0}) ↔ 𝐴 = 𝐵)) | 
| 195 | 9, 11, 14, 194 | mp3an2i 1467 | . 2
⊢ (𝜑 → ((𝐴 ∘f − 𝐵) = (ℕ0 ×
{0}) ↔ 𝐴 = 𝐵)) | 
| 196 | 193, 195 | mpbid 232 | 1
⊢ (𝜑 → 𝐴 = 𝐵) |