Metamath Proof Explorer

Theorem drngnzr

Description: All division rings are nonzero. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Assertion drngnzr 
|- ( R e. DivRing -> R e. NzRing )

Proof

Step Hyp Ref Expression
1 drngring 
 |-  ( R e. DivRing -> R e. Ring )
2 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
3 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
4 2 3 drngunz 
 |-  ( R e. DivRing -> ( 1r ` R ) =/= ( 0g ` R ) )
5 3 2 isnzr 
 |-  ( R e. NzRing <-> ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) )
6 1 4 5 sylanbrc 
 |-  ( R e. DivRing -> R e. NzRing )