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

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