Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
The floor and ceiling functions
flidz
Next ⟩
flltnz
Metamath Proof Explorer
Ascii
Unicode
Theorem
flidz
Description:
A real number equals its floor iff it is an integer.
(Contributed by
NM
, 11-Nov-2008)
Ref
Expression
Assertion
flidz
⊢
A
∈
ℝ
→
A
=
A
↔
A
∈
ℤ
Proof
Step
Hyp
Ref
Expression
1
flcl
⊢
A
∈
ℝ
→
A
∈
ℤ
2
eleq1
⊢
A
=
A
→
A
∈
ℤ
↔
A
∈
ℤ
3
1
2
syl5ibcom
⊢
A
∈
ℝ
→
A
=
A
→
A
∈
ℤ
4
flid
⊢
A
∈
ℤ
→
A
=
A
5
3
4
impbid1
⊢
A
∈
ℝ
→
A
=
A
↔
A
∈
ℤ