Theorem ringelnzr

Description: A ring is nonzero if it has a nonzero element. (Contributed by Stefan O'Rear, 6-Feb-2015) (Revised by Mario Carneiro, 13-Jun-2015)

	Ref	Expression
Hypotheses	ringelnzr.z	|- .0. = ( 0g ` R )
	ringelnzr.b	|- B = ( Base ` R )
Assertion	ringelnzr	|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> R e. NzRing )

Proof

Step	Hyp	Ref	Expression
1		ringelnzr.z	|- .0. = ( 0g ` R )
2		ringelnzr.b	|- B = ( Base ` R )
3		simpl	|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> R e. Ring )
4		eldifsni	|- ( X e. ( B \ { .0. } ) -> X =/= .0. )
5	4	adantl	|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> X =/= .0. )
6		eldifi	|- ( X e. ( B \ { .0. } ) -> X e. B )
7	6	adantl	|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> X e. B )
8	2 1	ring0cl	|- ( R e. Ring -> .0. e. B )
9	8	adantr	|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> .0. e. B )
10		eqid	|- ( 1r ` R ) = ( 1r ` R )
11	2 10 1	ring1eq0	|- ( ( R e. Ring /\ X e. B /\ .0. e. B ) -> ( ( 1r ` R ) = .0. -> X = .0. ) )
12	3 7 9 11	syl3anc	|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> ( ( 1r ` R ) = .0. -> X = .0. ) )
13	12	necon3d	|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> ( X =/= .0. -> ( 1r ` R ) =/= .0. ) )
14	5 13	mpd	|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> ( 1r ` R ) =/= .0. )
15	10 1	isnzr	|- ( R e. NzRing <-> ( R e. Ring /\ ( 1r ` R ) =/= .0. ) )
16	3 14 15	sylanbrc	|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> R e. NzRing )