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