Description: The zero ring is not a field. (Contributed by AV, 29-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | rng1nfld.m | |
|
Assertion | rng1nfld | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rng1nfld.m | |
|
2 | 1 | rng1nnzr | |
3 | df-nel | |
|
4 | 2 3 | sylib | |
5 | drngnzr | |
|
6 | 4 5 | nsyl | |
7 | isfld | |
|
8 | 7 | simplbi | |
9 | 6 8 | nsyl | |
10 | df-nel | |
|
11 | 9 10 | sylibr | |