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

Metamath Proof Explorer

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 ) )