Metamath Proof Explorer


Theorem coefv0

Description: The result of evaluating a polynomial at zero is the constant term. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypothesis coefv0.1 𝐴 = ( coeff ‘ 𝐹 )
Assertion coefv0 ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 ‘ 0 ) = ( 𝐴 ‘ 0 ) )

Proof

Step Hyp Ref Expression
1 coefv0.1 𝐴 = ( coeff ‘ 𝐹 )
2 0cn 0 ∈ ℂ
3 eqid ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 )
4 1 3 coeid2 ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 0 ∈ ℂ ) → ( 𝐹 ‘ 0 ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝐴𝑘 ) · ( 0 ↑ 𝑘 ) ) )
5 2 4 mpan2 ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 ‘ 0 ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝐴𝑘 ) · ( 0 ↑ 𝑘 ) ) )
6 dgrcl ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
7 nn0uz 0 = ( ℤ ‘ 0 )
8 6 7 eleqtrdi ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ( ℤ ‘ 0 ) )
9 fzss2 ( ( deg ‘ 𝐹 ) ∈ ( ℤ ‘ 0 ) → ( 0 ... 0 ) ⊆ ( 0 ... ( deg ‘ 𝐹 ) ) )
10 8 9 syl ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 0 ... 0 ) ⊆ ( 0 ... ( deg ‘ 𝐹 ) ) )
11 elfz1eq ( 𝑘 ∈ ( 0 ... 0 ) → 𝑘 = 0 )
12 fveq2 ( 𝑘 = 0 → ( 𝐴𝑘 ) = ( 𝐴 ‘ 0 ) )
13 oveq2 ( 𝑘 = 0 → ( 0 ↑ 𝑘 ) = ( 0 ↑ 0 ) )
14 0exp0e1 ( 0 ↑ 0 ) = 1
15 13 14 eqtrdi ( 𝑘 = 0 → ( 0 ↑ 𝑘 ) = 1 )
16 12 15 oveq12d ( 𝑘 = 0 → ( ( 𝐴𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 0 ) · 1 ) )
17 11 16 syl ( 𝑘 ∈ ( 0 ... 0 ) → ( ( 𝐴𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 0 ) · 1 ) )
18 1 coef3 ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
19 0nn0 0 ∈ ℕ0
20 ffvelrn ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐴 ‘ 0 ) ∈ ℂ )
21 18 19 20 sylancl ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐴 ‘ 0 ) ∈ ℂ )
22 21 mulid1d ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( 𝐴 ‘ 0 ) · 1 ) = ( 𝐴 ‘ 0 ) )
23 17 22 sylan9eqr ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( 0 ... 0 ) ) → ( ( 𝐴𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( 𝐴 ‘ 0 ) )
24 21 adantr ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( 0 ... 0 ) ) → ( 𝐴 ‘ 0 ) ∈ ℂ )
25 23 24 eqeltrd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( 0 ... 0 ) ) → ( ( 𝐴𝑘 ) · ( 0 ↑ 𝑘 ) ) ∈ ℂ )
26 eldifn ( 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) → ¬ 𝑘 ∈ ( 0 ... 0 ) )
27 eldifi ( 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) → 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) )
28 elfznn0 ( 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) → 𝑘 ∈ ℕ0 )
29 27 28 syl ( 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) → 𝑘 ∈ ℕ0 )
30 elnn0 ( 𝑘 ∈ ℕ0 ↔ ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) )
31 29 30 sylib ( 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) → ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) )
32 31 ord ( 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) → ( ¬ 𝑘 ∈ ℕ → 𝑘 = 0 ) )
33 id ( 𝑘 = 0 → 𝑘 = 0 )
34 0z 0 ∈ ℤ
35 elfz3 ( 0 ∈ ℤ → 0 ∈ ( 0 ... 0 ) )
36 34 35 ax-mp 0 ∈ ( 0 ... 0 )
37 33 36 eqeltrdi ( 𝑘 = 0 → 𝑘 ∈ ( 0 ... 0 ) )
38 32 37 syl6 ( 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) → ( ¬ 𝑘 ∈ ℕ → 𝑘 ∈ ( 0 ... 0 ) ) )
39 26 38 mt3d ( 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) → 𝑘 ∈ ℕ )
40 39 adantl ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) ) → 𝑘 ∈ ℕ )
41 40 0expd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) ) → ( 0 ↑ 𝑘 ) = 0 )
42 41 oveq2d ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) ) → ( ( 𝐴𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( ( 𝐴𝑘 ) · 0 ) )
43 ffvelrn ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) ∈ ℂ )
44 18 29 43 syl2an ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) ) → ( 𝐴𝑘 ) ∈ ℂ )
45 44 mul01d ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) ) → ( ( 𝐴𝑘 ) · 0 ) = 0 )
46 42 45 eqtrd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) ) → ( ( 𝐴𝑘 ) · ( 0 ↑ 𝑘 ) ) = 0 )
47 fzfid ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 0 ... ( deg ‘ 𝐹 ) ) ∈ Fin )
48 10 25 46 47 fsumss ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 𝐴𝑘 ) · ( 0 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝐴𝑘 ) · ( 0 ↑ 𝑘 ) ) )
49 22 21 eqeltrd ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( 𝐴 ‘ 0 ) · 1 ) ∈ ℂ )
50 16 fsum1 ( ( 0 ∈ ℤ ∧ ( ( 𝐴 ‘ 0 ) · 1 ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 𝐴𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 0 ) · 1 ) )
51 34 49 50 sylancr ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 𝐴𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 0 ) · 1 ) )
52 51 22 eqtrd ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 𝐴𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( 𝐴 ‘ 0 ) )
53 5 48 52 3eqtr2d ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 ‘ 0 ) = ( 𝐴 ‘ 0 ) )