Step | Hyp | Ref
| Expression |
1 | | plyaddcl 23976 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘𝑓 + 𝐺) ∈
(Poly‘ℂ)) |
2 | | coeadd.4 |
. . . . . 6
⊢ 𝑁 = (deg‘𝐺) |
3 | | dgrcl 23989 |
. . . . . 6
⊢ (𝐺 ∈ (Poly‘𝑆) → (deg‘𝐺) ∈
ℕ0) |
4 | 2, 3 | syl5eqel 2705 |
. . . . 5
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝑁 ∈
ℕ0) |
5 | 4 | adantl 482 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝑁 ∈
ℕ0) |
6 | | coeadd.3 |
. . . . . 6
⊢ 𝑀 = (deg‘𝐹) |
7 | | dgrcl 23989 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
8 | 6, 7 | syl5eqel 2705 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑀 ∈
ℕ0) |
9 | 8 | adantr 481 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝑀 ∈
ℕ0) |
10 | 5, 9 | ifcld 4131 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈
ℕ0) |
11 | | addcl 10018 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ) |
12 | 11 | adantl 482 |
. . . 4
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ) |
13 | | coefv0.1 |
. . . . . 6
⊢ 𝐴 = (coeff‘𝐹) |
14 | 13 | coef3 23988 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ) |
15 | 14 | adantr 481 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐴:ℕ0⟶ℂ) |
16 | | coeadd.2 |
. . . . . 6
⊢ 𝐵 = (coeff‘𝐺) |
17 | 16 | coef3 23988 |
. . . . 5
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐵:ℕ0⟶ℂ) |
18 | 17 | adantl 482 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐵:ℕ0⟶ℂ) |
19 | | nn0ex 11298 |
. . . . 5
⊢
ℕ0 ∈ V |
20 | 19 | a1i 11 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ℕ0 ∈
V) |
21 | | inidm 3822 |
. . . 4
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 |
22 | 12, 15, 18, 20, 20, 21 | off 6912 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐴 ∘𝑓 + 𝐵):ℕ0⟶ℂ) |
23 | | oveq12 6659 |
. . . . . . . . . 10
⊢ (((𝐴‘𝑘) = 0 ∧ (𝐵‘𝑘) = 0) → ((𝐴‘𝑘) + (𝐵‘𝑘)) = (0 + 0)) |
24 | | 00id 10211 |
. . . . . . . . . 10
⊢ (0 + 0) =
0 |
25 | 23, 24 | syl6eq 2672 |
. . . . . . . . 9
⊢ (((𝐴‘𝑘) = 0 ∧ (𝐵‘𝑘) = 0) → ((𝐴‘𝑘) + (𝐵‘𝑘)) = 0) |
26 | | ffn 6045 |
. . . . . . . . . . . 12
⊢ (𝐴:ℕ0⟶ℂ →
𝐴 Fn
ℕ0) |
27 | 15, 26 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐴 Fn ℕ0) |
28 | | ffn 6045 |
. . . . . . . . . . . 12
⊢ (𝐵:ℕ0⟶ℂ →
𝐵 Fn
ℕ0) |
29 | 18, 28 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐵 Fn ℕ0) |
30 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) = (𝐴‘𝑘)) |
31 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (𝐵‘𝑘) = (𝐵‘𝑘)) |
32 | 27, 29, 20, 20, 21, 30, 31 | ofval 6906 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → ((𝐴 ∘𝑓 +
𝐵)‘𝑘) = ((𝐴‘𝑘) + (𝐵‘𝑘))) |
33 | 32 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘𝑓 +
𝐵)‘𝑘) = 0 ↔ ((𝐴‘𝑘) + (𝐵‘𝑘)) = 0)) |
34 | 25, 33 | syl5ibr 236 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (((𝐴‘𝑘) = 0 ∧ (𝐵‘𝑘) = 0) → ((𝐴 ∘𝑓 + 𝐵)‘𝑘) = 0)) |
35 | 34 | necon3ad 2807 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘𝑓 +
𝐵)‘𝑘) ≠ 0 → ¬ ((𝐴‘𝑘) = 0 ∧ (𝐵‘𝑘) = 0))) |
36 | | neorian 2888 |
. . . . . . 7
⊢ (((𝐴‘𝑘) ≠ 0 ∨ (𝐵‘𝑘) ≠ 0) ↔ ¬ ((𝐴‘𝑘) = 0 ∧ (𝐵‘𝑘) = 0)) |
37 | 35, 36 | syl6ibr 242 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘𝑓 +
𝐵)‘𝑘) ≠ 0 → ((𝐴‘𝑘) ≠ 0 ∨ (𝐵‘𝑘) ≠ 0))) |
38 | 13, 6 | dgrub2 23991 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) |
39 | 38 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) |
40 | | plyco0 23948 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝐴:ℕ0⟶ℂ) →
((𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀))) |
41 | 9, 15, 40 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀))) |
42 | 39, 41 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀)) |
43 | 42 | r19.21bi 2932 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑀)) |
44 | 9 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈
ℕ0) |
45 | 44 | nn0red 11352 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈
ℝ) |
46 | 5 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → 𝑁 ∈
ℕ0) |
47 | 46 | nn0red 11352 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → 𝑁 ∈
ℝ) |
48 | | max1 12016 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
49 | 45, 47, 48 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → 𝑀 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
50 | | nn0re 11301 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
51 | 50 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℝ) |
52 | 10 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈
ℕ0) |
53 | 52 | nn0red 11352 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℝ) |
54 | | letr 10131 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℝ) → ((𝑘 ≤ 𝑀 ∧ 𝑀 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
55 | 51, 45, 53, 54 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → ((𝑘 ≤ 𝑀 ∧ 𝑀 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
56 | 49, 55 | mpan2d 710 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (𝑘 ≤ 𝑀 → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
57 | 43, 56 | syld 47 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
58 | 16, 2 | dgrub2 23991 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ (Poly‘𝑆) → (𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
59 | 58 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
60 | | plyco0 23948 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵:ℕ0⟶ℂ) →
((𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))) |
61 | 5, 18, 60 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))) |
62 | 59, 61 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ∀𝑘 ∈ ℕ0 ((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
63 | 62 | r19.21bi 2932 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → ((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
64 | | max2 12018 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑁 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
65 | 45, 47, 64 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → 𝑁 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
66 | | letr 10131 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℝ) → ((𝑘 ≤ 𝑁 ∧ 𝑁 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
67 | 51, 47, 53, 66 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → ((𝑘 ≤ 𝑁 ∧ 𝑁 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
68 | 65, 67 | mpan2d 710 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (𝑘 ≤ 𝑁 → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
69 | 63, 68 | syld 47 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → ((𝐵‘𝑘) ≠ 0 → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
70 | 57, 69 | jaod 395 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (((𝐴‘𝑘) ≠ 0 ∨ (𝐵‘𝑘) ≠ 0) → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
71 | 37, 70 | syld 47 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ ℕ0) → (((𝐴 ∘𝑓 +
𝐵)‘𝑘) ≠ 0 → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
72 | 71 | ralrimiva 2966 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ∀𝑘 ∈ ℕ0 (((𝐴 ∘𝑓 +
𝐵)‘𝑘) ≠ 0 → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
73 | | plyco0 23948 |
. . . . 5
⊢
((if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ∈ ℕ0 ∧ (𝐴 ∘𝑓 +
𝐵):ℕ0⟶ℂ) →
(((𝐴
∘𝑓 + 𝐵) “
(ℤ≥‘(if(𝑀 ≤ 𝑁, 𝑁, 𝑀) + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
(((𝐴
∘𝑓 + 𝐵)‘𝑘) ≠ 0 → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)))) |
74 | 10, 22, 73 | syl2anc 693 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (((𝐴 ∘𝑓 + 𝐵) “
(ℤ≥‘(if(𝑀 ≤ 𝑁, 𝑁, 𝑀) + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
(((𝐴
∘𝑓 + 𝐵)‘𝑘) ≠ 0 → 𝑘 ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)))) |
75 | 72, 74 | mpbird 247 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((𝐴 ∘𝑓 + 𝐵) “
(ℤ≥‘(if(𝑀 ≤ 𝑁, 𝑁, 𝑀) + 1))) = {0}) |
76 | | simpl 473 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐹 ∈ (Poly‘𝑆)) |
77 | | simpr 477 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐺 ∈ (Poly‘𝑆)) |
78 | 13, 6 | coeid 23994 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
79 | 78 | adantr 481 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
80 | 16, 2 | coeid 23994 |
. . . . 5
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) |
81 | 80 | adantl 482 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) |
82 | 76, 77, 9, 5, 15, 18, 39, 59, 79, 81 | plyaddlem1 23969 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘𝑓 + 𝐺) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))(((𝐴 ∘𝑓 + 𝐵)‘𝑘) · (𝑧↑𝑘)))) |
83 | 1, 10, 22, 75, 82 | coeeq 23983 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (coeff‘(𝐹 ∘𝑓 + 𝐺)) = (𝐴 ∘𝑓 + 𝐵)) |
84 | | elfznn0 12433 |
. . . 4
⊢ (𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) → 𝑘 ∈ ℕ0) |
85 | | ffvelrn 6357 |
. . . 4
⊢ (((𝐴 ∘𝑓 +
𝐵):ℕ0⟶ℂ ∧
𝑘 ∈
ℕ0) → ((𝐴 ∘𝑓 + 𝐵)‘𝑘) ∈ ℂ) |
86 | 22, 84, 85 | syl2an 494 |
. . 3
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) ∧ 𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) → ((𝐴 ∘𝑓 + 𝐵)‘𝑘) ∈ ℂ) |
87 | 1, 10, 86, 82 | dgrle 23999 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (deg‘(𝐹 ∘𝑓 + 𝐺)) ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) |
88 | 83, 87 | jca 554 |
1
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((coeff‘(𝐹 ∘𝑓 + 𝐺)) = (𝐴 ∘𝑓 + 𝐵) ∧ (deg‘(𝐹 ∘𝑓 +
𝐺)) ≤ if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |