Metamath Proof Explorer


Theorem dgrle

Description: Given an explicit expression for a polynomial, the degree is at most the highest term in the sum. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses dgrle.1 ( 𝜑𝐹 ∈ ( Poly ‘ 𝑆 ) )
dgrle.2 ( 𝜑𝑁 ∈ ℕ0 )
dgrle.3 ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
dgrle.4 ( 𝜑𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 · ( 𝑧𝑘 ) ) ) )
Assertion dgrle ( 𝜑 → ( deg ‘ 𝐹 ) ≤ 𝑁 )

Proof

Step Hyp Ref Expression
1 dgrle.1 ( 𝜑𝐹 ∈ ( Poly ‘ 𝑆 ) )
2 dgrle.2 ( 𝜑𝑁 ∈ ℕ0 )
3 dgrle.3 ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
4 dgrle.4 ( 𝜑𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 · ( 𝑧𝑘 ) ) ) )
5 1 2 3 4 coeeq2 ( 𝜑 → ( coeff ‘ 𝐹 ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) ) )
6 5 ad2antrr ( ( ( 𝜑𝑚 ∈ ℕ0 ) ∧ ¬ 𝑚𝑁 ) → ( coeff ‘ 𝐹 ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) ) )
7 6 fveq1d ( ( ( 𝜑𝑚 ∈ ℕ0 ) ∧ ¬ 𝑚𝑁 ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) )
8 nfcv 𝑘 𝑚
9 nfv 𝑘 ¬ 𝑚𝑁
10 nffvmpt1 𝑘 ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 )
11 10 nfeq1 𝑘 ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0
12 9 11 nfim 𝑘 ( ¬ 𝑚𝑁 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 )
13 breq1 ( 𝑘 = 𝑚 → ( 𝑘𝑁𝑚𝑁 ) )
14 13 notbid ( 𝑘 = 𝑚 → ( ¬ 𝑘𝑁 ↔ ¬ 𝑚𝑁 ) )
15 fveqeq2 ( 𝑘 = 𝑚 → ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = 0 ↔ ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 ) )
16 14 15 imbi12d ( 𝑘 = 𝑚 → ( ( ¬ 𝑘𝑁 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = 0 ) ↔ ( ¬ 𝑚𝑁 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 ) ) )
17 iffalse ( ¬ 𝑘𝑁 → if ( 𝑘𝑁 , 𝐴 , 0 ) = 0 )
18 17 fveq2d ( ¬ 𝑘𝑁 → ( I ‘ if ( 𝑘𝑁 , 𝐴 , 0 ) ) = ( I ‘ 0 ) )
19 0cn 0 ∈ ℂ
20 fvi ( 0 ∈ ℂ → ( I ‘ 0 ) = 0 )
21 19 20 ax-mp ( I ‘ 0 ) = 0
22 18 21 eqtrdi ( ¬ 𝑘𝑁 → ( I ‘ if ( 𝑘𝑁 , 𝐴 , 0 ) ) = 0 )
23 eqid ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) )
24 23 fvmpt2i ( 𝑘 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = ( I ‘ if ( 𝑘𝑁 , 𝐴 , 0 ) ) )
25 24 eqeq1d ( 𝑘 ∈ ℕ0 → ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = 0 ↔ ( I ‘ if ( 𝑘𝑁 , 𝐴 , 0 ) ) = 0 ) )
26 22 25 syl5ibr ( 𝑘 ∈ ℕ0 → ( ¬ 𝑘𝑁 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = 0 ) )
27 8 12 16 26 vtoclgaf ( 𝑚 ∈ ℕ0 → ( ¬ 𝑚𝑁 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 ) )
28 27 imp ( ( 𝑚 ∈ ℕ0 ∧ ¬ 𝑚𝑁 ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 )
29 28 adantll ( ( ( 𝜑𝑚 ∈ ℕ0 ) ∧ ¬ 𝑚𝑁 ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 )
30 7 29 eqtrd ( ( ( 𝜑𝑚 ∈ ℕ0 ) ∧ ¬ 𝑚𝑁 ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) = 0 )
31 30 ex ( ( 𝜑𝑚 ∈ ℕ0 ) → ( ¬ 𝑚𝑁 → ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) = 0 ) )
32 31 necon1ad ( ( 𝜑𝑚 ∈ ℕ0 ) → ( ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 → 𝑚𝑁 ) )
33 32 ralrimiva ( 𝜑 → ∀ 𝑚 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 → 𝑚𝑁 ) )
34 eqid ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 )
35 34 coef3 ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ )
36 1 35 syl ( 𝜑 → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ )
37 plyco0 ( ( 𝑁 ∈ ℕ0 ∧ ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ ) → ( ( ( coeff ‘ 𝐹 ) “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑚 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 → 𝑚𝑁 ) ) )
38 2 36 37 syl2anc ( 𝜑 → ( ( ( coeff ‘ 𝐹 ) “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑚 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 → 𝑚𝑁 ) ) )
39 33 38 mpbird ( 𝜑 → ( ( coeff ‘ 𝐹 ) “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
40 eqid ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 )
41 34 40 dgrlb ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑁 ∈ ℕ0 ∧ ( ( coeff ‘ 𝐹 ) “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ) → ( deg ‘ 𝐹 ) ≤ 𝑁 )
42 1 2 39 41 syl3anc ( 𝜑 → ( deg ‘ 𝐹 ) ≤ 𝑁 )