This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ℤ$

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