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 Could not format assertion : No typesetting found for |- ( R e. Ring -> ( R e. NzRing <-> E. m m e. ( MaxIdeal ` R ) ) ) with typecode |-

Proof

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