Database
BASIC ALGEBRAIC STRUCTURES
Ideals
Nonzero rings and zero rings
rng1nfld
Next ⟩
Left regular elements. More kinds of rings
Metamath Proof Explorer
Ascii
Unicode
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