Metamath Proof Explorer

Theorem fleqceilz

Description: A real number is an integer iff its floor equals its ceiling. (Contributed by AV, 30-Nov-2018)

Ref Expression
Assertion fleqceilz 
|- ( A e. RR -> ( A e. ZZ <-> ( |_ ` A ) = ( |^ ` A ) ) )

Proof

Step Hyp Ref Expression
1 flid 
 |-  ( A e. ZZ -> ( |_ ` A ) = A )
2 ceilid 
 |-  ( A e. ZZ -> ( |^ ` A ) = A )
3 1 2 eqtr4d 
 |-  ( A e. ZZ -> ( |_ ` A ) = ( |^ ` A ) )
4 eqeq1 
 |-  ( ( |_ ` A ) = A -> ( ( |_ ` A ) = ( |^ ` A ) <-> A = ( |^ ` A ) ) )
5 4 adantr 
 |-  ( ( ( |_ ` A ) = A /\ A e. RR ) -> ( ( |_ ` A ) = ( |^ ` A ) <-> A = ( |^ ` A ) ) )
6 ceilidz 
 |-  ( A e. RR -> ( A e. ZZ <-> ( |^ ` A ) = A ) )
7 eqcom 
 |-  ( ( |^ ` A ) = A <-> A = ( |^ ` A ) )
8 6 7 bitrdi 
 |-  ( A e. RR -> ( A e. ZZ <-> A = ( |^ ` A ) ) )
9 8 biimprd 
 |-  ( A e. RR -> ( A = ( |^ ` A ) -> A e. ZZ ) )
10 9 adantl 
 |-  ( ( ( |_ ` A ) = A /\ A e. RR ) -> ( A = ( |^ ` A ) -> A e. ZZ ) )
11 5 10 sylbid 
 |-  ( ( ( |_ ` A ) = A /\ A e. RR ) -> ( ( |_ ` A ) = ( |^ ` A ) -> A e. ZZ ) )
12 11 ex 
 |-  ( ( |_ ` A ) = A -> ( A e. RR -> ( ( |_ ` A ) = ( |^ ` A ) -> A e. ZZ ) ) )
13 flle 
 |-  ( A e. RR -> ( |_ ` A ) <_ A )
14 df-ne 
 |-  ( ( |_ ` A ) =/= A <-> -. ( |_ ` A ) = A )
15 necom 
 |-  ( ( |_ ` A ) =/= A <-> A =/= ( |_ ` A ) )
16 reflcl 
 |-  ( A e. RR -> ( |_ ` A ) e. RR )
17 id 
 |-  ( A e. RR -> A e. RR )
18 16 17 ltlend 
 |-  ( A e. RR -> ( ( |_ ` A ) < A <-> ( ( |_ ` A ) <_ A /\ A =/= ( |_ ` A ) ) ) )
19 breq1 
 |-  ( ( |_ ` A ) = ( |^ ` A ) -> ( ( |_ ` A ) < A <-> ( |^ ` A ) < A ) )
20 19 adantl 
 |-  ( ( A e. RR /\ ( |_ ` A ) = ( |^ ` A ) ) -> ( ( |_ ` A ) < A <-> ( |^ ` A ) < A ) )
21 ceilge 
 |-  ( A e. RR -> A <_ ( |^ ` A ) )
22 ceilcl 
 |-  ( A e. RR -> ( |^ ` A ) e. ZZ )
23 22 zred 
 |-  ( A e. RR -> ( |^ ` A ) e. RR )
24 17 23 lenltd 
 |-  ( A e. RR -> ( A <_ ( |^ ` A ) <-> -. ( |^ ` A ) < A ) )
25 pm2.21 
 |-  ( -. ( |^ ` A ) < A -> ( ( |^ ` A ) < A -> A e. ZZ ) )
26 24 25 syl6bi 
 |-  ( A e. RR -> ( A <_ ( |^ ` A ) -> ( ( |^ ` A ) < A -> A e. ZZ ) ) )
27 21 26 mpd 
 |-  ( A e. RR -> ( ( |^ ` A ) < A -> A e. ZZ ) )
28 27 adantr 
 |-  ( ( A e. RR /\ ( |_ ` A ) = ( |^ ` A ) ) -> ( ( |^ ` A ) < A -> A e. ZZ ) )
29 20 28 sylbid 
 |-  ( ( A e. RR /\ ( |_ ` A ) = ( |^ ` A ) ) -> ( ( |_ ` A ) < A -> A e. ZZ ) )
30 29 ex 
 |-  ( A e. RR -> ( ( |_ ` A ) = ( |^ ` A ) -> ( ( |_ ` A ) < A -> A e. ZZ ) ) )
31 30 com23 
 |-  ( A e. RR -> ( ( |_ ` A ) < A -> ( ( |_ ` A ) = ( |^ ` A ) -> A e. ZZ ) ) )
32 18 31 sylbird 
 |-  ( A e. RR -> ( ( ( |_ ` A ) <_ A /\ A =/= ( |_ ` A ) ) -> ( ( |_ ` A ) = ( |^ ` A ) -> A e. ZZ ) ) )
33 32 expd 
 |-  ( A e. RR -> ( ( |_ ` A ) <_ A -> ( A =/= ( |_ ` A ) -> ( ( |_ ` A ) = ( |^ ` A ) -> A e. ZZ ) ) ) )
34 33 com3r 
 |-  ( A =/= ( |_ ` A ) -> ( A e. RR -> ( ( |_ ` A ) <_ A -> ( ( |_ ` A ) = ( |^ ` A ) -> A e. ZZ ) ) ) )
35 15 34 sylbi 
 |-  ( ( |_ ` A ) =/= A -> ( A e. RR -> ( ( |_ ` A ) <_ A -> ( ( |_ ` A ) = ( |^ ` A ) -> A e. ZZ ) ) ) )
36 14 35 sylbir 
 |-  ( -. ( |_ ` A ) = A -> ( A e. RR -> ( ( |_ ` A ) <_ A -> ( ( |_ ` A ) = ( |^ ` A ) -> A e. ZZ ) ) ) )
37 13 36 mpdi 
 |-  ( -. ( |_ ` A ) = A -> ( A e. RR -> ( ( |_ ` A ) = ( |^ ` A ) -> A e. ZZ ) ) )
38 12 37 pm2.61i 
 |-  ( A e. RR -> ( ( |_ ` A ) = ( |^ ` A ) -> A e. ZZ ) )
39 3 38 impbid2 
 |-  ( A e. RR -> ( A e. ZZ <-> ( |_ ` A ) = ( |^ ` A ) ) )