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