Theorem ceicl

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

	Ref	Expression
Assertion	ceicl	⊢ ( 𝐴 ∈ ℝ → - ( ⌊ ‘ - 𝐴 ) ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		renegcl	⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
2	1	flcld	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ - 𝐴 ) ∈ ℤ )
3	2	znegcld	⊢ ( 𝐴 ∈ ℝ → - ( ⌊ ‘ - 𝐴 ) ∈ ℤ )