Metamath Proof Explorer


Theorem rng1nfld

Description: The zero ring is not a field. (Contributed by AV, 29-Apr-2019)

Ref Expression
Hypothesis rng1nfld.m M = Base ndx Z + ndx Z Z Z ndx Z Z Z
Assertion rng1nfld Z V M Field

Proof

Step Hyp Ref Expression
1 rng1nfld.m M = Base ndx Z + ndx Z Z Z ndx Z Z Z
2 1 rng1nnzr Z V M NzRing
3 df-nel M NzRing ¬ M NzRing
4 2 3 sylib Z V ¬ M NzRing
5 drngnzr M DivRing M NzRing
6 4 5 nsyl Z V ¬ M DivRing
7 isfld M Field M DivRing M CRing
8 simpl M DivRing M CRing M DivRing
9 8 a1i Z V M DivRing M CRing M DivRing
10 7 9 syl5bi Z V M Field M DivRing
11 6 10 mtod Z V ¬ M Field
12 df-nel M Field ¬ M Field
13 11 12 sylibr Z V M Field