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 ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ A < B + 1

Proof

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