Database
REAL AND COMPLEX NUMBERS
Integer sets
Integers (as a subset of complex numbers)
zrei
Next ⟩
zssre
Metamath Proof Explorer
Ascii
Unicode
Theorem
zrei
Description:
An integer is a real number.
(Contributed by
NM
, 14-Jul-2005)
Ref
Expression
Hypothesis
zrei.1
⊢
A
∈
ℤ
Assertion
zrei
⊢
A
∈
ℝ
Proof
Step
Hyp
Ref
Expression
1
zrei.1
⊢
A
∈
ℤ
2
zre
⊢
A
∈
ℤ
→
A
∈
ℝ
3
1
2
ax-mp
⊢
A
∈
ℝ