Theorem ceilcl

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

	Ref	Expression
Assertion	ceilcl	⊢ ( 𝐴 ∈ ℝ → ( ⌈ ‘ 𝐴 ) ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		ceilval	⊢ ( 𝐴 ∈ ℝ → ( ⌈ ‘ 𝐴 ) = - ( ⌊ ‘ - 𝐴 ) )
2		ceicl	⊢ ( 𝐴 ∈ ℝ → - ( ⌊ ‘ - 𝐴 ) ∈ ℤ )
3	1 2	eqeltrd	⊢ ( 𝐴 ∈ ℝ → ( ⌈ ‘ 𝐴 ) ∈ ℤ )