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	|- ( ( A e. RR /\ B e. ZZ /\ A <_ B ) -> ( |^ ` A ) <_ B )

Proof

Step	Hyp	Ref	Expression
1		ceilval	|- ( A e. RR -> ( |^ ` A ) = -u ( |_ ` -u A ) )
2	1	3ad2ant1	|- ( ( A e. RR /\ B e. ZZ /\ A <_ B ) -> ( |^ ` A ) = -u ( |_ ` -u A ) )
3		ceile	|- ( ( A e. RR /\ B e. ZZ /\ A <_ B ) -> -u ( |_ ` -u A ) <_ B )
4	2 3	eqbrtrd	|- ( ( A e. RR /\ B e. ZZ /\ A <_ B ) -> ( |^ ` A ) <_ B )