Theorem ceilcl

Description: Closure of the ceiling function. (Contributed by David A. Wheeler, 19-May-2015)

	Ref	Expression
Assertion	ceilcl	$$⊢A\in ℝ\to ⌈A⌉\in \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		ceilval	$$⊢A\in ℝ\to ⌈A⌉=-⌊-A⌋$$
2		ceicl	$$⊢A\in ℝ\to -⌊-A⌋\in \mathbb{Z}$$
3	1 2	eqeltrd	$$⊢A\in ℝ\to ⌈A⌉\in \mathbb{Z}$$