Metamath Proof Explorer


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