Metamath Proof Explorer

Theorem ltflcei

Description: Theorem to move the floor function across a strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017)

Ref Expression
Assertion ltflcei ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A < − − B

Proof

Step Hyp Ref Expression
1 flltp1 ⊢ A ∈ ℝ → A < A + 1
2 1 ad3antrrr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B ∧ B ≤ A → A < A + 1
3 renegcl ⊢ B ∈ ℝ → − B ∈ ℝ
4 flval ⊢ − B ∈ ℝ → − B = ι x ∈ ℤ | x ≤ − B ∧ − B < x + 1
5 3 4 syl ⊢ B ∈ ℝ → − B = ι x ∈ ℤ | x ≤ − B ∧ − B < x + 1
6 5 ad3antlr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B ∧ B ≤ A → − B = ι x ∈ ℤ | x ≤ − B ∧ − B < x + 1
7 fllep1 ⊢ A ∈ ℝ → A ≤ A + 1
8 7 adantl ⊢ B ∈ ℝ ∧ A ∈ ℝ → A ≤ A + 1
9 reflcl ⊢ A ∈ ℝ → A ∈ ℝ
10 peano2re ⊢ A ∈ ℝ → A + 1 ∈ ℝ
11 9 10 syl ⊢ A ∈ ℝ → A + 1 ∈ ℝ
12 11 adantl ⊢ B ∈ ℝ ∧ A ∈ ℝ → A + 1 ∈ ℝ
13 letr ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ A + 1 ∈ ℝ → B ≤ A ∧ A ≤ A + 1 → B ≤ A + 1
14 12 13 mpd3an3 ⊢ B ∈ ℝ ∧ A ∈ ℝ → B ≤ A ∧ A ≤ A + 1 → B ≤ A + 1
15 8 14 mpan2d ⊢ B ∈ ℝ ∧ A ∈ ℝ → B ≤ A → B ≤ A + 1
16 leneg ⊢ B ∈ ℝ ∧ A + 1 ∈ ℝ → B ≤ A + 1 ↔ − A + 1 ≤ − B
17 11 16 sylan2 ⊢ B ∈ ℝ ∧ A ∈ ℝ → B ≤ A + 1 ↔ − A + 1 ≤ − B
18 15 17 sylibd ⊢ B ∈ ℝ ∧ A ∈ ℝ → B ≤ A → − A + 1 ≤ − B
19 18 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ≤ A → − A + 1 ≤ − B
20 ltneg ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ − B < − A
21 9 20 sylan ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ − B < − A
22 9 recnd ⊢ A ∈ ℝ → A ∈ ℂ
23 ax-1cn ⊢ 1 ∈ ℂ
24 negdi2 ⊢ A ∈ ℂ ∧ 1 ∈ ℂ → − A + 1 = - A - 1
25 24 oveq1d ⊢ A ∈ ℂ ∧ 1 ∈ ℂ → - A + 1 + 1 = − A - 1 + 1
26 negcl ⊢ A ∈ ℂ → − A ∈ ℂ
27 npcan ⊢ − A ∈ ℂ ∧ 1 ∈ ℂ → − A - 1 + 1 = − A
28 26 27 sylan ⊢ A ∈ ℂ ∧ 1 ∈ ℂ → − A - 1 + 1 = − A
29 25 28 eqtr2d ⊢ A ∈ ℂ ∧ 1 ∈ ℂ → − A = - A + 1 + 1
30 22 23 29 sylancl ⊢ A ∈ ℝ → − A = - A + 1 + 1
31 30 breq2d ⊢ A ∈ ℝ → − B < − A ↔ − B < - A + 1 + 1
32 31 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ → − B < − A ↔ − B < - A + 1 + 1
33 21 32 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ − B < - A + 1 + 1
34 33 biimpd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B → − B < - A + 1 + 1
35 19 34 anim12d ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ≤ A ∧ A < B → − A + 1 ≤ − B ∧ − B < - A + 1 + 1
36 35 ancomsd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ∧ B ≤ A → − A + 1 ≤ − B ∧ − B < - A + 1 + 1
37 36 impl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B ∧ B ≤ A → − A + 1 ≤ − B ∧ − B < - A + 1 + 1
38 flcl ⊢ A ∈ ℝ → A ∈ ℤ
39 38 peano2zd ⊢ A ∈ ℝ → A + 1 ∈ ℤ
40 39 znegcld ⊢ A ∈ ℝ → − A + 1 ∈ ℤ
41 rebtwnz ⊢ − B ∈ ℝ → ∃! x ∈ ℤ x ≤ − B ∧ − B < x + 1
42 3 41 syl ⊢ B ∈ ℝ → ∃! x ∈ ℤ x ≤ − B ∧ − B < x + 1
43 breq1 ⊢ x = − A + 1 → x ≤ − B ↔ − A + 1 ≤ − B
44 oveq1 ⊢ x = − A + 1 → x + 1 = - A + 1 + 1
45 44 breq2d ⊢ x = − A + 1 → − B < x + 1 ↔ − B < - A + 1 + 1
46 43 45 anbi12d ⊢ x = − A + 1 → x ≤ − B ∧ − B < x + 1 ↔ − A + 1 ≤ − B ∧ − B < - A + 1 + 1
47 46 riota2 ⊢ − A + 1 ∈ ℤ ∧ ∃! x ∈ ℤ x ≤ − B ∧ − B < x + 1 → − A + 1 ≤ − B ∧ − B < - A + 1 + 1 ↔ ι x ∈ ℤ | x ≤ − B ∧ − B < x + 1 = − A + 1
48 40 42 47 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → − A + 1 ≤ − B ∧ − B < - A + 1 + 1 ↔ ι x ∈ ℤ | x ≤ − B ∧ − B < x + 1 = − A + 1
49 48 ad2antrr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B ∧ B ≤ A → − A + 1 ≤ − B ∧ − B < - A + 1 + 1 ↔ ι x ∈ ℤ | x ≤ − B ∧ − B < x + 1 = − A + 1
50 37 49 mpbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B ∧ B ≤ A → ι x ∈ ℤ | x ≤ − B ∧ − B < x + 1 = − A + 1
51 6 50 eqtrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B ∧ B ≤ A → − B = − A + 1
52 38 zcnd ⊢ A ∈ ℝ → A ∈ ℂ
53 peano2cn ⊢ A ∈ ℂ → A + 1 ∈ ℂ
54 52 53 syl ⊢ A ∈ ℝ → A + 1 ∈ ℂ
55 3 flcld ⊢ B ∈ ℝ → − B ∈ ℤ
56 55 zcnd ⊢ B ∈ ℝ → − B ∈ ℂ
57 negcon2 ⊢ A + 1 ∈ ℂ ∧ − B ∈ ℂ → A + 1 = − − B ↔ − B = − A + 1
58 54 56 57 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + 1 = − − B ↔ − B = − A + 1
59 58 ad2antrr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B ∧ B ≤ A → A + 1 = − − B ↔ − B = − A + 1
60 51 59 mpbird ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B ∧ B ≤ A → A + 1 = − − B
61 2 60 breqtrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B ∧ B ≤ A → A < − − B
62 61 ex ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → B ≤ A → A < − − B
63 ltnle ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ ¬ B ≤ A
64 ceige ⊢ B ∈ ℝ → B ≤ − − B
65 64 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ≤ − − B
66 ceicl ⊢ B ∈ ℝ → − − B ∈ ℤ
67 66 zred ⊢ B ∈ ℝ → − − B ∈ ℝ
68 67 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ → − − B ∈ ℝ
69 ltletr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ − − B ∈ ℝ → A < B ∧ B ≤ − − B → A < − − B
70 68 69 mpd3an3 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ∧ B ≤ − − B → A < − − B
71 65 70 mpan2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B → A < − − B
72 63 71 sylbird ⊢ A ∈ ℝ ∧ B ∈ ℝ → ¬ B ≤ A → A < − − B
73 72 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → ¬ B ≤ A → A < − − B
74 62 73 pm2.61d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → A < − − B
75 flval ⊢ A ∈ ℝ → A = ι x ∈ ℤ | x ≤ A ∧ A < x + 1
76 75 ad3antrrr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < − − B ∧ B ≤ A → A = ι x ∈ ℤ | x ≤ A ∧ A < x + 1
77 ceim1l ⊢ B ∈ ℝ → - − B - 1 < B
78 77 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ → - − B - 1 < B
79 peano2rem ⊢ − − B ∈ ℝ → - − B - 1 ∈ ℝ
80 67 79 syl ⊢ B ∈ ℝ → - − B - 1 ∈ ℝ
81 80 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ → - − B - 1 ∈ ℝ
82 ltleletr ⊢ - − B - 1 ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ → - − B - 1 < B ∧ B ≤ A → - − B - 1 ≤ A
83 82 3com13 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ - − B - 1 ∈ ℝ → - − B - 1 < B ∧ B ≤ A → - − B - 1 ≤ A
84 81 83 mpd3an3 ⊢ A ∈ ℝ ∧ B ∈ ℝ → - − B - 1 < B ∧ B ≤ A → - − B - 1 ≤ A
85 78 84 mpand ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ≤ A → - − B - 1 ≤ A
86 66 zcnd ⊢ B ∈ ℝ → − − B ∈ ℂ
87 npcan ⊢ − − B ∈ ℂ ∧ 1 ∈ ℂ → − − B - 1 + 1 = − − B
88 86 23 87 sylancl ⊢ B ∈ ℝ → − − B - 1 + 1 = − − B
89 88 breq2d ⊢ B ∈ ℝ → A < − − B - 1 + 1 ↔ A < − − B
90 89 biimprd ⊢ B ∈ ℝ → A < − − B → A < − − B - 1 + 1
91 90 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < − − B → A < − − B - 1 + 1
92 85 91 anim12d ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ≤ A ∧ A < − − B → - − B - 1 ≤ A ∧ A < − − B - 1 + 1
93 92 ancomsd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < − − B ∧ B ≤ A → - − B - 1 ≤ A ∧ A < − − B - 1 + 1
94 93 impl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < − − B ∧ B ≤ A → - − B - 1 ≤ A ∧ A < − − B - 1 + 1
95 peano2zm ⊢ − − B ∈ ℤ → - − B - 1 ∈ ℤ
96 66 95 syl ⊢ B ∈ ℝ → - − B - 1 ∈ ℤ
97 rebtwnz ⊢ A ∈ ℝ → ∃! x ∈ ℤ x ≤ A ∧ A < x + 1
98 breq1 ⊢ x = - − B - 1 → x ≤ A ↔ - − B - 1 ≤ A
99 oveq1 ⊢ x = - − B - 1 → x + 1 = − − B - 1 + 1
100 99 breq2d ⊢ x = - − B - 1 → A < x + 1 ↔ A < − − B - 1 + 1
101 98 100 anbi12d ⊢ x = - − B - 1 → x ≤ A ∧ A < x + 1 ↔ - − B - 1 ≤ A ∧ A < − − B - 1 + 1
102 101 riota2 ⊢ - − B - 1 ∈ ℤ ∧ ∃! x ∈ ℤ x ≤ A ∧ A < x + 1 → - − B - 1 ≤ A ∧ A < − − B - 1 + 1 ↔ ι x ∈ ℤ | x ≤ A ∧ A < x + 1 = - − B - 1
103 96 97 102 syl2anr ⊢ A ∈ ℝ ∧ B ∈ ℝ → - − B - 1 ≤ A ∧ A < − − B - 1 + 1 ↔ ι x ∈ ℤ | x ≤ A ∧ A < x + 1 = - − B - 1
104 103 ad2antrr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < − − B ∧ B ≤ A → - − B - 1 ≤ A ∧ A < − − B - 1 + 1 ↔ ι x ∈ ℤ | x ≤ A ∧ A < x + 1 = - − B - 1
105 94 104 mpbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < − − B ∧ B ≤ A → ι x ∈ ℤ | x ≤ A ∧ A < x + 1 = - − B - 1
106 76 105 eqtrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < − − B ∧ B ≤ A → A = - − B - 1
107 77 ad3antlr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < − − B ∧ B ≤ A → - − B - 1 < B
108 106 107 eqbrtrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < − − B ∧ B ≤ A → A < B
109 108 ex ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < − − B → B ≤ A → A < B
110 flle ⊢ A ∈ ℝ → A ≤ A
111 110 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ A
112 9 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ∈ ℝ
113 lelttr ⊢ A ∈ ℝ ∧ A ∈ ℝ ∧ B ∈ ℝ → A ≤ A ∧ A < B → A < B
114 113 3coml ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ → A ≤ A ∧ A < B → A < B
115 112 114 mpd3an3 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ A ∧ A < B → A < B
116 111 115 mpand ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B → A < B
117 63 116 sylbird ⊢ A ∈ ℝ ∧ B ∈ ℝ → ¬ B ≤ A → A < B
118 117 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < − − B → ¬ B ≤ A → A < B
119 109 118 pm2.61d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < − − B → A < B
120 74 119 impbida ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A < − − B