Proof of Theorem plyaddlem1
Step | Hyp | Ref
| Expression |
1 | | cnex 10017 |
. . . 4
⊢ ℂ
∈ V |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → ℂ ∈
V) |
3 | | sumex 14418 |
. . . 4
⊢
Σ𝑘 ∈
(0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ V |
4 | 3 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ V) |
5 | | sumex 14418 |
. . . 4
⊢
Σ𝑘 ∈
(0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ V |
6 | 5 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ V) |
7 | | plyaddlem.f |
. . 3
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
8 | | plyaddlem.g |
. . 3
⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) |
9 | 2, 4, 6, 7, 8 | offval2 6914 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) = (𝑧 ∈ ℂ ↦ (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) + Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))) |
10 | | fzfid 12772 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∈ Fin) |
11 | | elfznn0 12433 |
. . . . . 6
⊢ (𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) → 𝑘 ∈ ℕ0) |
12 | | plyaddlem.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
13 | 12 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝐴:ℕ0⟶ℂ) |
14 | 13 | ffvelrnda 6359 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ) |
15 | | expcl 12878 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑧↑𝑘) ∈
ℂ) |
16 | 15 | adantll 750 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ) |
17 | 14, 16 | mulcld 10060 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
18 | 11, 17 | sylan2 491 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
19 | | plyaddlem.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵:ℕ0⟶ℂ) |
20 | 19 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝐵:ℕ0⟶ℂ) |
21 | 20 | ffvelrnda 6359 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐵‘𝑘) ∈ ℂ) |
22 | 21, 16 | mulcld 10060 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
23 | 11, 22 | sylan2 491 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) → ((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
24 | 10, 18, 23 | fsumadd 14470 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))(((𝐴‘𝑘) · (𝑧↑𝑘)) + ((𝐵‘𝑘) · (𝑧↑𝑘))) = (Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))((𝐴‘𝑘) · (𝑧↑𝑘)) + Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))((𝐵‘𝑘) · (𝑧↑𝑘)))) |
25 | | ffn 6045 |
. . . . . . . . . . 11
⊢ (𝐴:ℕ0⟶ℂ →
𝐴 Fn
ℕ0) |
26 | 12, 25 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 Fn ℕ0) |
27 | | ffn 6045 |
. . . . . . . . . . 11
⊢ (𝐵:ℕ0⟶ℂ →
𝐵 Fn
ℕ0) |
28 | 19, 27 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 Fn ℕ0) |
29 | | nn0ex 11298 |
. . . . . . . . . . 11
⊢
ℕ0 ∈ V |
30 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℕ0 ∈
V) |
31 | | inidm 3822 |
. . . . . . . . . 10
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 |
32 | | eqidd 2623 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) = (𝐴‘𝑘)) |
33 | | eqidd 2623 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐵‘𝑘) = (𝐵‘𝑘)) |
34 | 26, 28, 30, 30, 31, 32, 33 | ofval 6906 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴 ∘𝑓 +
𝐵)‘𝑘) = ((𝐴‘𝑘) + (𝐵‘𝑘))) |
35 | 34 | adantlr 751 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴 ∘𝑓 +
𝐵)‘𝑘) = ((𝐴‘𝑘) + (𝐵‘𝑘))) |
36 | 35 | oveq1d 6665 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘𝑓 +
𝐵)‘𝑘) · (𝑧↑𝑘)) = (((𝐴‘𝑘) + (𝐵‘𝑘)) · (𝑧↑𝑘))) |
37 | 14, 21, 16 | adddird 10065 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((𝐴‘𝑘) + (𝐵‘𝑘)) · (𝑧↑𝑘)) = (((𝐴‘𝑘) · (𝑧↑𝑘)) + ((𝐵‘𝑘) · (𝑧↑𝑘)))) |
38 | 36, 37 | eqtrd 2656 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘𝑓 +
𝐵)‘𝑘) · (𝑧↑𝑘)) = (((𝐴‘𝑘) · (𝑧↑𝑘)) + ((𝐵‘𝑘) · (𝑧↑𝑘)))) |
39 | 11, 38 | sylan2 491 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) → (((𝐴 ∘𝑓 + 𝐵)‘𝑘) · (𝑧↑𝑘)) = (((𝐴‘𝑘) · (𝑧↑𝑘)) + ((𝐵‘𝑘) · (𝑧↑𝑘)))) |
40 | 39 | sumeq2dv 14433 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))(((𝐴 ∘𝑓 + 𝐵)‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))(((𝐴‘𝑘) · (𝑧↑𝑘)) + ((𝐵‘𝑘) · (𝑧↑𝑘)))) |
41 | | plyaddlem.m |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
42 | 41 | nn0zd 11480 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
43 | | plyaddlem.n |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
44 | 43, 41 | ifcld 4131 |
. . . . . . . . . 10
⊢ (𝜑 → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈
ℕ0) |
45 | 44 | nn0zd 11480 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℤ) |
46 | 41 | nn0red 11352 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) |
47 | 43 | nn0red 11352 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℝ) |
48 | | max1 12016 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
49 | 46, 47, 48 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
50 | | eluz2 11693 |
. . . . . . . . 9
⊢ (if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℤ ∧ 𝑀 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
51 | 42, 45, 49, 50 | syl3anbrc 1246 |
. . . . . . . 8
⊢ (𝜑 → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ (ℤ≥‘𝑀)) |
52 | | fzss2 12381 |
. . . . . . . 8
⊢ (if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ (ℤ≥‘𝑀) → (0...𝑀) ⊆ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
53 | 51, 52 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (0...𝑀) ⊆ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
54 | 53 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑀) ⊆ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
55 | | elfznn0 12433 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℕ0) |
56 | 55, 17 | sylan2 491 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
57 | | eldifn 3733 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀)) → ¬ 𝑘 ∈ (0...𝑀)) |
58 | 57 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → ¬ 𝑘 ∈ (0...𝑀)) |
59 | | eldifi 3732 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀)) → 𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
60 | 59, 11 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀)) → 𝑘 ∈ ℕ0) |
61 | 60 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → 𝑘 ∈ ℕ0) |
62 | | nn0uz 11722 |
. . . . . . . . . . . . . . . . . 18
⊢
ℕ0 = (ℤ≥‘0) |
63 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℕ0) |
64 | 41, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑀 + 1) ∈
ℕ0) |
65 | 64, 62 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀 + 1) ∈
(ℤ≥‘0)) |
66 | | uzsplit 12412 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 + 1) ∈
(ℤ≥‘0) → (ℤ≥‘0) =
((0...((𝑀 + 1) − 1))
∪ (ℤ≥‘(𝑀 + 1)))) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(ℤ≥‘0) = ((0...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1)))) |
68 | 62, 67 | syl5eq 2668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ℕ0 =
((0...((𝑀 + 1) − 1))
∪ (ℤ≥‘(𝑀 + 1)))) |
69 | 41 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℂ) |
70 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℂ |
71 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑀 + 1)
− 1) = 𝑀) |
72 | 69, 70, 71 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀) |
73 | 72 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (0...((𝑀 + 1) − 1)) = (0...𝑀)) |
74 | 73 | uneq1d 3766 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((0...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1))) = ((0...𝑀) ∪ (ℤ≥‘(𝑀 + 1)))) |
75 | 68, 74 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ℕ0 =
((0...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) |
76 | 75 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → ℕ0 = ((0...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) |
77 | 61, 76 | eleqtrd 2703 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → 𝑘 ∈ ((0...𝑀) ∪ (ℤ≥‘(𝑀 + 1)))) |
78 | | elun 3753 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((0...𝑀) ∪ (ℤ≥‘(𝑀 + 1))) ↔ (𝑘 ∈ (0...𝑀) ∨ 𝑘 ∈ (ℤ≥‘(𝑀 + 1)))) |
79 | 77, 78 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (𝑘 ∈ (0...𝑀) ∨ 𝑘 ∈ (ℤ≥‘(𝑀 + 1)))) |
80 | 79 | ord 392 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (¬ 𝑘 ∈ (0...𝑀) → 𝑘 ∈ (ℤ≥‘(𝑀 + 1)))) |
81 | 58, 80 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → 𝑘 ∈ (ℤ≥‘(𝑀 + 1))) |
82 | | ffun 6048 |
. . . . . . . . . . . . . 14
⊢ (𝐴:ℕ0⟶ℂ →
Fun 𝐴) |
83 | 12, 82 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Fun 𝐴) |
84 | | ssun2 3777 |
. . . . . . . . . . . . . . 15
⊢
(ℤ≥‘(𝑀 + 1)) ⊆ ((0...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1))) |
85 | 84, 68 | syl5sseqr 3654 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) ⊆
ℕ0) |
86 | | fdm 6051 |
. . . . . . . . . . . . . . 15
⊢ (𝐴:ℕ0⟶ℂ →
dom 𝐴 =
ℕ0) |
87 | 12, 86 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝐴 = ℕ0) |
88 | 85, 87 | sseqtr4d 3642 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) ⊆ dom 𝐴) |
89 | | funfvima2 6493 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐴 ∧
(ℤ≥‘(𝑀 + 1)) ⊆ dom 𝐴) → (𝑘 ∈ (ℤ≥‘(𝑀 + 1)) → (𝐴‘𝑘) ∈ (𝐴 “
(ℤ≥‘(𝑀 + 1))))) |
90 | 83, 88, 89 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝑀 + 1)) → (𝐴‘𝑘) ∈ (𝐴 “
(ℤ≥‘(𝑀 + 1))))) |
91 | 90 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (𝑘 ∈ (ℤ≥‘(𝑀 + 1)) → (𝐴‘𝑘) ∈ (𝐴 “
(ℤ≥‘(𝑀 + 1))))) |
92 | 81, 91 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (𝐴‘𝑘) ∈ (𝐴 “
(ℤ≥‘(𝑀 + 1)))) |
93 | | plyaddlem.a2 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) |
94 | 93 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) |
95 | 92, 94 | eleqtrd 2703 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (𝐴‘𝑘) ∈ {0}) |
96 | | elsni 4194 |
. . . . . . . . 9
⊢ ((𝐴‘𝑘) ∈ {0} → (𝐴‘𝑘) = 0) |
97 | 95, 96 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (𝐴‘𝑘) = 0) |
98 | 97 | oveq1d 6665 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘))) |
99 | 60, 16 | sylan2 491 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (𝑧↑𝑘) ∈ ℂ) |
100 | 99 | mul02d 10234 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (0 · (𝑧↑𝑘)) = 0) |
101 | 98, 100 | eqtrd 2656 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) = 0) |
102 | 54, 56, 101, 10 | fsumss 14456 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))((𝐴‘𝑘) · (𝑧↑𝑘))) |
103 | 43 | nn0zd 11480 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℤ) |
104 | | max2 12018 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑁 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
105 | 46, 47, 104 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
106 | | eluz2 11693 |
. . . . . . . . 9
⊢ (if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ (ℤ≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℤ ∧ 𝑁 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
107 | 103, 45, 105, 106 | syl3anbrc 1246 |
. . . . . . . 8
⊢ (𝜑 → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ (ℤ≥‘𝑁)) |
108 | | fzss2 12381 |
. . . . . . . 8
⊢ (if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ (ℤ≥‘𝑁) → (0...𝑁) ⊆ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
109 | 107, 108 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (0...𝑁) ⊆ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
110 | 109 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑁) ⊆ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
111 | | elfznn0 12433 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
112 | 111, 22 | sylan2 491 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
113 | | eldifn 3733 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁)) → ¬ 𝑘 ∈ (0...𝑁)) |
114 | 113 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → ¬ 𝑘 ∈ (0...𝑁)) |
115 | | eldifi 3732 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁)) → 𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
116 | 115, 11 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁)) → 𝑘 ∈ ℕ0) |
117 | 116 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → 𝑘 ∈ ℕ0) |
118 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
119 | 43, 118 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
120 | 119, 62 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘0)) |
121 | | uzsplit 12412 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 + 1) ∈
(ℤ≥‘0) → (ℤ≥‘0) =
((0...((𝑁 + 1) − 1))
∪ (ℤ≥‘(𝑁 + 1)))) |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(ℤ≥‘0) = ((0...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1)))) |
123 | 62, 122 | syl5eq 2668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ℕ0 =
((0...((𝑁 + 1) − 1))
∪ (ℤ≥‘(𝑁 + 1)))) |
124 | 43 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℂ) |
125 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 1)
− 1) = 𝑁) |
126 | 124, 70, 125 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁) |
127 | 126 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁)) |
128 | 127 | uneq1d 3766 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1))) = ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))) |
129 | 123, 128 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ℕ0 =
((0...𝑁) ∪
(ℤ≥‘(𝑁 + 1)))) |
130 | 129 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → ℕ0 = ((0...𝑁) ∪
(ℤ≥‘(𝑁 + 1)))) |
131 | 117, 130 | eleqtrd 2703 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → 𝑘 ∈ ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))) |
132 | | elun 3753 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))) ↔ (𝑘 ∈ (0...𝑁) ∨ 𝑘 ∈ (ℤ≥‘(𝑁 + 1)))) |
133 | 131, 132 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (𝑘 ∈ (0...𝑁) ∨ 𝑘 ∈ (ℤ≥‘(𝑁 + 1)))) |
134 | 133 | ord 392 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (¬ 𝑘 ∈ (0...𝑁) → 𝑘 ∈ (ℤ≥‘(𝑁 + 1)))) |
135 | 114, 134 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) |
136 | | ffun 6048 |
. . . . . . . . . . . . . 14
⊢ (𝐵:ℕ0⟶ℂ →
Fun 𝐵) |
137 | 19, 136 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Fun 𝐵) |
138 | | ssun2 3777 |
. . . . . . . . . . . . . . 15
⊢
(ℤ≥‘(𝑁 + 1)) ⊆ ((0...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1))) |
139 | 138, 123 | syl5sseqr 3654 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(ℤ≥‘(𝑁 + 1)) ⊆
ℕ0) |
140 | | fdm 6051 |
. . . . . . . . . . . . . . 15
⊢ (𝐵:ℕ0⟶ℂ →
dom 𝐵 =
ℕ0) |
141 | 19, 140 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝐵 = ℕ0) |
142 | 139, 141 | sseqtr4d 3642 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(ℤ≥‘(𝑁 + 1)) ⊆ dom 𝐵) |
143 | | funfvima2 6493 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐵 ∧
(ℤ≥‘(𝑁 + 1)) ⊆ dom 𝐵) → (𝑘 ∈ (ℤ≥‘(𝑁 + 1)) → (𝐵‘𝑘) ∈ (𝐵 “
(ℤ≥‘(𝑁 + 1))))) |
144 | 137, 142,
143 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝑁 + 1)) → (𝐵‘𝑘) ∈ (𝐵 “
(ℤ≥‘(𝑁 + 1))))) |
145 | 144 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (𝑘 ∈ (ℤ≥‘(𝑁 + 1)) → (𝐵‘𝑘) ∈ (𝐵 “
(ℤ≥‘(𝑁 + 1))))) |
146 | 135, 145 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (𝐵‘𝑘) ∈ (𝐵 “
(ℤ≥‘(𝑁 + 1)))) |
147 | | plyaddlem.b2 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
148 | 147 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
149 | 146, 148 | eleqtrd 2703 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (𝐵‘𝑘) ∈ {0}) |
150 | | elsni 4194 |
. . . . . . . . 9
⊢ ((𝐵‘𝑘) ∈ {0} → (𝐵‘𝑘) = 0) |
151 | 149, 150 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (𝐵‘𝑘) = 0) |
152 | 151 | oveq1d 6665 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → ((𝐵‘𝑘) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘))) |
153 | 116, 16 | sylan2 491 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (𝑧↑𝑘) ∈ ℂ) |
154 | 153 | mul02d 10234 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (0 · (𝑧↑𝑘)) = 0) |
155 | 152, 154 | eqtrd 2656 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → ((𝐵‘𝑘) · (𝑧↑𝑘)) = 0) |
156 | 110, 112,
155, 10 | fsumss 14456 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))((𝐵‘𝑘) · (𝑧↑𝑘))) |
157 | 102, 156 | oveq12d 6668 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) + Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))) = (Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))((𝐴‘𝑘) · (𝑧↑𝑘)) + Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))((𝐵‘𝑘) · (𝑧↑𝑘)))) |
158 | 24, 40, 157 | 3eqtr4d 2666 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))(((𝐴 ∘𝑓 + 𝐵)‘𝑘) · (𝑧↑𝑘)) = (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) + Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) |
159 | 158 | mpteq2dva 4744 |
. 2
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))(((𝐴 ∘𝑓 + 𝐵)‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) + Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))) |
160 | 9, 159 | eqtr4d 2659 |
1
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))(((𝐴 ∘𝑓 + 𝐵)‘𝑘) · (𝑧↑𝑘)))) |