Database
REAL AND COMPLEX NUMBERS
Integer sets
Integers (as a subset of complex numbers)
zrevaddcl
Next ⟩
znnsub
Metamath Proof Explorer
Ascii
Unicode
Theorem
zrevaddcl
Description:
Reverse closure law for addition of integers.
(Contributed by
NM
, 11-May-2004)
Ref
Expression
Assertion
zrevaddcl
⊢
N
∈
ℤ
→
M
∈
ℂ
∧
M
+
N
∈
ℤ
↔
M
∈
ℤ
Proof
Step
Hyp
Ref
Expression
1
zcn
⊢
N
∈
ℤ
→
N
∈
ℂ
2
pncan
⊢
M
∈
ℂ
∧
N
∈
ℂ
→
M
+
N
-
N
=
M
3
1
2
sylan2
⊢
M
∈
ℂ
∧
N
∈
ℤ
→
M
+
N
-
N
=
M
4
3
ancoms
⊢
N
∈
ℤ
∧
M
∈
ℂ
→
M
+
N
-
N
=
M
5
4
adantr
⊢
N
∈
ℤ
∧
M
∈
ℂ
∧
M
+
N
∈
ℤ
→
M
+
N
-
N
=
M
6
zsubcl
⊢
M
+
N
∈
ℤ
∧
N
∈
ℤ
→
M
+
N
-
N
∈
ℤ
7
6
ancoms
⊢
N
∈
ℤ
∧
M
+
N
∈
ℤ
→
M
+
N
-
N
∈
ℤ
8
7
adantlr
⊢
N
∈
ℤ
∧
M
∈
ℂ
∧
M
+
N
∈
ℤ
→
M
+
N
-
N
∈
ℤ
9
5
8
eqeltrrd
⊢
N
∈
ℤ
∧
M
∈
ℂ
∧
M
+
N
∈
ℤ
→
M
∈
ℤ
10
9
ex
⊢
N
∈
ℤ
∧
M
∈
ℂ
→
M
+
N
∈
ℤ
→
M
∈
ℤ
11
zaddcl
⊢
M
∈
ℤ
∧
N
∈
ℤ
→
M
+
N
∈
ℤ
12
11
expcom
⊢
N
∈
ℤ
→
M
∈
ℤ
→
M
+
N
∈
ℤ
13
12
adantr
⊢
N
∈
ℤ
∧
M
∈
ℂ
→
M
∈
ℤ
→
M
+
N
∈
ℤ
14
10
13
impbid
⊢
N
∈
ℤ
∧
M
∈
ℂ
→
M
+
N
∈
ℤ
↔
M
∈
ℤ
15
14
pm5.32da
⊢
N
∈
ℤ
→
M
∈
ℂ
∧
M
+
N
∈
ℤ
↔
M
∈
ℂ
∧
M
∈
ℤ
16
zcn
⊢
M
∈
ℤ
→
M
∈
ℂ
17
16
pm4.71ri
⊢
M
∈
ℤ
↔
M
∈
ℂ
∧
M
∈
ℤ
18
15
17
bitr4di
⊢
N
∈
ℤ
→
M
∈
ℂ
∧
M
+
N
∈
ℤ
↔
M
∈
ℤ