This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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