Metamath Proof Explorer

Theorem dgrlb

Description: If all the coefficients above M are zero, then the degree of F is at most M . (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Hypotheses dgrub.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
dgrub.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
Assertion dgrlb ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → 𝑁 ≤ 𝑀 )

Proof

Step Hyp Ref Expression
1 dgrub.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
2 dgrub.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
3 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
4 2 3 eqeltrid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑁 ∈ ℕ0 )
5 4 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → 𝑁 ∈ ℕ0 )
6 5 nn0red ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → 𝑁 ∈ ℝ )
7 simp2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → 𝑀 ∈ ℕ0 )
8 7 nn0red ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → 𝑀 ∈ ℝ )
9 1 dgrlem ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ∧ ∃ 𝑛 ∈ ℤ ∀ 𝑥 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥 ≤ 𝑛 ) )
10 9 simpld ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
11 10 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
12 ffn ⊢ ( 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) → 𝐴 Fn ℕ0 )
13 elpreima ⊢ ( 𝐴 Fn ℕ0 → ( 𝑦 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑦 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) ) ) )
14 11 12 13 3syl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → ( 𝑦 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑦 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) ) ) )
15 14 biimpa ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) ∧ 𝑦 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ) → ( 𝑦 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) ) )
16 15 simpld ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) ∧ 𝑦 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ) → 𝑦 ∈ ℕ0 )
17 16 nn0red ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) ∧ 𝑦 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ) → 𝑦 ∈ ℝ )
18 8 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) ∧ 𝑦 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ) → 𝑀 ∈ ℝ )
19 eldifsni ⊢ ( ( 𝐴 ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) → ( 𝐴 ‘ 𝑦 ) ≠ 0 )
20 15 19 simpl2im ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) ∧ 𝑦 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ) → ( 𝐴 ‘ 𝑦 ) ≠ 0 )
21 simp3 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
22 1 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
23 22 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → 𝐴 : ℕ0 ⟶ ℂ )
24 plyco0 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ ℂ ) → ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ↔ ∀ 𝑦 ∈ ℕ0 ( ( 𝐴 ‘ 𝑦 ) ≠ 0 → 𝑦 ≤ 𝑀 ) ) )
25 7 23 24 syl2anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ↔ ∀ 𝑦 ∈ ℕ0 ( ( 𝐴 ‘ 𝑦 ) ≠ 0 → 𝑦 ≤ 𝑀 ) ) )
26 21 25 mpbid ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → ∀ 𝑦 ∈ ℕ0 ( ( 𝐴 ‘ 𝑦 ) ≠ 0 → 𝑦 ≤ 𝑀 ) )
27 26 r19.21bi ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑦 ) ≠ 0 → 𝑦 ≤ 𝑀 ) )
28 16 27 syldan ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) ∧ 𝑦 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ) → ( ( 𝐴 ‘ 𝑦 ) ≠ 0 → 𝑦 ≤ 𝑀 ) )
29 20 28 mpd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) ∧ 𝑦 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ) → 𝑦 ≤ 𝑀 )
30 17 18 29 lensymd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) ∧ 𝑦 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ) → ¬ 𝑀 < 𝑦 )
31 30 ralrimiva ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → ∀ 𝑦 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ¬ 𝑀 < 𝑦 )
32 nn0ssre ⊢ ℕ0 ⊆ ℝ
33 ltso ⊢ < Or ℝ
34 soss ⊢ ( ℕ0 ⊆ ℝ → ( < Or ℝ → < Or ℕ0 ) )
35 32 33 34 mp2 ⊢ < Or ℕ0
36 35 a1i ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → < Or ℕ0 )
37 0zd ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 0 ∈ ℤ )
38 cnvimass ⊢ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ⊆ dom 𝐴
39 38 10 fssdm ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ⊆ ℕ0 )
40 9 simprd ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑛 ∈ ℤ ∀ 𝑥 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥 ≤ 𝑛 )
41 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
42 41 uzsupss ⊢ ( ( 0 ∈ ℤ ∧ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ⊆ ℕ0 ∧ ∃ 𝑛 ∈ ℤ ∀ 𝑥 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥 ≤ 𝑛 ) → ∃ 𝑛 ∈ ℕ0 ( ∀ 𝑥 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ¬ 𝑛 < 𝑥 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑥 < 𝑛 → ∃ 𝑦 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥 < 𝑦 ) ) )
43 37 39 40 42 syl3anc ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑛 ∈ ℕ0 ( ∀ 𝑥 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ¬ 𝑛 < 𝑥 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑥 < 𝑛 → ∃ 𝑦 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥 < 𝑦 ) ) )
44 43 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → ∃ 𝑛 ∈ ℕ0 ( ∀ 𝑥 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ¬ 𝑛 < 𝑥 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑥 < 𝑛 → ∃ 𝑦 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) 𝑥 < 𝑦 ) ) )
45 36 44 supnub ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → ( ( 𝑀 ∈ ℕ0 ∧ ∀ 𝑦 ∈ ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) ¬ 𝑀 < 𝑦 ) → ¬ 𝑀 < sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) ) )
46 7 31 45 mp2and ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → ¬ 𝑀 < sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )
47 1 dgrval ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) = sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )
48 2 47 syl5eq ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑁 = sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )
49 48 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → 𝑁 = sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )
50 49 breq2d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → ( 𝑀 < 𝑁 ↔ 𝑀 < sup ( ( ◡ 𝐴 “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) ) )
51 46 50 mtbird ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → ¬ 𝑀 < 𝑁 )
52 6 8 51 nltled ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → 𝑁 ≤ 𝑀 )