Metamath Proof Explorer


Theorem deg1nn0clb

Description: A polynomial is nonzero iff it has definite degree. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses deg1z.d 𝐷 = ( deg1𝑅 )
deg1z.p 𝑃 = ( Poly1𝑅 )
deg1z.z 0 = ( 0g𝑃 )
deg1nn0cl.b 𝐵 = ( Base ‘ 𝑃 )
Assertion deg1nn0clb ( ( 𝑅 ∈ 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 5 3expia ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵 ) → ( 𝐹0 → ( 𝐷𝐹 ) ∈ ℕ0 ) )
7 mnfnre -∞ ∉ ℝ
8 7 neli ¬ -∞ ∈ ℝ
9 nn0re ( -∞ ∈ ℕ0 → -∞ ∈ ℝ )
10 8 9 mto ¬ -∞ ∈ ℕ0
11 1 2 3 deg1z ( 𝑅 ∈ Ring → ( 𝐷0 ) = -∞ )
12 11 adantr ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵 ) → ( 𝐷0 ) = -∞ )
13 12 eleq1d ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵 ) → ( ( 𝐷0 ) ∈ ℕ0 ↔ -∞ ∈ ℕ0 ) )
14 10 13 mtbiri ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵 ) → ¬ ( 𝐷0 ) ∈ ℕ0 )
15 fveq2 ( 𝐹 = 0 → ( 𝐷𝐹 ) = ( 𝐷0 ) )
16 15 eleq1d ( 𝐹 = 0 → ( ( 𝐷𝐹 ) ∈ ℕ0 ↔ ( 𝐷0 ) ∈ ℕ0 ) )
17 16 notbid ( 𝐹 = 0 → ( ¬ ( 𝐷𝐹 ) ∈ ℕ0 ↔ ¬ ( 𝐷0 ) ∈ ℕ0 ) )
18 14 17 syl5ibrcom ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵 ) → ( 𝐹 = 0 → ¬ ( 𝐷𝐹 ) ∈ ℕ0 ) )
19 18 necon2ad ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵 ) → ( ( 𝐷𝐹 ) ∈ ℕ0𝐹0 ) )
20 6 19 impbid ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵 ) → ( 𝐹0 ↔ ( 𝐷𝐹 ) ∈ ℕ0 ) )