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 ) ) )