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	ffvelrnd	⊢ ( ( 𝐹 ∈ ( 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 ) → 𝑀 ≤ 𝑁 )