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 ffvelcdm ⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐴 ‘ 0 ) ∈ ℂ )
21 18 19 20 sylancl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐴 ‘ 0 ) ∈ ℂ )
22 21 mulridd ⊢ ( 𝐹 ∈ ( 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 ffvelcdm ⊢ ( ( 𝐴 : ℕ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 ) )