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

Metamath Proof Explorer

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