Theorem ceicl

Description: The ceiling function returns an integer (closure law). (Contributed by Jeff Hankins, 10-Jun-2007)

	Ref	Expression
Assertion	ceicl	$$⊢A\in ℝ\to -⌊-A⌋\in \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		renegcl	$$⊢A\in ℝ\to -A\in ℝ$$
2	1	flcld	$$⊢A\in ℝ\to ⌊-A⌋\in \mathbb{Z}$$
3	2	znegcld	$$⊢A\in ℝ\to -⌊-A⌋\in \mathbb{Z}$$