Metamath Proof Explorer


Theorem coeaddlem

Description: Lemma for coeadd and dgradd . (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses coefv0.1 𝐴 = ( coeff ‘ 𝐹 )
coeadd.2 𝐵 = ( coeff ‘ 𝐺 )
coeadd.3 𝑀 = ( deg ‘ 𝐹 )
coeadd.4 𝑁 = ( deg ‘ 𝐺 )
Assertion coeaddlem ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹f + 𝐺 ) ) = ( 𝐴f + 𝐵 ) ∧ ( deg ‘ ( 𝐹f + 𝐺 ) ) ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 coefv0.1 𝐴 = ( coeff ‘ 𝐹 )
2 coeadd.2 𝐵 = ( coeff ‘ 𝐺 )
3 coeadd.3 𝑀 = ( deg ‘ 𝐹 )
4 coeadd.4 𝑁 = ( deg ‘ 𝐺 )
5 plyaddcl ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐹f + 𝐺 ) ∈ ( Poly ‘ ℂ ) )
6 dgrcl ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐺 ) ∈ ℕ0 )
7 4 6 eqeltrid ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝑁 ∈ ℕ0 )
8 7 adantl ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑁 ∈ ℕ0 )
9 dgrcl ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
10 3 9 eqeltrid ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑀 ∈ ℕ0 )
11 10 adantr ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑀 ∈ ℕ0 )
12 8 11 ifcld ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ∈ ℕ0 )
13 addcl ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
14 13 adantl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
15 1 coef3 ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
16 15 adantr ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐴 : ℕ0 ⟶ ℂ )
17 2 coef3 ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐵 : ℕ0 ⟶ ℂ )
18 17 adantl ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐵 : ℕ0 ⟶ ℂ )
19 nn0ex 0 ∈ V
20 19 a1i ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ℕ0 ∈ V )
21 inidm ( ℕ0 ∩ ℕ0 ) = ℕ0
22 14 16 18 20 20 21 off ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐴f + 𝐵 ) : ℕ0 ⟶ ℂ )
23 oveq12 ( ( ( 𝐴𝑘 ) = 0 ∧ ( 𝐵𝑘 ) = 0 ) → ( ( 𝐴𝑘 ) + ( 𝐵𝑘 ) ) = ( 0 + 0 ) )
24 00id ( 0 + 0 ) = 0
25 23 24 eqtrdi ( ( ( 𝐴𝑘 ) = 0 ∧ ( 𝐵𝑘 ) = 0 ) → ( ( 𝐴𝑘 ) + ( 𝐵𝑘 ) ) = 0 )
26 16 ffnd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐴 Fn ℕ0 )
27 18 ffnd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐵 Fn ℕ0 )
28 eqidd ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) = ( 𝐴𝑘 ) )
29 eqidd ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵𝑘 ) = ( 𝐵𝑘 ) )
30 26 27 20 20 21 28 29 ofval ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) = ( ( 𝐴𝑘 ) + ( 𝐵𝑘 ) ) )
31 30 eqeq1d ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) = 0 ↔ ( ( 𝐴𝑘 ) + ( 𝐵𝑘 ) ) = 0 ) )
32 25 31 syl5ibr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴𝑘 ) = 0 ∧ ( 𝐵𝑘 ) = 0 ) → ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) = 0 ) )
33 32 necon3ad ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) ≠ 0 → ¬ ( ( 𝐴𝑘 ) = 0 ∧ ( 𝐵𝑘 ) = 0 ) ) )
34 neorian ( ( ( 𝐴𝑘 ) ≠ 0 ∨ ( 𝐵𝑘 ) ≠ 0 ) ↔ ¬ ( ( 𝐴𝑘 ) = 0 ∧ ( 𝐵𝑘 ) = 0 ) )
35 33 34 syl6ibr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) ≠ 0 → ( ( 𝐴𝑘 ) ≠ 0 ∨ ( 𝐵𝑘 ) ≠ 0 ) ) )
36 1 3 dgrub2 ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐴 “ ( ℤ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
37 36 adantr ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐴 “ ( ℤ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
38 plyco0 ( ( 𝑀 ∈ ℕ0𝐴 : ℕ0 ⟶ ℂ ) → ( ( 𝐴 “ ( ℤ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐴𝑘 ) ≠ 0 → 𝑘𝑀 ) ) )
39 11 16 38 syl2anc ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐴 “ ( ℤ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐴𝑘 ) ≠ 0 → 𝑘𝑀 ) ) )
40 37 39 mpbid ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ∀ 𝑘 ∈ ℕ0 ( ( 𝐴𝑘 ) ≠ 0 → 𝑘𝑀 ) )
41 40 r19.21bi ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴𝑘 ) ≠ 0 → 𝑘𝑀 ) )
42 11 adantr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 )
43 42 nn0red ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
44 8 adantr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
45 44 nn0red ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
46 max1 ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) )
47 43 45 46 syl2anc ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) )
48 nn0re ( 𝑘 ∈ ℕ0𝑘 ∈ ℝ )
49 48 adantl ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℝ )
50 12 adantr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ∈ ℕ0 )
51 50 nn0red ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ∈ ℝ )
52 letr ( ( 𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ∈ ℝ ) → ( ( 𝑘𝑀𝑀 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) → 𝑘 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
53 49 43 51 52 syl3anc ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑘𝑀𝑀 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) → 𝑘 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
54 47 53 mpan2d ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘𝑀𝑘 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
55 41 54 syld ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴𝑘 ) ≠ 0 → 𝑘 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
56 2 4 dgrub2 ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( 𝐵 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
57 56 adantl ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐵 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
58 plyco0 ( ( 𝑁 ∈ ℕ0𝐵 : ℕ0 ⟶ ℂ ) → ( ( 𝐵 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐵𝑘 ) ≠ 0 → 𝑘𝑁 ) ) )
59 8 18 58 syl2anc ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐵 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐵𝑘 ) ≠ 0 → 𝑘𝑁 ) ) )
60 57 59 mpbid ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ∀ 𝑘 ∈ ℕ0 ( ( 𝐵𝑘 ) ≠ 0 → 𝑘𝑁 ) )
61 60 r19.21bi ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐵𝑘 ) ≠ 0 → 𝑘𝑁 ) )
62 max2 ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑁 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) )
63 43 45 62 syl2anc ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) )
64 letr ( ( 𝑘 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ∈ ℝ ) → ( ( 𝑘𝑁𝑁 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) → 𝑘 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
65 49 45 51 64 syl3anc ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑘𝑁𝑁 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) → 𝑘 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
66 63 65 mpan2d ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘𝑁𝑘 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
67 61 66 syld ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐵𝑘 ) ≠ 0 → 𝑘 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
68 55 67 jaod ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴𝑘 ) ≠ 0 ∨ ( 𝐵𝑘 ) ≠ 0 ) → 𝑘 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
69 35 68 syld ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
70 69 ralrimiva ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ∀ 𝑘 ∈ ℕ0 ( ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
71 plyco0 ( ( if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ∈ ℕ0 ∧ ( 𝐴f + 𝐵 ) : ℕ0 ⟶ ℂ ) → ( ( ( 𝐴f + 𝐵 ) “ ( ℤ ‘ ( if ( 𝑀𝑁 , 𝑁 , 𝑀 ) + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ) )
72 12 22 71 syl2anc ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ( 𝐴f + 𝐵 ) “ ( ℤ ‘ ( if ( 𝑀𝑁 , 𝑁 , 𝑀 ) + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ) )
73 70 72 mpbird ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐴f + 𝐵 ) “ ( ℤ ‘ ( if ( 𝑀𝑁 , 𝑁 , 𝑀 ) + 1 ) ) ) = { 0 } )
74 simpl ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
75 simpr ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
76 1 3 coeid ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ) )
77 76 adantr ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ) )
78 2 4 coeid ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ) )
79 78 adantl ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ) )
80 74 75 11 8 16 18 37 57 77 79 plyaddlem1 ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐹f + 𝐺 ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) ) )
81 5 12 22 73 80 coeeq ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( 𝐹f + 𝐺 ) ) = ( 𝐴f + 𝐵 ) )
82 elfznn0 ( 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) → 𝑘 ∈ ℕ0 )
83 ffvelrn ( ( ( 𝐴f + 𝐵 ) : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) ∈ ℂ )
84 22 82 83 syl2an ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ) → ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) ∈ ℂ )
85 5 12 84 80 dgrle ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( 𝐹f + 𝐺 ) ) ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) )
86 81 85 jca ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹f + 𝐺 ) ) = ( 𝐴f + 𝐵 ) ∧ ( deg ‘ ( 𝐹f + 𝐺 ) ) ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )