Database
BASIC ALGEBRAIC STRUCTURES
The complex numbers as an algebraic extensible structure
Ring of integers
zringsub
Next ⟩
zringmulg
Metamath Proof Explorer
Ascii
Unicode
Theorem
zringsub
Description:
The subtraction of elements in the ring of integers.
(Contributed by
AV
, 24-Mar-2025)
Ref
Expression
Hypothesis
zringsub.p
⊢
-
˙
=
-
ℤ
ring
Assertion
zringsub
⊢
X
∈
ℤ
∧
Y
∈
ℤ
→
X
-
˙
Y
=
X
−
Y
Proof
Step
Hyp
Ref
Expression
1
zringsub.p
⊢
-
˙
=
-
ℤ
ring
2
zcn
⊢
x
∈
ℤ
→
x
∈
ℂ
3
zaddcl
⊢
x
∈
ℤ
∧
y
∈
ℤ
→
x
+
y
∈
ℤ
4
znegcl
⊢
x
∈
ℤ
→
−
x
∈
ℤ
5
0z
⊢
0
∈
ℤ
6
2
3
4
5
cnsubglem
⊢
ℤ
∈
SubGrp
⁡
ℂ
fld
7
cnfldsub
⊢
−
=
-
ℂ
fld
8
df-zring
⊢
ℤ
ring
=
ℂ
fld
↾
𝑠
ℤ
9
7
8
1
subgsub
⊢
ℤ
∈
SubGrp
⁡
ℂ
fld
∧
X
∈
ℤ
∧
Y
∈
ℤ
→
X
−
Y
=
X
-
˙
Y
10
6
9
mp3an1
⊢
X
∈
ℤ
∧
Y
∈
ℤ
→
X
−
Y
=
X
-
˙
Y
11
10
eqcomd
⊢
X
∈
ℤ
∧
Y
∈
ℤ
→
X
-
˙
Y
=
X
−
Y