Theorem unitnz

Description: In a nonzero ring, a unit cannot be zero. (Contributed by Thierry Arnoux, 25-Apr-2025)

	Ref	Expression
Hypotheses	unitnz.1	|- U = ( Unit ` R )
	unitnz.2	|- .0. = ( 0g ` R )
	unitnz.3	|- ( ph -> R e. NzRing )
	unitnz.4	|- ( ph -> X e. U )
Assertion	unitnz	|- ( ph -> X =/= .0. )

Proof

Step	Hyp	Ref	Expression
1		unitnz.1	|- U = ( Unit ` R )
2		unitnz.2	|- .0. = ( 0g ` R )
3		unitnz.3	|- ( ph -> R e. NzRing )
4		unitnz.4	|- ( ph -> X e. U )
5		nzrring	|- ( R e. NzRing -> R e. Ring )
6	3 5	syl	|- ( ph -> R e. Ring )
7		eqid	|- ( 1r ` R ) = ( 1r ` R )
8	7 2	nzrnz	|- ( R e. NzRing -> ( 1r ` R ) =/= .0. )
9	3 8	syl	|- ( ph -> ( 1r ` R ) =/= .0. )
10	1 2 7	0unit	|- ( R e. Ring -> ( .0. e. U <-> ( 1r ` R ) = .0. ) )
11	10	necon3bbid	|- ( R e. Ring -> ( -. .0. e. U <-> ( 1r ` R ) =/= .0. ) )
12	11	biimpar	|- ( ( R e. Ring /\ ( 1r ` R ) =/= .0. ) -> -. .0. e. U )
13	6 9 12	syl2anc	|- ( ph -> -. .0. e. U )
14		nelne2	|- ( ( X e. U /\ -. .0. e. U ) -> X =/= .0. )
15	4 13 14	syl2anc	|- ( ph -> X =/= .0. )