Metamath Proof Explorer

Theorem ceilbi

Description: A condition equivalent to ceiling. Analogous to flbi . (Contributed by AV, 2-Nov-2025)

Ref Expression
Assertion ceilbi 
|- ( ( A e. RR /\ B e. ZZ ) -> ( ( |^ ` A ) = B <-> ( A <_ B /\ B < ( A + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 ceilval 
 |-  ( A e. RR -> ( |^ ` A ) = -u ( |_ ` -u A ) )
2 1 adantr 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( |^ ` A ) = -u ( |_ ` -u A ) )
3 2 eqeq1d 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( ( |^ ` A ) = B <-> -u ( |_ ` -u A ) = B ) )
4 renegcl 
 |-  ( A e. RR -> -u A e. RR )
5 4 flcld 
 |-  ( A e. RR -> ( |_ ` -u A ) e. ZZ )
6 5 zcnd 
 |-  ( A e. RR -> ( |_ ` -u A ) e. CC )
7 zcn 
 |-  ( B e. ZZ -> B e. CC )
8 negcon1 
 |-  ( ( ( |_ ` -u A ) e. CC /\ B e. CC ) -> ( -u ( |_ ` -u A ) = B <-> -u B = ( |_ ` -u A ) ) )
9 6 7 8 syl2an 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( -u ( |_ ` -u A ) = B <-> -u B = ( |_ ` -u A ) ) )
10 eqcom 
 |-  ( -u B = ( |_ ` -u A ) <-> ( |_ ` -u A ) = -u B )
11 10 a1i 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( -u B = ( |_ ` -u A ) <-> ( |_ ` -u A ) = -u B ) )
12 znegcl 
 |-  ( B e. ZZ -> -u B e. ZZ )
13 flbi 
 |-  ( ( -u A e. RR /\ -u B e. ZZ ) -> ( ( |_ ` -u A ) = -u B <-> ( -u B <_ -u A /\ -u A < ( -u B + 1 ) ) ) )
14 4 12 13 syl2an 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( ( |_ ` -u A ) = -u B <-> ( -u B <_ -u A /\ -u A < ( -u B + 1 ) ) ) )
15 simpl 
 |-  ( ( A e. RR /\ B e. ZZ ) -> A e. RR )
16 zre 
 |-  ( B e. ZZ -> B e. RR )
17 16 adantl 
 |-  ( ( A e. RR /\ B e. ZZ ) -> B e. RR )
18 15 17 lenegd 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( A <_ B <-> -u B <_ -u A ) )
19 18 bicomd 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( -u B <_ -u A <-> A <_ B ) )
20 peano2rem 
 |-  ( B e. RR -> ( B - 1 ) e. RR )
21 16 20 syl 
 |-  ( B e. ZZ -> ( B - 1 ) e. RR )
22 21 adantl 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( B - 1 ) e. RR )
23 22 15 ltnegd 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( ( B - 1 ) < A <-> -u A < -u ( B - 1 ) ) )
24 1red 
 |-  ( ( A e. RR /\ B e. ZZ ) -> 1 e. RR )
25 17 24 15 ltsubaddd 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( ( B - 1 ) < A <-> B < ( A + 1 ) ) )
26 1cnd 
 |-  ( A e. RR -> 1 e. CC )
27 negsubdi 
 |-  ( ( B e. CC /\ 1 e. CC ) -> -u ( B - 1 ) = ( -u B + 1 ) )
28 7 26 27 syl2anr 
 |-  ( ( A e. RR /\ B e. ZZ ) -> -u ( B - 1 ) = ( -u B + 1 ) )
29 28 breq2d 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( -u A < -u ( B - 1 ) <-> -u A < ( -u B + 1 ) ) )
30 23 25 29 3bitr3rd 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( -u A < ( -u B + 1 ) <-> B < ( A + 1 ) ) )
31 19 30 anbi12d 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( ( -u B <_ -u A /\ -u A < ( -u B + 1 ) ) <-> ( A <_ B /\ B < ( A + 1 ) ) ) )
32 11 14 31 3bitrd 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( -u B = ( |_ ` -u A ) <-> ( A <_ B /\ B < ( A + 1 ) ) ) )
33 3 9 32 3bitrd 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( ( |^ ` A ) = B <-> ( A <_ B /\ B < ( A + 1 ) ) ) )