Metamath Proof Explorer

Theorem coe1termlem

Description: The coefficient function of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypothesis coe1term.1 ⊢ 𝐹 = ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧 ↑ 𝑁 ) ) )
Assertion coe1termlem ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( coeff ‘ 𝐹 ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ∧ ( 𝐴 ≠ 0 → ( deg ‘ 𝐹 ) = 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 coe1term.1 ⊢ 𝐹 = ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧 ↑ 𝑁 ) ) )
2 ssid ⊢ ℂ ⊆ ℂ
3 1 ply1term ⊢ ( ( ℂ ⊆ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
4 2 3 mp3an1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
5 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
6 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
7 0cn ⊢ 0 ∈ ℂ
8 ifcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ∈ ℂ )
9 6 7 8 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ∈ ℂ )
10 9 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ∈ ℂ )
11 10 fmpttd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) : ℕ0 ⟶ ℂ )
12 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) )
13 eqeq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 = 𝑁 ↔ 𝑘 = 𝑁 ) )
14 13 ifbid ⊢ ( 𝑛 = 𝑘 → if ( 𝑛 = 𝑁 , 𝐴 , 0 ) = if ( 𝑘 = 𝑁 , 𝐴 , 0 ) )
15 simpr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
16 ifcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ∈ ℂ )
17 6 7 16 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ∈ ℂ )
18 17 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ∈ ℂ )
19 12 14 15 18 fvmptd3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 = 𝑁 , 𝐴 , 0 ) )
20 19 neeq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) ≠ 0 ↔ if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ≠ 0 ) )
21 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
22 21 leidd ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ≤ 𝑁 )
23 22 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ≤ 𝑁 )
24 iffalse ⊢ ( ¬ 𝑘 = 𝑁 → if ( 𝑘 = 𝑁 , 𝐴 , 0 ) = 0 )
25 24 necon1ai ⊢ ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ≠ 0 → 𝑘 = 𝑁 )
26 25 breq1d ⊢ ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ≠ 0 → ( 𝑘 ≤ 𝑁 ↔ 𝑁 ≤ 𝑁 ) )
27 23 26 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
28 20 27 sylbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
29 28 ralrimiva ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ∀ 𝑘 ∈ ℕ0 ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
30 plyco0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) : ℕ0 ⟶ ℂ ) → ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) )
31 5 11 30 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) )
32 29 31 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
33 1 ply1termlem ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
34 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
35 19 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) )
36 34 35 sylan2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) )
37 36 sumeq2dv ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) )
38 37 mpteq2dv ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
39 33 38 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
40 4 5 11 32 39 coeeq ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( coeff ‘ 𝐹 ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) )
41 4 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ≠ 0 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
42 5 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ≠ 0 ) → 𝑁 ∈ ℕ0 )
43 11 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ≠ 0 ) → ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) : ℕ0 ⟶ ℂ )
44 32 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ≠ 0 ) → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
45 39 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ≠ 0 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
46 iftrue ⊢ ( 𝑛 = 𝑁 → if ( 𝑛 = 𝑁 , 𝐴 , 0 ) = 𝐴 )
47 46 12 fvmptg ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℂ ) → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑁 ) = 𝐴 )
48 47 ancoms ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑁 ) = 𝐴 )
49 48 neeq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑁 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )
50 49 biimpar ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ≠ 0 ) → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑁 ) ≠ 0 )
51 41 42 43 44 45 50 dgreq ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ≠ 0 ) → ( deg ‘ 𝐹 ) = 𝑁 )
52 51 ex ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ≠ 0 → ( deg ‘ 𝐹 ) = 𝑁 ) )
53 40 52 jca ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( coeff ‘ 𝐹 ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ∧ ( 𝐴 ≠ 0 → ( deg ‘ 𝐹 ) = 𝑁 ) ) )