Proof of Theorem plyaddlem1
Step | Hyp | Ref
| Expression |
1 | | cnex 10810 |
. . . 4
⊢ ℂ
∈ V |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → ℂ ∈
V) |
3 | | sumex 15251 |
. . . 4
⊢
Σ𝑘 ∈
(0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ V |
4 | 3 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ V) |
5 | | sumex 15251 |
. . . 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 7488 |
. 2
⊢ (𝜑 → (𝐹 ∘f + 𝐺) = (𝑧 ∈ ℂ ↦ (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) + Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))) |
10 | | fzfid 13546 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∈ Fin) |
11 | | elfznn0 13205 |
. . . . . 6
⊢ (𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) → 𝑘 ∈ ℕ0) |
12 | | plyaddlem.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
13 | 12 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝐴:ℕ0⟶ℂ) |
14 | 13 | ffvelrnda 6904 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ) |
15 | | expcl 13653 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑧↑𝑘) ∈
ℂ) |
16 | 15 | adantll 714 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ) |
17 | 14, 16 | mulcld 10853 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
18 | 11, 17 | sylan2 596 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
19 | | plyaddlem.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵:ℕ0⟶ℂ) |
20 | 19 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝐵:ℕ0⟶ℂ) |
21 | 20 | ffvelrnda 6904 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐵‘𝑘) ∈ ℂ) |
22 | 21, 16 | mulcld 10853 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
23 | 11, 22 | sylan2 596 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) → ((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
24 | 10, 18, 23 | fsumadd 15304 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))(((𝐴‘𝑘) · (𝑧↑𝑘)) + ((𝐵‘𝑘) · (𝑧↑𝑘))) = (Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))((𝐴‘𝑘) · (𝑧↑𝑘)) + Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))((𝐵‘𝑘) · (𝑧↑𝑘)))) |
25 | 12 | ffnd 6546 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 Fn ℕ0) |
26 | 19 | ffnd 6546 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 Fn ℕ0) |
27 | | nn0ex 12096 |
. . . . . . . . . . 11
⊢
ℕ0 ∈ V |
28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℕ0 ∈
V) |
29 | | inidm 4133 |
. . . . . . . . . 10
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 |
30 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) = (𝐴‘𝑘)) |
31 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐵‘𝑘) = (𝐵‘𝑘)) |
32 | 25, 26, 28, 28, 29, 30, 31 | ofval 7479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴 ∘f + 𝐵)‘𝑘) = ((𝐴‘𝑘) + (𝐵‘𝑘))) |
33 | 32 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴 ∘f + 𝐵)‘𝑘) = ((𝐴‘𝑘) + (𝐵‘𝑘))) |
34 | 33 | oveq1d 7228 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘f + 𝐵)‘𝑘) · (𝑧↑𝑘)) = (((𝐴‘𝑘) + (𝐵‘𝑘)) · (𝑧↑𝑘))) |
35 | 14, 21, 16 | adddird 10858 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((𝐴‘𝑘) + (𝐵‘𝑘)) · (𝑧↑𝑘)) = (((𝐴‘𝑘) · (𝑧↑𝑘)) + ((𝐵‘𝑘) · (𝑧↑𝑘)))) |
36 | 34, 35 | eqtrd 2777 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘f + 𝐵)‘𝑘) · (𝑧↑𝑘)) = (((𝐴‘𝑘) · (𝑧↑𝑘)) + ((𝐵‘𝑘) · (𝑧↑𝑘)))) |
37 | 11, 36 | sylan2 596 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) → (((𝐴 ∘f + 𝐵)‘𝑘) · (𝑧↑𝑘)) = (((𝐴‘𝑘) · (𝑧↑𝑘)) + ((𝐵‘𝑘) · (𝑧↑𝑘)))) |
38 | 37 | sumeq2dv 15267 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))(((𝐴 ∘f + 𝐵)‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))(((𝐴‘𝑘) · (𝑧↑𝑘)) + ((𝐵‘𝑘) · (𝑧↑𝑘)))) |
39 | | plyaddlem.m |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
40 | 39 | nn0zd 12280 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
41 | | plyaddlem.n |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
42 | 41, 39 | ifcld 4485 |
. . . . . . . . . 10
⊢ (𝜑 → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈
ℕ0) |
43 | 42 | nn0zd 12280 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℤ) |
44 | 39 | nn0red 12151 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) |
45 | 41 | nn0red 12151 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℝ) |
46 | | max1 12775 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
47 | 44, 45, 46 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
48 | | eluz2 12444 |
. . . . . . . . 9
⊢ (if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℤ ∧ 𝑀 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
49 | 40, 43, 47, 48 | syl3anbrc 1345 |
. . . . . . . 8
⊢ (𝜑 → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ (ℤ≥‘𝑀)) |
50 | | fzss2 13152 |
. . . . . . . 8
⊢ (if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ (ℤ≥‘𝑀) → (0...𝑀) ⊆ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
51 | 49, 50 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (0...𝑀) ⊆ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
52 | 51 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑀) ⊆ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
53 | | elfznn0 13205 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℕ0) |
54 | 53, 17 | sylan2 596 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
55 | | eldifn 4042 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀)) → ¬ 𝑘 ∈ (0...𝑀)) |
56 | 55 | adantl 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → ¬ 𝑘 ∈ (0...𝑀)) |
57 | | eldifi 4041 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀)) → 𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
58 | 57, 11 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀)) → 𝑘 ∈ ℕ0) |
59 | 58 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → 𝑘 ∈ ℕ0) |
60 | | nn0uz 12476 |
. . . . . . . . . . . . . . . . . 18
⊢
ℕ0 = (ℤ≥‘0) |
61 | | peano2nn0 12130 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℕ0) |
62 | 39, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑀 + 1) ∈
ℕ0) |
63 | 62, 60 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀 + 1) ∈
(ℤ≥‘0)) |
64 | | uzsplit 13184 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 + 1) ∈
(ℤ≥‘0) → (ℤ≥‘0) =
((0...((𝑀 + 1) − 1))
∪ (ℤ≥‘(𝑀 + 1)))) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(ℤ≥‘0) = ((0...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1)))) |
66 | 60, 65 | syl5eq 2790 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ℕ0 =
((0...((𝑀 + 1) − 1))
∪ (ℤ≥‘(𝑀 + 1)))) |
67 | 39 | nn0cnd 12152 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℂ) |
68 | | ax-1cn 10787 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℂ |
69 | | pncan 11084 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑀 + 1)
− 1) = 𝑀) |
70 | 67, 68, 69 | sylancl 589 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀) |
71 | 70 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (0...((𝑀 + 1) − 1)) = (0...𝑀)) |
72 | 71 | uneq1d 4076 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((0...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1))) = ((0...𝑀) ∪ (ℤ≥‘(𝑀 + 1)))) |
73 | 66, 72 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ℕ0 =
((0...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) |
74 | 73 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → ℕ0 = ((0...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) |
75 | 59, 74 | eleqtrd 2840 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → 𝑘 ∈ ((0...𝑀) ∪ (ℤ≥‘(𝑀 + 1)))) |
76 | | elun 4063 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((0...𝑀) ∪ (ℤ≥‘(𝑀 + 1))) ↔ (𝑘 ∈ (0...𝑀) ∨ 𝑘 ∈ (ℤ≥‘(𝑀 + 1)))) |
77 | 75, 76 | sylib 221 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (𝑘 ∈ (0...𝑀) ∨ 𝑘 ∈ (ℤ≥‘(𝑀 + 1)))) |
78 | 77 | ord 864 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (¬ 𝑘 ∈ (0...𝑀) → 𝑘 ∈ (ℤ≥‘(𝑀 + 1)))) |
79 | 56, 78 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → 𝑘 ∈ (ℤ≥‘(𝑀 + 1))) |
80 | 12 | ffund 6549 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Fun 𝐴) |
81 | | ssun2 4087 |
. . . . . . . . . . . . . . 15
⊢
(ℤ≥‘(𝑀 + 1)) ⊆ ((0...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1))) |
82 | 81, 66 | sseqtrrid 3954 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) ⊆
ℕ0) |
83 | 12 | fdmd 6556 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝐴 = ℕ0) |
84 | 82, 83 | sseqtrrd 3942 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) ⊆ dom 𝐴) |
85 | | funfvima2 7047 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐴 ∧
(ℤ≥‘(𝑀 + 1)) ⊆ dom 𝐴) → (𝑘 ∈ (ℤ≥‘(𝑀 + 1)) → (𝐴‘𝑘) ∈ (𝐴 “
(ℤ≥‘(𝑀 + 1))))) |
86 | 80, 84, 85 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝑀 + 1)) → (𝐴‘𝑘) ∈ (𝐴 “
(ℤ≥‘(𝑀 + 1))))) |
87 | 86 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (𝑘 ∈ (ℤ≥‘(𝑀 + 1)) → (𝐴‘𝑘) ∈ (𝐴 “
(ℤ≥‘(𝑀 + 1))))) |
88 | 79, 87 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (𝐴‘𝑘) ∈ (𝐴 “
(ℤ≥‘(𝑀 + 1)))) |
89 | | plyaddlem.a2 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) |
90 | 89 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) |
91 | 88, 90 | eleqtrd 2840 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (𝐴‘𝑘) ∈ {0}) |
92 | | elsni 4558 |
. . . . . . . . 9
⊢ ((𝐴‘𝑘) ∈ {0} → (𝐴‘𝑘) = 0) |
93 | 91, 92 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (𝐴‘𝑘) = 0) |
94 | 93 | oveq1d 7228 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘))) |
95 | 58, 16 | sylan2 596 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (𝑧↑𝑘) ∈ ℂ) |
96 | 95 | mul02d 11030 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → (0 · (𝑧↑𝑘)) = 0) |
97 | 94, 96 | eqtrd 2777 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑀))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) = 0) |
98 | 52, 54, 97, 10 | fsumss 15289 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))((𝐴‘𝑘) · (𝑧↑𝑘))) |
99 | 41 | nn0zd 12280 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℤ) |
100 | | max2 12777 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑁 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
101 | 44, 45, 100 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
102 | | eluz2 12444 |
. . . . . . . . 9
⊢ (if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ (ℤ≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℤ ∧ 𝑁 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
103 | 99, 43, 101, 102 | syl3anbrc 1345 |
. . . . . . . 8
⊢ (𝜑 → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ (ℤ≥‘𝑁)) |
104 | | fzss2 13152 |
. . . . . . . 8
⊢ (if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ (ℤ≥‘𝑁) → (0...𝑁) ⊆ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
105 | 103, 104 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (0...𝑁) ⊆ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
106 | 105 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑁) ⊆ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
107 | | elfznn0 13205 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
108 | 107, 22 | sylan2 596 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
109 | | eldifn 4042 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁)) → ¬ 𝑘 ∈ (0...𝑁)) |
110 | 109 | adantl 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → ¬ 𝑘 ∈ (0...𝑁)) |
111 | | eldifi 4041 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁)) → 𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
112 | 111, 11 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁)) → 𝑘 ∈ ℕ0) |
113 | 112 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → 𝑘 ∈ ℕ0) |
114 | | peano2nn0 12130 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
115 | 41, 114 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
116 | 115, 60 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘0)) |
117 | | uzsplit 13184 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 + 1) ∈
(ℤ≥‘0) → (ℤ≥‘0) =
((0...((𝑁 + 1) − 1))
∪ (ℤ≥‘(𝑁 + 1)))) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(ℤ≥‘0) = ((0...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1)))) |
119 | 60, 118 | syl5eq 2790 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ℕ0 =
((0...((𝑁 + 1) − 1))
∪ (ℤ≥‘(𝑁 + 1)))) |
120 | 41 | nn0cnd 12152 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℂ) |
121 | | pncan 11084 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 1)
− 1) = 𝑁) |
122 | 120, 68, 121 | sylancl 589 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁) |
123 | 122 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁)) |
124 | 123 | uneq1d 4076 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1))) = ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))) |
125 | 119, 124 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ℕ0 =
((0...𝑁) ∪
(ℤ≥‘(𝑁 + 1)))) |
126 | 125 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → ℕ0 = ((0...𝑁) ∪
(ℤ≥‘(𝑁 + 1)))) |
127 | 113, 126 | eleqtrd 2840 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → 𝑘 ∈ ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))) |
128 | | elun 4063 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))) ↔ (𝑘 ∈ (0...𝑁) ∨ 𝑘 ∈ (ℤ≥‘(𝑁 + 1)))) |
129 | 127, 128 | sylib 221 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (𝑘 ∈ (0...𝑁) ∨ 𝑘 ∈ (ℤ≥‘(𝑁 + 1)))) |
130 | 129 | ord 864 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (¬ 𝑘 ∈ (0...𝑁) → 𝑘 ∈ (ℤ≥‘(𝑁 + 1)))) |
131 | 110, 130 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) |
132 | 19 | ffund 6549 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Fun 𝐵) |
133 | | ssun2 4087 |
. . . . . . . . . . . . . . 15
⊢
(ℤ≥‘(𝑁 + 1)) ⊆ ((0...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1))) |
134 | 133, 119 | sseqtrrid 3954 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(ℤ≥‘(𝑁 + 1)) ⊆
ℕ0) |
135 | 19 | fdmd 6556 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝐵 = ℕ0) |
136 | 134, 135 | sseqtrrd 3942 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(ℤ≥‘(𝑁 + 1)) ⊆ dom 𝐵) |
137 | | funfvima2 7047 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐵 ∧
(ℤ≥‘(𝑁 + 1)) ⊆ dom 𝐵) → (𝑘 ∈ (ℤ≥‘(𝑁 + 1)) → (𝐵‘𝑘) ∈ (𝐵 “
(ℤ≥‘(𝑁 + 1))))) |
138 | 132, 136,
137 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝑁 + 1)) → (𝐵‘𝑘) ∈ (𝐵 “
(ℤ≥‘(𝑁 + 1))))) |
139 | 138 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (𝑘 ∈ (ℤ≥‘(𝑁 + 1)) → (𝐵‘𝑘) ∈ (𝐵 “
(ℤ≥‘(𝑁 + 1))))) |
140 | 131, 139 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (𝐵‘𝑘) ∈ (𝐵 “
(ℤ≥‘(𝑁 + 1)))) |
141 | | plyaddlem.b2 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
142 | 141 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
143 | 140, 142 | eleqtrd 2840 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (𝐵‘𝑘) ∈ {0}) |
144 | | elsni 4558 |
. . . . . . . . 9
⊢ ((𝐵‘𝑘) ∈ {0} → (𝐵‘𝑘) = 0) |
145 | 143, 144 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (𝐵‘𝑘) = 0) |
146 | 145 | oveq1d 7228 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → ((𝐵‘𝑘) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘))) |
147 | 112, 16 | sylan2 596 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (𝑧↑𝑘) ∈ ℂ) |
148 | 147 | mul02d 11030 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → (0 · (𝑧↑𝑘)) = 0) |
149 | 146, 148 | eqtrd 2777 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) ∖ (0...𝑁))) → ((𝐵‘𝑘) · (𝑧↑𝑘)) = 0) |
150 | 106, 108,
149, 10 | fsumss 15289 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))((𝐵‘𝑘) · (𝑧↑𝑘))) |
151 | 98, 150 | oveq12d 7231 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) + Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))) = (Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))((𝐴‘𝑘) · (𝑧↑𝑘)) + Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))((𝐵‘𝑘) · (𝑧↑𝑘)))) |
152 | 24, 38, 151 | 3eqtr4d 2787 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))(((𝐴 ∘f + 𝐵)‘𝑘) · (𝑧↑𝑘)) = (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) + Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) |
153 | 152 | mpteq2dva 5150 |
. 2
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))(((𝐴 ∘f + 𝐵)‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) + Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))) |
154 | 9, 153 | eqtr4d 2780 |
1
⊢ (𝜑 → (𝐹 ∘f + 𝐺) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))(((𝐴 ∘f + 𝐵)‘𝑘) · (𝑧↑𝑘)))) |