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

Metamath Proof Explorer

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 )