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