Theorem deg1ge

Description: Conversely, a nonzero coefficient sets a lower bound on the degree. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Hypotheses	deg1leb.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1leb.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1leb.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	deg1leb.y	⊢ 0 = ( 0g ‘ 𝑅 )
	deg1leb.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
Assertion	deg1ge	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝐺 ) ≠ 0 ) → 𝐺 ≤ ( 𝐷 ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		deg1leb.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1leb.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1leb.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		deg1leb.y	⊢ 0 = ( 0g ‘ 𝑅 )
5		deg1leb.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
6	1 2 3	deg1xrcl	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
7		nn0re	⊢ ( 𝐺 ∈ ℕ0 → 𝐺 ∈ ℝ )
8	7	rexrd	⊢ ( 𝐺 ∈ ℕ0 → 𝐺 ∈ ℝ* )
9		xrltnle	⊢ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ 𝐺 ∈ ℝ* ) → ( ( 𝐷 ‘ 𝐹 ) < 𝐺 ↔ ¬ 𝐺 ≤ ( 𝐷 ‘ 𝐹 ) ) )
10	6 8 9	syl2an	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ) → ( ( 𝐷 ‘ 𝐹 ) < 𝐺 ↔ ¬ 𝐺 ≤ ( 𝐷 ‘ 𝐹 ) ) )
11	1 2 3 4 5	deg1lt	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ∧ ( 𝐷 ‘ 𝐹 ) < 𝐺 ) → ( 𝐴 ‘ 𝐺 ) = 0 )
12	11	3expia	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ) → ( ( 𝐷 ‘ 𝐹 ) < 𝐺 → ( 𝐴 ‘ 𝐺 ) = 0 ) )
13	10 12	sylbird	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ) → ( ¬ 𝐺 ≤ ( 𝐷 ‘ 𝐹 ) → ( 𝐴 ‘ 𝐺 ) = 0 ) )
14	13	necon1ad	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝐺 ) ≠ 0 → 𝐺 ≤ ( 𝐷 ‘ 𝐹 ) ) )
15	14	3impia	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝐺 ) ≠ 0 ) → 𝐺 ≤ ( 𝐷 ‘ 𝐹 ) )