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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ⌊ ‘ 𝐴 ) < 𝐵 ↔ 𝐴 < - ( ⌊ ‘ - 𝐵 ) ) )

Proof

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