Theorem mxidlnzrb

Description: A ring is nonzero if and only if it has maximal ideals. (Contributed by Thierry Arnoux, 10-Apr-2024)

	Ref	Expression
Assertion	mxidlnzrb	|- ( R e. Ring -> ( R e. NzRing <-> E. m m e. ( MaxIdeal ` R ) ) )

Proof

Step	Hyp	Ref	Expression
1		krull	|- ( R e. NzRing -> E. m m e. ( MaxIdeal ` R ) )
2	1	adantl	|- ( ( R e. Ring /\ R e. NzRing ) -> E. m m e. ( MaxIdeal ` R ) )
3		19.42v	|- ( E. m ( R e. Ring /\ m e. ( MaxIdeal ` R ) ) <-> ( R e. Ring /\ E. m m e. ( MaxIdeal ` R ) ) )
4		eqid	|- ( Base ` R ) = ( Base ` R )
5	4	mxidlnzr	|- ( ( R e. Ring /\ m e. ( MaxIdeal ` R ) ) -> R e. NzRing )
6	5	exlimiv	|- ( E. m ( R e. Ring /\ m e. ( MaxIdeal ` R ) ) -> R e. NzRing )
7	3 6	sylbir	|- ( ( R e. Ring /\ E. m m e. ( MaxIdeal ` R ) ) -> R e. NzRing )
8	2 7	impbida	|- ( R e. Ring -> ( R e. NzRing <-> E. m m e. ( MaxIdeal ` R ) ) )