This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrrid ⊢ ( 𝑘 ∈ ℕ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 ‘ 𝐹 ) ≤ 𝑁 )