Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Real subtraction
reelznn0nn
Next ⟩
nn0addcom
Metamath Proof Explorer
Ascii
Unicode
Theorem
reelznn0nn
Description:
elznn0nn
restated using
df-resub
.
(Contributed by
SN
, 25-Jan-2025)
Ref
Expression
Assertion
reelznn0nn
⊢
N
∈
ℤ
↔
N
∈
ℕ
0
∨
N
∈
ℝ
∧
0
-
ℝ
N
∈
ℕ
Proof
Step
Hyp
Ref
Expression
1
elznn0nn
⊢
N
∈
ℤ
↔
N
∈
ℕ
0
∨
N
∈
ℝ
∧
−
N
∈
ℕ
2
df-neg
⊢
−
N
=
0
−
N
3
0re
⊢
0
∈
ℝ
4
resubeqsub
⊢
0
∈
ℝ
∧
N
∈
ℝ
→
0
-
ℝ
N
=
0
−
N
5
3
4
mpan
⊢
N
∈
ℝ
→
0
-
ℝ
N
=
0
−
N
6
2
5
eqtr4id
⊢
N
∈
ℝ
→
−
N
=
0
-
ℝ
N
7
6
eleq1d
⊢
N
∈
ℝ
→
−
N
∈
ℕ
↔
0
-
ℝ
N
∈
ℕ
8
7
pm5.32i
⊢
N
∈
ℝ
∧
−
N
∈
ℕ
↔
N
∈
ℝ
∧
0
-
ℝ
N
∈
ℕ
9
8
orbi2i
⊢
N
∈
ℕ
0
∨
N
∈
ℝ
∧
−
N
∈
ℕ
↔
N
∈
ℕ
0
∨
N
∈
ℝ
∧
0
-
ℝ
N
∈
ℕ
10
1
9
bitri
⊢
N
∈
ℤ
↔
N
∈
ℕ
0
∨
N
∈
ℝ
∧
0
-
ℝ
N
∈
ℕ