Metamath Proof Explorer


Theorem flflp1

Description: Move floor function between strict and non-strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017)

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

Proof

Step Hyp Ref Expression
1 flltp1
 |-  ( A e. RR -> A < ( ( |_ ` A ) + 1 ) )
2 1 ad3antrrr
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) <_ B ) /\ B < A ) -> A < ( ( |_ ` A ) + 1 ) )
3 flval
 |-  ( B e. RR -> ( |_ ` B ) = ( iota_ x e. ZZ ( x <_ B /\ B < ( x + 1 ) ) ) )
4 3 ad3antlr
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) <_ B ) /\ B < A ) -> ( |_ ` B ) = ( iota_ x e. ZZ ( x <_ B /\ B < ( x + 1 ) ) ) )
5 simplr
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) <_ B ) /\ B < A ) -> ( |_ ` A ) <_ B )
6 1 adantr
 |-  ( ( A e. RR /\ B e. RR ) -> A < ( ( |_ ` A ) + 1 ) )
7 reflcl
 |-  ( A e. RR -> ( |_ ` A ) e. RR )
8 peano2re
 |-  ( ( |_ ` A ) e. RR -> ( ( |_ ` A ) + 1 ) e. RR )
9 7 8 syl
 |-  ( A e. RR -> ( ( |_ ` A ) + 1 ) e. RR )
10 9 adantl
 |-  ( ( B e. RR /\ A e. RR ) -> ( ( |_ ` A ) + 1 ) e. RR )
11 lttr
 |-  ( ( B e. RR /\ A e. RR /\ ( ( |_ ` A ) + 1 ) e. RR ) -> ( ( B < A /\ A < ( ( |_ ` A ) + 1 ) ) -> B < ( ( |_ ` A ) + 1 ) ) )
12 10 11 mpd3an3
 |-  ( ( B e. RR /\ A e. RR ) -> ( ( B < A /\ A < ( ( |_ ` A ) + 1 ) ) -> B < ( ( |_ ` A ) + 1 ) ) )
13 12 ancoms
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( B < A /\ A < ( ( |_ ` A ) + 1 ) ) -> B < ( ( |_ ` A ) + 1 ) ) )
14 6 13 mpan2d
 |-  ( ( A e. RR /\ B e. RR ) -> ( B < A -> B < ( ( |_ ` A ) + 1 ) ) )
15 14 imp
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> B < ( ( |_ ` A ) + 1 ) )
16 15 adantlr
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) <_ B ) /\ B < A ) -> B < ( ( |_ ` A ) + 1 ) )
17 flcl
 |-  ( A e. RR -> ( |_ ` A ) e. ZZ )
18 rebtwnz
 |-  ( B e. RR -> E! x e. ZZ ( x <_ B /\ B < ( x + 1 ) ) )
19 breq1
 |-  ( x = ( |_ ` A ) -> ( x <_ B <-> ( |_ ` A ) <_ B ) )
20 oveq1
 |-  ( x = ( |_ ` A ) -> ( x + 1 ) = ( ( |_ ` A ) + 1 ) )
21 20 breq2d
 |-  ( x = ( |_ ` A ) -> ( B < ( x + 1 ) <-> B < ( ( |_ ` A ) + 1 ) ) )
22 19 21 anbi12d
 |-  ( x = ( |_ ` A ) -> ( ( x <_ B /\ B < ( x + 1 ) ) <-> ( ( |_ ` A ) <_ B /\ B < ( ( |_ ` A ) + 1 ) ) ) )
23 22 riota2
 |-  ( ( ( |_ ` A ) e. ZZ /\ E! x e. ZZ ( x <_ B /\ B < ( x + 1 ) ) ) -> ( ( ( |_ ` A ) <_ B /\ B < ( ( |_ ` A ) + 1 ) ) <-> ( iota_ x e. ZZ ( x <_ B /\ B < ( x + 1 ) ) ) = ( |_ ` A ) ) )
24 17 18 23 syl2an
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( |_ ` A ) <_ B /\ B < ( ( |_ ` A ) + 1 ) ) <-> ( iota_ x e. ZZ ( x <_ B /\ B < ( x + 1 ) ) ) = ( |_ ` A ) ) )
25 24 ad2antrr
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) <_ B ) /\ B < A ) -> ( ( ( |_ ` A ) <_ B /\ B < ( ( |_ ` A ) + 1 ) ) <-> ( iota_ x e. ZZ ( x <_ B /\ B < ( x + 1 ) ) ) = ( |_ ` A ) ) )
26 5 16 25 mpbi2and
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) <_ B ) /\ B < A ) -> ( iota_ x e. ZZ ( x <_ B /\ B < ( x + 1 ) ) ) = ( |_ ` A ) )
27 4 26 eqtrd
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) <_ B ) /\ B < A ) -> ( |_ ` B ) = ( |_ ` A ) )
28 27 oveq1d
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) <_ B ) /\ B < A ) -> ( ( |_ ` B ) + 1 ) = ( ( |_ ` A ) + 1 ) )
29 2 28 breqtrrd
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) <_ B ) /\ B < A ) -> A < ( ( |_ ` B ) + 1 ) )
30 29 ex
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) <_ B ) -> ( B < A -> A < ( ( |_ ` B ) + 1 ) ) )
31 lenlt
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
32 flltp1
 |-  ( B e. RR -> B < ( ( |_ ` B ) + 1 ) )
33 32 adantl
 |-  ( ( A e. RR /\ B e. RR ) -> B < ( ( |_ ` B ) + 1 ) )
34 reflcl
 |-  ( B e. RR -> ( |_ ` B ) e. RR )
35 peano2re
 |-  ( ( |_ ` B ) e. RR -> ( ( |_ ` B ) + 1 ) e. RR )
36 34 35 syl
 |-  ( B e. RR -> ( ( |_ ` B ) + 1 ) e. RR )
37 36 adantl
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( |_ ` B ) + 1 ) e. RR )
38 lelttr
 |-  ( ( A e. RR /\ B e. RR /\ ( ( |_ ` B ) + 1 ) e. RR ) -> ( ( A <_ B /\ B < ( ( |_ ` B ) + 1 ) ) -> A < ( ( |_ ` B ) + 1 ) ) )
39 37 38 mpd3an3
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A <_ B /\ B < ( ( |_ ` B ) + 1 ) ) -> A < ( ( |_ ` B ) + 1 ) ) )
40 33 39 mpan2d
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B -> A < ( ( |_ ` B ) + 1 ) ) )
41 31 40 sylbird
 |-  ( ( A e. RR /\ B e. RR ) -> ( -. B < A -> A < ( ( |_ ` B ) + 1 ) ) )
42 41 adantr
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) <_ B ) -> ( -. B < A -> A < ( ( |_ ` B ) + 1 ) ) )
43 30 42 pm2.61d
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) <_ B ) -> A < ( ( |_ ` B ) + 1 ) )
44 flval
 |-  ( A e. RR -> ( |_ ` A ) = ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) )
45 44 ad3antrrr
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A < ( ( |_ ` B ) + 1 ) ) /\ B < A ) -> ( |_ ` A ) = ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) )
46 34 ad2antlr
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( |_ ` B ) e. RR )
47 simpll
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> A e. RR )
48 simplr
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> B e. RR )
49 flle
 |-  ( B e. RR -> ( |_ ` B ) <_ B )
50 49 ad2antlr
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( |_ ` B ) <_ B )
51 simpr
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> B < A )
52 46 48 47 50 51 lelttrd
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( |_ ` B ) < A )
53 46 47 52 ltled
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( |_ ` B ) <_ A )
54 53 adantlr
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A < ( ( |_ ` B ) + 1 ) ) /\ B < A ) -> ( |_ ` B ) <_ A )
55 simplr
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A < ( ( |_ ` B ) + 1 ) ) /\ B < A ) -> A < ( ( |_ ` B ) + 1 ) )
56 flcl
 |-  ( B e. RR -> ( |_ ` B ) e. ZZ )
57 rebtwnz
 |-  ( A e. RR -> E! x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) )
58 breq1
 |-  ( x = ( |_ ` B ) -> ( x <_ A <-> ( |_ ` B ) <_ A ) )
59 oveq1
 |-  ( x = ( |_ ` B ) -> ( x + 1 ) = ( ( |_ ` B ) + 1 ) )
60 59 breq2d
 |-  ( x = ( |_ ` B ) -> ( A < ( x + 1 ) <-> A < ( ( |_ ` B ) + 1 ) ) )
61 58 60 anbi12d
 |-  ( x = ( |_ ` B ) -> ( ( x <_ A /\ A < ( x + 1 ) ) <-> ( ( |_ ` B ) <_ A /\ A < ( ( |_ ` B ) + 1 ) ) ) )
62 61 riota2
 |-  ( ( ( |_ ` B ) e. ZZ /\ E! x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) -> ( ( ( |_ ` B ) <_ A /\ A < ( ( |_ ` B ) + 1 ) ) <-> ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) = ( |_ ` B ) ) )
63 56 57 62 syl2anr
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( |_ ` B ) <_ A /\ A < ( ( |_ ` B ) + 1 ) ) <-> ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) = ( |_ ` B ) ) )
64 63 ad2antrr
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A < ( ( |_ ` B ) + 1 ) ) /\ B < A ) -> ( ( ( |_ ` B ) <_ A /\ A < ( ( |_ ` B ) + 1 ) ) <-> ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) = ( |_ ` B ) ) )
65 54 55 64 mpbi2and
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A < ( ( |_ ` B ) + 1 ) ) /\ B < A ) -> ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) = ( |_ ` B ) )
66 45 65 eqtrd
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A < ( ( |_ ` B ) + 1 ) ) /\ B < A ) -> ( |_ ` A ) = ( |_ ` B ) )
67 49 ad3antlr
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A < ( ( |_ ` B ) + 1 ) ) /\ B < A ) -> ( |_ ` B ) <_ B )
68 66 67 eqbrtrd
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A < ( ( |_ ` B ) + 1 ) ) /\ B < A ) -> ( |_ ` A ) <_ B )
69 68 ex
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < ( ( |_ ` B ) + 1 ) ) -> ( B < A -> ( |_ ` A ) <_ B ) )
70 flle
 |-  ( A e. RR -> ( |_ ` A ) <_ A )
71 70 adantr
 |-  ( ( A e. RR /\ B e. RR ) -> ( |_ ` A ) <_ A )
72 7 adantr
 |-  ( ( A e. RR /\ B e. RR ) -> ( |_ ` A ) e. RR )
73 letr
 |-  ( ( ( |_ ` A ) e. RR /\ A e. RR /\ B e. RR ) -> ( ( ( |_ ` A ) <_ A /\ A <_ B ) -> ( |_ ` A ) <_ B ) )
74 73 3coml
 |-  ( ( A e. RR /\ B e. RR /\ ( |_ ` A ) e. RR ) -> ( ( ( |_ ` A ) <_ A /\ A <_ B ) -> ( |_ ` A ) <_ B ) )
75 72 74 mpd3an3
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( |_ ` A ) <_ A /\ A <_ B ) -> ( |_ ` A ) <_ B ) )
76 71 75 mpand
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B -> ( |_ ` A ) <_ B ) )
77 31 76 sylbird
 |-  ( ( A e. RR /\ B e. RR ) -> ( -. B < A -> ( |_ ` A ) <_ B ) )
78 77 adantr
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < ( ( |_ ` B ) + 1 ) ) -> ( -. B < A -> ( |_ ` A ) <_ B ) )
79 69 78 pm2.61d
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < ( ( |_ ` B ) + 1 ) ) -> ( |_ ` A ) <_ B )
80 43 79 impbida
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( |_ ` A ) <_ B <-> A < ( ( |_ ` B ) + 1 ) ) )