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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ⌊ ‘ 𝐴 ) ≤ 𝐵𝐴 < ( ( ⌊ ‘ 𝐵 ) + 1 ) ) )

Proof

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