Metamath Proof Explorer

Theorem coeidlem

Description: Lemma for coeid . (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Hypotheses dgrub.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
dgrub.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
coeid.3 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
coeid.4 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
coeid.5 ⊢ ( 𝜑 → 𝐵 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
coeid.6 ⊢ ( 𝜑 → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
coeid.7 ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
Assertion coeidlem ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 dgrub.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
2 dgrub.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
3 coeid.3 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
4 coeid.4 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
5 coeid.5 ⊢ ( 𝜑 → 𝐵 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
6 coeid.6 ⊢ ( 𝜑 → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
7 coeid.7 ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
8 plybss ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ⊆ ℂ )
9 3 8 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
10 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
11 10 snssd ⊢ ( 𝜑 → { 0 } ⊆ ℂ )
12 9 11 unssd ⊢ ( 𝜑 → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
13 cnex ⊢ ℂ ∈ V
14 ssexg ⊢ ( ( ( 𝑆 ∪ { 0 } ) ⊆ ℂ ∧ ℂ ∈ V ) → ( 𝑆 ∪ { 0 } ) ∈ V )
15 12 13 14 sylancl ⊢ ( 𝜑 → ( 𝑆 ∪ { 0 } ) ∈ V )
16 nn0ex ⊢ ℕ0 ∈ V
17 elmapg ⊢ ( ( ( 𝑆 ∪ { 0 } ) ∈ V ∧ ℕ0 ∈ V ) → ( 𝐵 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝐵 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
18 15 16 17 sylancl ⊢ ( 𝜑 → ( 𝐵 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝐵 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
19 5 18 mpbid ⊢ ( 𝜑 → 𝐵 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
20 19 12 fssd ⊢ ( 𝜑 → 𝐵 : ℕ0 ⟶ ℂ )
21 3 4 20 6 7 coeeq ⊢ ( 𝜑 → ( coeff ‘ 𝐹 ) = 𝐵 )
22 1 21 eqtr2id ⊢ ( 𝜑 → 𝐵 = 𝐴 )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝐵 = 𝐴 )
24 fveq1 ⊢ ( 𝐵 = 𝐴 → ( 𝐵 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) )
25 24 oveq1d ⊢ ( 𝐵 = 𝐴 → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
26 25 sumeq2sdv ⊢ ( 𝐵 = 𝐴 → Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
27 23 26 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
28 3 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
29 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
30 2 29 eqeltrid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑁 ∈ ℕ0 )
31 28 30 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑁 ∈ ℕ0 )
32 31 nn0zd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑁 ∈ ℤ )
33 4 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑀 ∈ ℕ0 )
34 33 nn0zd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑀 ∈ ℤ )
35 23 imaeq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
36 6 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
37 35 36 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
38 1 2 dgrlb ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → 𝑁 ≤ 𝑀 )
39 28 33 37 38 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑁 ≤ 𝑀 )
40 eluz2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ≤ 𝑀 ) )
41 32 34 39 40 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
42 fzss2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... 𝑀 ) )
43 41 42 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... 𝑀 ) )
44 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
45 plyssc ⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
46 45 3 sselid ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℂ ) )
47 1 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ ℂ ) → 𝐴 : ℕ0 ⟶ ℂ )
48 46 47 syl ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝐴 : ℕ0 ⟶ ℂ )
50 49 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
51 expcl ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
52 51 adantll ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
53 50 52 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
54 44 53 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
55 eldifn ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) )
56 55 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) )
57 eldifi ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... 𝑀 ) )
58 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑀 ) → 𝑘 ∈ ℕ0 )
59 57 58 syl ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
60 1 2 dgrub ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑘 ≤ 𝑁 )
61 60 3expia ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
62 28 59 61 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
63 elfzuz ⊢ ( 𝑘 ∈ ( 0 ... 𝑀 ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
64 57 63 syl ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
65 elfz5 ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ≤ 𝑁 ) )
66 64 32 65 syl2anr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ≤ 𝑁 ) )
67 62 66 sylibrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ ( 0 ... 𝑁 ) ) )
68 67 necon1bd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( ¬ 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝐴 ‘ 𝑘 ) = 0 ) )
69 56 68 mpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐴 ‘ 𝑘 ) = 0 )
70 69 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( 0 · ( 𝑧 ↑ 𝑘 ) ) )
71 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑧 ∈ ℂ )
72 71 59 51 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
73 72 mul02d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( 0 · ( 𝑧 ↑ 𝑘 ) ) = 0 )
74 70 73 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = 0 )
75 fzfid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 0 ... 𝑀 ) ∈ Fin )
76 43 54 74 75 fsumss ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
77 27 76 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
78 77 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
79 7 78 eqtrd ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )