Database
REAL AND COMPLEX NUMBERS
Integer sets
Integers (as a subset of complex numbers)
zssre
Next ⟩
zsscn
Metamath Proof Explorer
Ascii
Unicode
Theorem
zssre
Description:
The integers are a subset of the reals.
(Contributed by
NM
, 2-Aug-2004)
Ref
Expression
Assertion
zssre
⊢
ℤ
⊆
ℝ
Proof
Step
Hyp
Ref
Expression
1
zre
⊢
x
∈
ℤ
→
x
∈
ℝ
2
1
ssriv
⊢
ℤ
⊆
ℝ