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

Metamath Proof Explorer

Theorem nzrunit

Description: A unit is nonzero in any nonzero ring. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses nzrunit.1 
|- U = ( Unit ` R )
nzrunit.2 
|- .0. = ( 0g ` R )
Assertion nzrunit 
|- ( ( R e. NzRing /\ A e. U ) -> A =/= .0. )

Proof

Step Hyp Ref Expression
1 nzrunit.1 
 |-  U = ( Unit ` R )
2 nzrunit.2 
 |-  .0. = ( 0g ` R )
3 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
4 3 2 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= .0. )
5 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
6 1 2 3 0unit 
 |-  ( R e. Ring -> ( .0. e. U <-> ( 1r ` R ) = .0. ) )
7 6 necon3bbid 
 |-  ( R e. Ring -> ( -. .0. e. U <-> ( 1r ` R ) =/= .0. ) )
8 5 7 syl 
 |-  ( R e. NzRing -> ( -. .0. e. U <-> ( 1r ` R ) =/= .0. ) )
9 4 8 mpbird 
 |-  ( R e. NzRing -> -. .0. e. U )
10 eleq1 
 |-  ( A = .0. -> ( A e. U <-> .0. e. U ) )
11 10 notbid 
 |-  ( A = .0. -> ( -. A e. U <-> -. .0. e. U ) )
12 9 11 syl5ibrcom 
 |-  ( R e. NzRing -> ( A = .0. -> -. A e. U ) )
13 12 necon2ad 
 |-  ( R e. NzRing -> ( A e. U -> A =/= .0. ) )
14 13 imp 
 |-  ( ( R e. NzRing /\ A e. U ) -> A =/= .0. )