Theorem ceile

Description: The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by Jeff Hankins, 10-Jun-2007)

	Ref	Expression
Assertion	ceile	|- ( ( A e. RR /\ B e. ZZ /\ A <_ B ) -> -u ( |_ ` -u A ) <_ B )

Proof

Step	Hyp	Ref	Expression
1		ceim1l	|- ( A e. RR -> ( -u ( |_ ` -u A ) - 1 ) < A )
2	1	adantr	|- ( ( A e. RR /\ B e. ZZ ) -> ( -u ( |_ ` -u A ) - 1 ) < A )
3		ceicl	|- ( A e. RR -> -u ( |_ ` -u A ) e. ZZ )
4		zre	|- ( -u ( |_ ` -u A ) e. ZZ -> -u ( |_ ` -u A ) e. RR )
5		peano2rem	|- ( -u ( |_ ` -u A ) e. RR -> ( -u ( |_ ` -u A ) - 1 ) e. RR )
6	3 4 5	3syl	|- ( A e. RR -> ( -u ( |_ ` -u A ) - 1 ) e. RR )
7	6	adantr	|- ( ( A e. RR /\ B e. ZZ ) -> ( -u ( |_ ` -u A ) - 1 ) e. RR )
8		simpl	|- ( ( A e. RR /\ B e. ZZ ) -> A e. RR )
9		zre	|- ( B e. ZZ -> B e. RR )
10	9	adantl	|- ( ( A e. RR /\ B e. ZZ ) -> B e. RR )
11		ltletr	|- ( ( ( -u ( |_ ` -u A ) - 1 ) e. RR /\ A e. RR /\ B e. RR ) -> ( ( ( -u ( |_ ` -u A ) - 1 ) < A /\ A <_ B ) -> ( -u ( |_ ` -u A ) - 1 ) < B ) )
12	7 8 10 11	syl3anc	|- ( ( A e. RR /\ B e. ZZ ) -> ( ( ( -u ( |_ ` -u A ) - 1 ) < A /\ A <_ B ) -> ( -u ( |_ ` -u A ) - 1 ) < B ) )
13	2 12	mpand	|- ( ( A e. RR /\ B e. ZZ ) -> ( A <_ B -> ( -u ( |_ ` -u A ) - 1 ) < B ) )
14		zlem1lt	|- ( ( -u ( |_ ` -u A ) e. ZZ /\ B e. ZZ ) -> ( -u ( |_ ` -u A ) <_ B <-> ( -u ( |_ ` -u A ) - 1 ) < B ) )
15	3 14	sylan	|- ( ( A e. RR /\ B e. ZZ ) -> ( -u ( |_ ` -u A ) <_ B <-> ( -u ( |_ ` -u A ) - 1 ) < B ) )
16	13 15	sylibrd	|- ( ( A e. RR /\ B e. ZZ ) -> ( A <_ B -> -u ( |_ ` -u A ) <_ B ) )
17	16	3impia	|- ( ( A e. RR /\ B e. ZZ /\ A <_ B ) -> -u ( |_ ` -u A ) <_ B )