Theorem deg1lt0

Description: A polynomial is zero iff it has negative degree. (Contributed by Stefan O'Rear, 1-Apr-2015)

	Ref	Expression
Hypotheses	deg1z.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1z.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1z.z	⊢ 0 = ( 0g ‘ 𝑃 )
	deg1nn0cl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion	deg1lt0	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) < 0 ↔ 𝐹 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		deg1z.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1z.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1z.z	⊢ 0 = ( 0g ‘ 𝑃 )
4		deg1nn0cl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
5	1 2 3 4	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
6		nn0nlt0	⊢ ( ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 → ¬ ( 𝐷 ‘ 𝐹 ) < 0 )
7	5 6	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ¬ ( 𝐷 ‘ 𝐹 ) < 0 )
8	7	3expia	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( 𝐹 ≠ 0 → ¬ ( 𝐷 ‘ 𝐹 ) < 0 ) )
9	8	necon4ad	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) < 0 → 𝐹 = 0 ) )
10	1 2 3	deg1z	⊢ ( 𝑅 ∈ Ring → ( 𝐷 ‘ 0 ) = -∞ )
11		mnflt0	⊢ -∞ < 0
12	10 11	eqbrtrdi	⊢ ( 𝑅 ∈ Ring → ( 𝐷 ‘ 0 ) < 0 )
13	12	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( 𝐷 ‘ 0 ) < 0 )
14		fveq2	⊢ ( 𝐹 = 0 → ( 𝐷 ‘ 𝐹 ) = ( 𝐷 ‘ 0 ) )
15	14	breq1d	⊢ ( 𝐹 = 0 → ( ( 𝐷 ‘ 𝐹 ) < 0 ↔ ( 𝐷 ‘ 0 ) < 0 ) )
16	13 15	syl5ibrcom	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( 𝐹 = 0 → ( 𝐷 ‘ 𝐹 ) < 0 ) )
17	9 16	impbid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) < 0 ↔ 𝐹 = 0 ) )