Step | Hyp | Ref
| Expression |
1 | | plyaddcl 25392 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f + 𝐺) ∈
(Poly‘ℂ)) |
2 | | coeadd.4 |
. . . . . 6
⊢ 𝑁 = (deg‘𝐺) |
3 | | dgrcl 25405 |
. . . . . 6
⊢ (𝐺 ∈ (Poly‘𝑆) → (deg‘𝐺) ∈
ℕ0) |
4 | 2, 3 | eqeltrid 2845 |
. . . . 5
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝑁 ∈
ℕ0) |
5 | 4 | adantl 482 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝑁 ∈
ℕ0) |
6 | | coeadd.3 |
. . . . . 6
⊢ 𝑀 = (deg‘𝐹) |
7 | | dgrcl 25405 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
8 | 6, 7 | eqeltrid 2845 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑀 ∈
ℕ0) |
9 | 8 | adantr 481 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝑀 ∈
ℕ0) |
10 | 5, 9 | ifcld 4511 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈
ℕ0) |
11 | | addcl 10964 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ) |
12 | 11 | adantl 482 |
. . . 4
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ) |
13 | | coefv0.1 |
. . . . . 6
⊢ 𝐴 = (coeff‘𝐹) |
14 | 13 | coef3 25404 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ) |
15 | 14 | adantr 481 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐴:ℕ0⟶ℂ) |
16 | | coeadd.2 |
. . . . . 6
⊢ 𝐵 = (coeff‘𝐺) |
17 | 16 | coef3 25404 |
. . . . 5
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐵:ℕ0⟶ℂ) |
18 | 17 | adantl 482 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐵:ℕ0⟶ℂ) |
19 | | nn0ex 12250 |
. . . . 5
⊢
ℕ0 ∈ V |
20 | 19 | a1i 11 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ℕ0 ∈
V) |
21 | | inidm 4158 |
. . . 4
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 |
22 | 12, 15, 18, 20, 20, 21 | off 7546 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐴 ∘f + 𝐵):ℕ0⟶ℂ) |
23 | | oveq12 7281 |
. . . . . . . . . 10
⊢ (((𝐴‘𝑘) = 0 ∧ (𝐵‘𝑘) = 0) → ((𝐴‘𝑘) + (𝐵‘𝑘)) = (0 + 0)) |
24 | | 00id 11161 |
. . . . . . . . . 10
⊢ (0 + 0) =
0 |
25 | 23, 24 | eqtrdi 2796 |
. . . . . . . . 9
⊢ (((𝐴‘𝑘) = 0 ∧ (𝐵‘𝑘) = 0) → ((𝐴‘𝑘) + (𝐵‘𝑘)) = 0) |
26 | 15 | ffnd 6599 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐴 Fn ℕ0) |
27 | 18 | ffnd 6599 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐵 Fn ℕ0) |
28 | | eqidd 2741 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) = (𝐴‘𝑘)) |
29 | | eqidd 2741 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (𝐵‘𝑘) = (𝐵‘𝑘)) |
30 | 26, 27, 20, 20, 21, 28, 29 | ofval 7539 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → ((𝐴 ∘f + 𝐵)‘𝑘) = ((𝐴‘𝑘) + (𝐵‘𝑘))) |
31 | 30 | eqeq1d 2742 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘f + 𝐵)‘𝑘) = 0 ↔ ((𝐴‘𝑘) + (𝐵‘𝑘)) = 0)) |
32 | 25, 31 | syl5ibr 245 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (((𝐴‘𝑘) = 0 ∧ (𝐵‘𝑘) = 0) → ((𝐴 ∘f + 𝐵)‘𝑘) = 0)) |
33 | 32 | necon3ad 2958 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘f + 𝐵)‘𝑘) ≠ 0 → ¬ ((𝐴‘𝑘) = 0 ∧ (𝐵‘𝑘) = 0))) |
34 | | neorian 3041 |
. . . . . . 7
⊢ (((𝐴‘𝑘) ≠ 0 ∨ (𝐵‘𝑘) ≠ 0) ↔ ¬ ((𝐴‘𝑘) = 0 ∧ (𝐵‘𝑘) = 0)) |
35 | 33, 34 | syl6ibr 251 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘f + 𝐵)‘𝑘) ≠ 0 → ((𝐴‘𝑘) ≠ 0 ∨ (𝐵‘𝑘) ≠ 0))) |
36 | 13, 6 | dgrub2 25407 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) |
37 | 36 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) |
38 | | plyco0 25364 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝐴:ℕ0⟶ℂ) →
((𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀))) |
39 | 9, 15, 38 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀))) |
40 | 37, 39 | mpbid 231 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀)) |
41 | 40 | r19.21bi 3135 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀)) |
42 | 9 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈
ℕ0) |
43 | 42 | nn0red 12305 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈
ℝ) |
44 | 5 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → 𝑁 ∈
ℕ0) |
45 | 44 | nn0red 12305 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → 𝑁 ∈
ℝ) |
46 | | max1 12930 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
47 | 43, 45, 46 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → 𝑀 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
48 | | nn0re 12253 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
49 | 48 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℝ) |
50 | 10 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈
ℕ0) |
51 | 50 | nn0red 12305 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℝ) |
52 | | letr 11080 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℝ) → ((𝑘 ≤ 𝑀 ∧ 𝑀 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
53 | 49, 43, 51, 52 | syl3anc 1370 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → ((𝑘 ≤ 𝑀 ∧ 𝑀 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
54 | 47, 53 | mpan2d 691 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (𝑘 ≤ 𝑀 → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
55 | 41, 54 | syld 47 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
56 | 16, 2 | dgrub2 25407 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ (Poly‘𝑆) → (𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
57 | 56 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
58 | | plyco0 25364 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵:ℕ0⟶ℂ) →
((𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))) |
59 | 5, 18, 58 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))) |
60 | 57, 59 | mpbid 231 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ∀𝑘 ∈ ℕ0 ((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
61 | 60 | r19.21bi 3135 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → ((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
62 | | max2 12932 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑁 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
63 | 43, 45, 62 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → 𝑁 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
64 | | letr 11080 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℝ) → ((𝑘 ≤ 𝑁 ∧ 𝑁 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
65 | 49, 45, 51, 64 | syl3anc 1370 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → ((𝑘 ≤ 𝑁 ∧ 𝑁 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
66 | 63, 65 | mpan2d 691 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (𝑘 ≤ 𝑁 → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
67 | 61, 66 | syld 47 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → ((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
68 | 55, 67 | jaod 856 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (((𝐴‘𝑘) ≠ 0 ∨ (𝐵‘𝑘) ≠ 0) → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
69 | 35, 68 | syld 47 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘f + 𝐵)‘𝑘) ≠ 0 → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
70 | 69 | ralrimiva 3110 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ∀𝑘 ∈ ℕ0 (((𝐴 ∘f + 𝐵)‘𝑘) ≠ 0 → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
71 | | plyco0 25364 |
. . . . 5
⊢
((if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℕ0 ∧ (𝐴 ∘f + 𝐵):ℕ0⟶ℂ) →
(((𝐴 ∘f +
𝐵) “
(ℤ≥‘(if(𝑀 ≤ 𝑁, 𝑁, 𝑀) + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
(((𝐴 ∘f +
𝐵)‘𝑘) ≠ 0 → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)))) |
72 | 10, 22, 71 | syl2anc 584 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (((𝐴 ∘f + 𝐵) “
(ℤ≥‘(if(𝑀 ≤ 𝑁, 𝑁, 𝑀) + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
(((𝐴 ∘f +
𝐵)‘𝑘) ≠ 0 → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)))) |
73 | 70, 72 | mpbird 256 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((𝐴 ∘f + 𝐵) “
(ℤ≥‘(if(𝑀 ≤ 𝑁, 𝑁, 𝑀) + 1))) = {0}) |
74 | | simpl 483 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐹 ∈ (Poly‘𝑆)) |
75 | | simpr 485 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐺 ∈ (Poly‘𝑆)) |
76 | 13, 6 | coeid 25410 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
77 | 76 | adantr 481 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
78 | 16, 2 | coeid 25410 |
. . . . 5
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) |
79 | 78 | adantl 482 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) |
80 | 74, 75, 9, 5, 15, 18, 37, 57, 77, 79 | plyaddlem1 25385 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f + 𝐺) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))(((𝐴 ∘f + 𝐵)‘𝑘) · (𝑧↑𝑘)))) |
81 | 1, 10, 22, 73, 80 | coeeq 25399 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (coeff‘(𝐹 ∘f + 𝐺)) = (𝐴 ∘f + 𝐵)) |
82 | | elfznn0 13360 |
. . . 4
⊢ (𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) → 𝑘 ∈ ℕ0) |
83 | | ffvelrn 6956 |
. . . 4
⊢ (((𝐴 ∘f + 𝐵):ℕ0⟶ℂ ∧
𝑘 ∈
ℕ0) → ((𝐴 ∘f + 𝐵)‘𝑘) ∈ ℂ) |
84 | 22, 82, 83 | syl2an 596 |
. . 3
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) → ((𝐴 ∘f + 𝐵)‘𝑘) ∈ ℂ) |
85 | 1, 10, 84, 80 | dgrle 25415 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (deg‘(𝐹 ∘f + 𝐺)) ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
86 | 81, 85 | jca 512 |
1
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((coeff‘(𝐹 ∘f + 𝐺)) = (𝐴 ∘f + 𝐵) ∧ (deg‘(𝐹 ∘f + 𝐺)) ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |