Database
REAL AND COMPLEX NUMBERS
Integer sets
Integers (as a subset of complex numbers)
0zd
Next ⟩
elnn0z
Metamath Proof Explorer
Ascii
Structured
Theorem
0zd
Description:
Zero is an integer, deduction form.
(Contributed by
David A. Wheeler
, 8-Dec-2018)
Ref
Expression
Assertion
0zd
⊢
(
𝜑
→ 0 ∈ ℤ )
Proof
Step
Hyp
Ref
Expression
1
0z
⊢
0 ∈ ℤ
2
1
a1i
⊢
(
𝜑
→ 0 ∈ ℤ )