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