Metamath Proof Explorer

Theorem ceim1l

Description: One less than the ceiling of a real number is strictly less than that number. (Contributed by Jeff Hankins, 10-Jun-2007)

Ref Expression
Assertion ceim1l 
|- ( A e. RR -> ( -u ( |_ ` -u A ) - 1 ) < A )

Proof

Step Hyp Ref Expression
1 renegcl 
 |-  ( A e. RR -> -u A e. RR )
2 reflcl 
 |-  ( -u A e. RR -> ( |_ ` -u A ) e. RR )
3 1 2 syl 
 |-  ( A e. RR -> ( |_ ` -u A ) e. RR )
4 3 recnd 
 |-  ( A e. RR -> ( |_ ` -u A ) e. CC )
5 ax-1cn 
 |-  1 e. CC
6 negdi 
 |-  ( ( ( |_ ` -u A ) e. CC /\ 1 e. CC ) -> -u ( ( |_ ` -u A ) + 1 ) = ( -u ( |_ ` -u A ) + -u 1 ) )
7 4 5 6 sylancl 
 |-  ( A e. RR -> -u ( ( |_ ` -u A ) + 1 ) = ( -u ( |_ ` -u A ) + -u 1 ) )
8 4 negcld 
 |-  ( A e. RR -> -u ( |_ ` -u A ) e. CC )
9 negsub 
 |-  ( ( -u ( |_ ` -u A ) e. CC /\ 1 e. CC ) -> ( -u ( |_ ` -u A ) + -u 1 ) = ( -u ( |_ ` -u A ) - 1 ) )
10 8 5 9 sylancl 
 |-  ( A e. RR -> ( -u ( |_ ` -u A ) + -u 1 ) = ( -u ( |_ ` -u A ) - 1 ) )
11 7 10 eqtr2d 
 |-  ( A e. RR -> ( -u ( |_ ` -u A ) - 1 ) = -u ( ( |_ ` -u A ) + 1 ) )
12 peano2re 
 |-  ( ( |_ ` -u A ) e. RR -> ( ( |_ ` -u A ) + 1 ) e. RR )
13 3 12 syl 
 |-  ( A e. RR -> ( ( |_ ` -u A ) + 1 ) e. RR )
14 flltp1 
 |-  ( -u A e. RR -> -u A < ( ( |_ ` -u A ) + 1 ) )
15 1 14 syl 
 |-  ( A e. RR -> -u A < ( ( |_ ` -u A ) + 1 ) )
16 15 adantr 
 |-  ( ( A e. RR /\ ( ( |_ ` -u A ) + 1 ) e. RR ) -> -u A < ( ( |_ ` -u A ) + 1 ) )
17 ltnegcon1 
 |-  ( ( A e. RR /\ ( ( |_ ` -u A ) + 1 ) e. RR ) -> ( -u A < ( ( |_ ` -u A ) + 1 ) <-> -u ( ( |_ ` -u A ) + 1 ) < A ) )
18 16 17 mpbid 
 |-  ( ( A e. RR /\ ( ( |_ ` -u A ) + 1 ) e. RR ) -> -u ( ( |_ ` -u A ) + 1 ) < A )
19 13 18 mpdan 
 |-  ( A e. RR -> -u ( ( |_ ` -u A ) + 1 ) < A )
20 11 19 eqbrtrd 
 |-  ( A e. RR -> ( -u ( |_ ` -u A ) - 1 ) < A )