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 
|- D = ( deg1 ` R )
deg1z.p 
|- P = ( Poly1 ` R )
deg1z.z 
|- .0. = ( 0g ` P )
deg1nn0cl.b 
|- B = ( Base ` P )
Assertion deg1nn0clb 
|- ( ( R e. Ring /\ F e. B ) -> ( F =/= .0. <-> ( D ` F ) e. NN0 ) )

Proof

Step Hyp Ref Expression
1 deg1z.d 
 |-  D = ( deg1 ` R )
2 deg1z.p 
 |-  P = ( Poly1 ` R )
3 deg1z.z 
 |-  .0. = ( 0g ` P )
4 deg1nn0cl.b 
 |-  B = ( Base ` P )
5 1 2 3 4 deg1nn0cl 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 )
6 5 3expia 
 |-  ( ( R e. Ring /\ F e. B ) -> ( F =/= .0. -> ( D ` F ) e. NN0 ) )
7 mnfnre 
 |-  -oo e/ RR
8 7 neli 
 |-  -. -oo e. RR
9 nn0re 
 |-  ( -oo e. NN0 -> -oo e. RR )
10 8 9 mto 
 |-  -. -oo e. NN0
11 1 2 3 deg1z 
 |-  ( R e. Ring -> ( D ` .0. ) = -oo )
12 11 adantr 
 |-  ( ( R e. Ring /\ F e. B ) -> ( D ` .0. ) = -oo )
13 12 eleq1d 
 |-  ( ( R e. Ring /\ F e. B ) -> ( ( D ` .0. ) e. NN0 <-> -oo e. NN0 ) )
14 10 13 mtbiri 
 |-  ( ( R e. Ring /\ F e. B ) -> -. ( D ` .0. ) e. NN0 )
15 fveq2 
 |-  ( F = .0. -> ( D ` F ) = ( D ` .0. ) )
16 15 eleq1d 
 |-  ( F = .0. -> ( ( D ` F ) e. NN0 <-> ( D ` .0. ) e. NN0 ) )
17 16 notbid 
 |-  ( F = .0. -> ( -. ( D ` F ) e. NN0 <-> -. ( D ` .0. ) e. NN0 ) )
18 14 17 syl5ibrcom 
 |-  ( ( R e. Ring /\ F e. B ) -> ( F = .0. -> -. ( D ` F ) e. NN0 ) )
19 18 necon2ad 
 |-  ( ( R e. Ring /\ F e. B ) -> ( ( D ` F ) e. NN0 -> F =/= .0. ) )
20 6 19 impbid 
 |-  ( ( R e. Ring /\ F e. B ) -> ( F =/= .0. <-> ( D ` F ) e. NN0 ) )