Metamath Proof Explorer


Theorem flcl

Description: The floor (greatest integer) function is an integer (closure law). (Contributed by NM, 15-Nov-2004) (Revised by Mario Carneiro, 2-Nov-2013)

Ref Expression
Assertion flcl A A

Proof

Step Hyp Ref Expression
1 flval A A = ι x | x A A < x + 1
2 rebtwnz A ∃! x x A A < x + 1
3 riotacl ∃! x x A A < x + 1 ι x | x A A < x + 1
4 2 3 syl A ι x | x A A < x + 1
5 1 4 eqeltrd A A