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

Metamath Proof Explorer

Theorem dgrub

Description: If the M -th coefficient of F is nonzero, then the degree of F is at least M . (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Hypotheses dgrub.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
dgrub.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
Assertion dgrub ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) → 𝑀 ≤ 𝑁 )

Proof

Step Hyp Ref Expression
1 dgrub.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
2 dgrub.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
3 simp2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) → 𝑀 ∈ ℕ0 )
4 3 nn0red ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) → 𝑀 ∈ ℝ )
5 simp1 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
6 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
7 2 6 eqeltrid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑁 ∈ ℕ0 )
8 5 7 syl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) → 𝑁 ∈ ℕ0 )
9 8 nn0red ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) → 𝑁 ∈ ℝ )
10 1 dgrval ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) = sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )
11 2 10 eqtrid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑁 = sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )
12 5 11 syl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) → 𝑁 = sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )
13 1 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
14 5 13 syl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) → 𝐴 : ℕ0 ⟶ ℂ )
15 14 3 ffvelcdmd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) → ( 𝐴 ‘ 𝑀 ) ∈ ℂ )
16 simp3 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) → ( 𝐴 ‘ 𝑀 ) ≠ 0 )
17 eldifsn ⊢ ( ( 𝐴 ‘ 𝑀 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝐴 ‘ 𝑀 ) ∈ ℂ ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) )
18 15 16 17 sylanbrc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) → ( 𝐴 ‘ 𝑀 ) ∈ ( ℂ ∖ { 0 } ) )
19 1 coef ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
20 ffn ⊢ ( 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) → 𝐴 Fn ℕ0 )
21 elpreima ⊢ ( 𝐴 Fn ℕ0 → ( 𝑀 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ∈ ( ℂ ∖ { 0 } ) ) ) )
22 5 19 20 21 4syl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) → ( 𝑀 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ∈ ( ℂ ∖ { 0 } ) ) ) )
23 3 18 22 mpbir2and ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) → 𝑀 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) )
24 nn0ssre ⊢ ℕ0 ⊆ ℝ
25 ltso ⊢ < Or ℝ
26 soss ⊢ ( ℕ0 ⊆ ℝ → ( < Or ℝ → < Or ℕ0 ) )
27 24 25 26 mp2 ⊢ < Or ℕ0
28 27 a1i ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → < Or ℕ0 )
29 0zd ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 0 ∈ ℤ )
30 cnvimass ⊢ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ⊆ dom 𝐴
31 30 19 fssdm ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ⊆ ℕ0 )
32 1 dgrlem ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ∧ ∃ 𝑛 ∈ ℤ ∀ 𝑥 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥 ≤ 𝑛 ) )
33 32 simprd ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑛 ∈ ℤ ∀ 𝑥 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥 ≤ 𝑛 )
34 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
35 34 uzsupss ⊢ ( ( 0 ∈ ℤ ∧ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ⊆ ℕ0 ∧ ∃ 𝑛 ∈ ℤ ∀ 𝑥 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥 ≤ 𝑛 ) → ∃ 𝑛 ∈ ℕ0 ( ∀ 𝑥 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ¬ 𝑛 < 𝑥 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑥 < 𝑛 → ∃ 𝑦 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥 < 𝑦 ) ) )
36 29 31 33 35 syl3anc ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑛 ∈ ℕ0 ( ∀ 𝑥 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ¬ 𝑛 < 𝑥 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑥 < 𝑛 → ∃ 𝑦 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥 < 𝑦 ) ) )
37 28 36 supub ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝑀 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) → ¬ sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) < 𝑀 ) )
38 5 23 37 sylc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) → ¬ sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) < 𝑀 )
39 12 38 eqnbrtrd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) → ¬ 𝑁 < 𝑀 )
40 4 9 39 nltled ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) → 𝑀 ≤ 𝑁 )