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