Theorem ceille

Description: The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by AV, 30-Nov-2018)

	Ref	Expression
Assertion	ceille	$$⊢\left(A\in ℝ\wedge B\in \mathbb{Z}\wedge A\le B\right)\to ⌈A⌉\le B$$

Proof

Step	Hyp	Ref	Expression
1		ceilval	$$⊢A\in ℝ\to ⌈A⌉=-⌊-A⌋$$
2	1	3ad2ant1	$$⊢\left(A\in ℝ\wedge B\in \mathbb{Z}\wedge A\le B\right)\to ⌈A⌉=-⌊-A⌋$$
3		ceile	$$⊢\left(A\in ℝ\wedge B\in \mathbb{Z}\wedge A\le B\right)\to -⌊-A⌋\le B$$
4	2 3	eqbrtrd	$$⊢\left(A\in ℝ\wedge B\in \mathbb{Z}\wedge A\le B\right)\to ⌈A⌉\le B$$