| Step | Hyp | Ref
| Expression |
| 1 | | flltp1 13840 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → 𝐴 < ((⌊‘𝐴) + 1)) |
| 2 | 1 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) <
𝐵) ∧ 𝐵 ≤ 𝐴) → 𝐴 < ((⌊‘𝐴) + 1)) |
| 3 | | renegcl 11572 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ → -𝐵 ∈
ℝ) |
| 4 | | flval 13834 |
. . . . . . . . 9
⊢ (-𝐵 ∈ ℝ →
(⌊‘-𝐵) =
(℩𝑥 ∈
ℤ (𝑥 ≤ -𝐵 ∧ -𝐵 < (𝑥 + 1)))) |
| 5 | 3, 4 | syl 17 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ →
(⌊‘-𝐵) =
(℩𝑥 ∈
ℤ (𝑥 ≤ -𝐵 ∧ -𝐵 < (𝑥 + 1)))) |
| 6 | 5 | ad3antlr 731 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) <
𝐵) ∧ 𝐵 ≤ 𝐴) → (⌊‘-𝐵) = (℩𝑥 ∈ ℤ (𝑥 ≤ -𝐵 ∧ -𝐵 < (𝑥 + 1)))) |
| 7 | | fllep1 13841 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ ((⌊‘𝐴) + 1)) |
| 8 | 7 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → 𝐴 ≤ ((⌊‘𝐴) + 1)) |
| 9 | | reflcl 13836 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
| 10 | | peano2re 11434 |
. . . . . . . . . . . . . . . . 17
⊢
((⌊‘𝐴)
∈ ℝ → ((⌊‘𝐴) + 1) ∈ ℝ) |
| 11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℝ →
((⌊‘𝐴) + 1)
∈ ℝ) |
| 12 | 11 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) →
((⌊‘𝐴) + 1)
∈ ℝ) |
| 13 | | letr 11355 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧
((⌊‘𝐴) + 1)
∈ ℝ) → ((𝐵
≤ 𝐴 ∧ 𝐴 ≤ ((⌊‘𝐴) + 1)) → 𝐵 ≤ ((⌊‘𝐴) + 1))) |
| 14 | 12, 13 | mpd3an3 1464 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝐵 ≤ 𝐴 ∧ 𝐴 ≤ ((⌊‘𝐴) + 1)) → 𝐵 ≤ ((⌊‘𝐴) + 1))) |
| 15 | 8, 14 | mpan2d 694 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 → 𝐵 ≤ ((⌊‘𝐴) + 1))) |
| 16 | | leneg 11766 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℝ ∧
((⌊‘𝐴) + 1)
∈ ℝ) → (𝐵
≤ ((⌊‘𝐴) +
1) ↔ -((⌊‘𝐴) + 1) ≤ -𝐵)) |
| 17 | 11, 16 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ ((⌊‘𝐴) + 1) ↔
-((⌊‘𝐴) + 1)
≤ -𝐵)) |
| 18 | 15, 17 | sylibd 239 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 → -((⌊‘𝐴) + 1) ≤ -𝐵)) |
| 19 | 18 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ≤ 𝐴 → -((⌊‘𝐴) + 1) ≤ -𝐵)) |
| 20 | | ltneg 11763 |
. . . . . . . . . . . . . 14
⊢
(((⌊‘𝐴)
∈ ℝ ∧ 𝐵
∈ ℝ) → ((⌊‘𝐴) < 𝐵 ↔ -𝐵 < -(⌊‘𝐴))) |
| 21 | 9, 20 | sylan 580 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((⌊‘𝐴) <
𝐵 ↔ -𝐵 < -(⌊‘𝐴))) |
| 22 | 9 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℂ) |
| 23 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
| 24 | | negdi2 11567 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⌊‘𝐴)
∈ ℂ ∧ 1 ∈ ℂ) → -((⌊‘𝐴) + 1) = (-(⌊‘𝐴) − 1)) |
| 25 | 24 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢
(((⌊‘𝐴)
∈ ℂ ∧ 1 ∈ ℂ) → (-((⌊‘𝐴) + 1) + 1) =
((-(⌊‘𝐴)
− 1) + 1)) |
| 26 | | negcl 11508 |
. . . . . . . . . . . . . . . . . 18
⊢
((⌊‘𝐴)
∈ ℂ → -(⌊‘𝐴) ∈ ℂ) |
| 27 | | npcan 11517 |
. . . . . . . . . . . . . . . . . 18
⊢
((-(⌊‘𝐴)
∈ ℂ ∧ 1 ∈ ℂ) → ((-(⌊‘𝐴) − 1) + 1) =
-(⌊‘𝐴)) |
| 28 | 26, 27 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢
(((⌊‘𝐴)
∈ ℂ ∧ 1 ∈ ℂ) → ((-(⌊‘𝐴) − 1) + 1) =
-(⌊‘𝐴)) |
| 29 | 25, 28 | eqtr2d 2778 |
. . . . . . . . . . . . . . . 16
⊢
(((⌊‘𝐴)
∈ ℂ ∧ 1 ∈ ℂ) → -(⌊‘𝐴) = (-((⌊‘𝐴) + 1) + 1)) |
| 30 | 22, 23, 29 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ →
-(⌊‘𝐴) =
(-((⌊‘𝐴) + 1) +
1)) |
| 31 | 30 | breq2d 5155 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ → (-𝐵 < -(⌊‘𝐴) ↔ -𝐵 < (-((⌊‘𝐴) + 1) + 1))) |
| 32 | 31 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐵 < -(⌊‘𝐴) ↔ -𝐵 < (-((⌊‘𝐴) + 1) + 1))) |
| 33 | 21, 32 | bitrd 279 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((⌊‘𝐴) <
𝐵 ↔ -𝐵 < (-((⌊‘𝐴) + 1) + 1))) |
| 34 | 33 | biimpd 229 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((⌊‘𝐴) <
𝐵 → -𝐵 < (-((⌊‘𝐴) + 1) + 1))) |
| 35 | 19, 34 | anim12d 609 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐵 ≤ 𝐴 ∧ (⌊‘𝐴) < 𝐵) → (-((⌊‘𝐴) + 1) ≤ -𝐵 ∧ -𝐵 < (-((⌊‘𝐴) + 1) + 1)))) |
| 36 | 35 | ancomsd 465 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(((⌊‘𝐴) <
𝐵 ∧ 𝐵 ≤ 𝐴) → (-((⌊‘𝐴) + 1) ≤ -𝐵 ∧ -𝐵 < (-((⌊‘𝐴) + 1) + 1)))) |
| 37 | 36 | impl 455 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) <
𝐵) ∧ 𝐵 ≤ 𝐴) → (-((⌊‘𝐴) + 1) ≤ -𝐵 ∧ -𝐵 < (-((⌊‘𝐴) + 1) + 1))) |
| 38 | | flcl 13835 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℤ) |
| 39 | 38 | peano2zd 12725 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ →
((⌊‘𝐴) + 1)
∈ ℤ) |
| 40 | 39 | znegcld 12724 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ →
-((⌊‘𝐴) + 1)
∈ ℤ) |
| 41 | | rebtwnz 12989 |
. . . . . . . . . . 11
⊢ (-𝐵 ∈ ℝ →
∃!𝑥 ∈ ℤ
(𝑥 ≤ -𝐵 ∧ -𝐵 < (𝑥 + 1))) |
| 42 | 3, 41 | syl 17 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ →
∃!𝑥 ∈ ℤ
(𝑥 ≤ -𝐵 ∧ -𝐵 < (𝑥 + 1))) |
| 43 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝑥 = -((⌊‘𝐴) + 1) → (𝑥 ≤ -𝐵 ↔ -((⌊‘𝐴) + 1) ≤ -𝐵)) |
| 44 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝑥 = -((⌊‘𝐴) + 1) → (𝑥 + 1) = (-((⌊‘𝐴) + 1) + 1)) |
| 45 | 44 | breq2d 5155 |
. . . . . . . . . . . 12
⊢ (𝑥 = -((⌊‘𝐴) + 1) → (-𝐵 < (𝑥 + 1) ↔ -𝐵 < (-((⌊‘𝐴) + 1) + 1))) |
| 46 | 43, 45 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑥 = -((⌊‘𝐴) + 1) → ((𝑥 ≤ -𝐵 ∧ -𝐵 < (𝑥 + 1)) ↔ (-((⌊‘𝐴) + 1) ≤ -𝐵 ∧ -𝐵 < (-((⌊‘𝐴) + 1) + 1)))) |
| 47 | 46 | riota2 7413 |
. . . . . . . . . 10
⊢
((-((⌊‘𝐴) + 1) ∈ ℤ ∧ ∃!𝑥 ∈ ℤ (𝑥 ≤ -𝐵 ∧ -𝐵 < (𝑥 + 1))) → ((-((⌊‘𝐴) + 1) ≤ -𝐵 ∧ -𝐵 < (-((⌊‘𝐴) + 1) + 1)) ↔ (℩𝑥 ∈ ℤ (𝑥 ≤ -𝐵 ∧ -𝐵 < (𝑥 + 1))) = -((⌊‘𝐴) + 1))) |
| 48 | 40, 42, 47 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((-((⌊‘𝐴) + 1)
≤ -𝐵 ∧ -𝐵 < (-((⌊‘𝐴) + 1) + 1)) ↔
(℩𝑥 ∈
ℤ (𝑥 ≤ -𝐵 ∧ -𝐵 < (𝑥 + 1))) = -((⌊‘𝐴) + 1))) |
| 49 | 48 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) <
𝐵) ∧ 𝐵 ≤ 𝐴) → ((-((⌊‘𝐴) + 1) ≤ -𝐵 ∧ -𝐵 < (-((⌊‘𝐴) + 1) + 1)) ↔ (℩𝑥 ∈ ℤ (𝑥 ≤ -𝐵 ∧ -𝐵 < (𝑥 + 1))) = -((⌊‘𝐴) + 1))) |
| 50 | 37, 49 | mpbid 232 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) <
𝐵) ∧ 𝐵 ≤ 𝐴) → (℩𝑥 ∈ ℤ (𝑥 ≤ -𝐵 ∧ -𝐵 < (𝑥 + 1))) = -((⌊‘𝐴) + 1)) |
| 51 | 6, 50 | eqtrd 2777 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) <
𝐵) ∧ 𝐵 ≤ 𝐴) → (⌊‘-𝐵) = -((⌊‘𝐴) + 1)) |
| 52 | 38 | zcnd 12723 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℂ) |
| 53 | | peano2cn 11433 |
. . . . . . . . 9
⊢
((⌊‘𝐴)
∈ ℂ → ((⌊‘𝐴) + 1) ∈ ℂ) |
| 54 | 52, 53 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ →
((⌊‘𝐴) + 1)
∈ ℂ) |
| 55 | 3 | flcld 13838 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ →
(⌊‘-𝐵) ∈
ℤ) |
| 56 | 55 | zcnd 12723 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ →
(⌊‘-𝐵) ∈
ℂ) |
| 57 | | negcon2 11562 |
. . . . . . . 8
⊢
((((⌊‘𝐴)
+ 1) ∈ ℂ ∧ (⌊‘-𝐵) ∈ ℂ) →
(((⌊‘𝐴) + 1) =
-(⌊‘-𝐵) ↔
(⌊‘-𝐵) =
-((⌊‘𝐴) +
1))) |
| 58 | 54, 56, 57 | syl2an 596 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(((⌊‘𝐴) + 1) =
-(⌊‘-𝐵) ↔
(⌊‘-𝐵) =
-((⌊‘𝐴) +
1))) |
| 59 | 58 | ad2antrr 726 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) <
𝐵) ∧ 𝐵 ≤ 𝐴) → (((⌊‘𝐴) + 1) = -(⌊‘-𝐵) ↔ (⌊‘-𝐵) = -((⌊‘𝐴) + 1))) |
| 60 | 51, 59 | mpbird 257 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) <
𝐵) ∧ 𝐵 ≤ 𝐴) → ((⌊‘𝐴) + 1) = -(⌊‘-𝐵)) |
| 61 | 2, 60 | breqtrd 5169 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) <
𝐵) ∧ 𝐵 ≤ 𝐴) → 𝐴 < -(⌊‘-𝐵)) |
| 62 | 61 | ex 412 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) <
𝐵) → (𝐵 ≤ 𝐴 → 𝐴 < -(⌊‘-𝐵))) |
| 63 | | ltnle 11340 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
| 64 | | ceige 13884 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ → 𝐵 ≤ -(⌊‘-𝐵)) |
| 65 | 64 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ -(⌊‘-𝐵)) |
| 66 | | ceicl 13881 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ →
-(⌊‘-𝐵) ∈
ℤ) |
| 67 | 66 | zred 12722 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ →
-(⌊‘-𝐵) ∈
ℝ) |
| 68 | 67 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
-(⌊‘-𝐵) ∈
ℝ) |
| 69 | | ltletr 11353 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧
-(⌊‘-𝐵) ∈
ℝ) → ((𝐴 <
𝐵 ∧ 𝐵 ≤ -(⌊‘-𝐵)) → 𝐴 < -(⌊‘-𝐵))) |
| 70 | 68, 69 | mpd3an3 1464 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ -(⌊‘-𝐵)) → 𝐴 < -(⌊‘-𝐵))) |
| 71 | 65, 70 | mpan2d 694 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 < -(⌊‘-𝐵))) |
| 72 | 63, 71 | sylbird 260 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (¬
𝐵 ≤ 𝐴 → 𝐴 < -(⌊‘-𝐵))) |
| 73 | 72 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) <
𝐵) → (¬ 𝐵 ≤ 𝐴 → 𝐴 < -(⌊‘-𝐵))) |
| 74 | 62, 73 | pm2.61d 179 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) <
𝐵) → 𝐴 < -(⌊‘-𝐵)) |
| 75 | | flval 13834 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) =
(℩𝑥 ∈
ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1)))) |
| 76 | 75 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < -(⌊‘-𝐵)) ∧ 𝐵 ≤ 𝐴) → (⌊‘𝐴) = (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1)))) |
| 77 | | ceim1l 13887 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ →
(-(⌊‘-𝐵)
− 1) < 𝐵) |
| 78 | 77 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(-(⌊‘-𝐵)
− 1) < 𝐵) |
| 79 | | peano2rem 11576 |
. . . . . . . . . . . . . 14
⊢
(-(⌊‘-𝐵)
∈ ℝ → (-(⌊‘-𝐵) − 1) ∈
ℝ) |
| 80 | 67, 79 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℝ →
(-(⌊‘-𝐵)
− 1) ∈ ℝ) |
| 81 | 80 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(-(⌊‘-𝐵)
− 1) ∈ ℝ) |
| 82 | | ltleletr 11354 |
. . . . . . . . . . . . 13
⊢
(((-(⌊‘-𝐵) − 1) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) →
(((-(⌊‘-𝐵)
− 1) < 𝐵 ∧
𝐵 ≤ 𝐴) → (-(⌊‘-𝐵) − 1) ≤ 𝐴)) |
| 83 | 82 | 3com13 1125 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧
(-(⌊‘-𝐵)
− 1) ∈ ℝ) → (((-(⌊‘-𝐵) − 1) < 𝐵 ∧ 𝐵 ≤ 𝐴) → (-(⌊‘-𝐵) − 1) ≤ 𝐴)) |
| 84 | 81, 83 | mpd3an3 1464 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(((-(⌊‘-𝐵)
− 1) < 𝐵 ∧
𝐵 ≤ 𝐴) → (-(⌊‘-𝐵) − 1) ≤ 𝐴)) |
| 85 | 78, 84 | mpand 695 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ≤ 𝐴 → (-(⌊‘-𝐵) − 1) ≤ 𝐴)) |
| 86 | 66 | zcnd 12723 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ ℝ →
-(⌊‘-𝐵) ∈
ℂ) |
| 87 | | npcan 11517 |
. . . . . . . . . . . . . 14
⊢
((-(⌊‘-𝐵) ∈ ℂ ∧ 1 ∈ ℂ)
→ ((-(⌊‘-𝐵) − 1) + 1) = -(⌊‘-𝐵)) |
| 88 | 86, 23, 87 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℝ →
((-(⌊‘-𝐵)
− 1) + 1) = -(⌊‘-𝐵)) |
| 89 | 88 | breq2d 5155 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ → (𝐴 < ((-(⌊‘-𝐵) − 1) + 1) ↔ 𝐴 < -(⌊‘-𝐵))) |
| 90 | 89 | biimprd 248 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ → (𝐴 < -(⌊‘-𝐵) → 𝐴 < ((-(⌊‘-𝐵) − 1) + 1))) |
| 91 | 90 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < -(⌊‘-𝐵) → 𝐴 < ((-(⌊‘-𝐵) − 1) + 1))) |
| 92 | 85, 91 | anim12d 609 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐵 ≤ 𝐴 ∧ 𝐴 < -(⌊‘-𝐵)) → ((-(⌊‘-𝐵) − 1) ≤ 𝐴 ∧ 𝐴 < ((-(⌊‘-𝐵) − 1) + 1)))) |
| 93 | 92 | ancomsd 465 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 < -(⌊‘-𝐵) ∧ 𝐵 ≤ 𝐴) → ((-(⌊‘-𝐵) − 1) ≤ 𝐴 ∧ 𝐴 < ((-(⌊‘-𝐵) − 1) + 1)))) |
| 94 | 93 | impl 455 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < -(⌊‘-𝐵)) ∧ 𝐵 ≤ 𝐴) → ((-(⌊‘-𝐵) − 1) ≤ 𝐴 ∧ 𝐴 < ((-(⌊‘-𝐵) − 1) + 1))) |
| 95 | | peano2zm 12660 |
. . . . . . . . . 10
⊢
(-(⌊‘-𝐵)
∈ ℤ → (-(⌊‘-𝐵) − 1) ∈
ℤ) |
| 96 | 66, 95 | syl 17 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ →
(-(⌊‘-𝐵)
− 1) ∈ ℤ) |
| 97 | | rebtwnz 12989 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
∃!𝑥 ∈ ℤ
(𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) |
| 98 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑥 = (-(⌊‘-𝐵) − 1) → (𝑥 ≤ 𝐴 ↔ (-(⌊‘-𝐵) − 1) ≤ 𝐴)) |
| 99 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑥 = (-(⌊‘-𝐵) − 1) → (𝑥 + 1) = ((-(⌊‘-𝐵) − 1) +
1)) |
| 100 | 99 | breq2d 5155 |
. . . . . . . . . . 11
⊢ (𝑥 = (-(⌊‘-𝐵) − 1) → (𝐴 < (𝑥 + 1) ↔ 𝐴 < ((-(⌊‘-𝐵) − 1) + 1))) |
| 101 | 98, 100 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑥 = (-(⌊‘-𝐵) − 1) → ((𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1)) ↔ ((-(⌊‘-𝐵) − 1) ≤ 𝐴 ∧ 𝐴 < ((-(⌊‘-𝐵) − 1) + 1)))) |
| 102 | 101 | riota2 7413 |
. . . . . . . . 9
⊢
(((-(⌊‘-𝐵) − 1) ∈ ℤ ∧
∃!𝑥 ∈ ℤ
(𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) → (((-(⌊‘-𝐵) − 1) ≤ 𝐴 ∧ 𝐴 < ((-(⌊‘-𝐵) − 1) + 1)) ↔
(℩𝑥 ∈
ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) = (-(⌊‘-𝐵) − 1))) |
| 103 | 96, 97, 102 | syl2anr 597 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(((-(⌊‘-𝐵)
− 1) ≤ 𝐴 ∧
𝐴 <
((-(⌊‘-𝐵)
− 1) + 1)) ↔ (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) = (-(⌊‘-𝐵) − 1))) |
| 104 | 103 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < -(⌊‘-𝐵)) ∧ 𝐵 ≤ 𝐴) → (((-(⌊‘-𝐵) − 1) ≤ 𝐴 ∧ 𝐴 < ((-(⌊‘-𝐵) − 1) + 1)) ↔
(℩𝑥 ∈
ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) = (-(⌊‘-𝐵) − 1))) |
| 105 | 94, 104 | mpbid 232 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < -(⌊‘-𝐵)) ∧ 𝐵 ≤ 𝐴) → (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) = (-(⌊‘-𝐵) − 1)) |
| 106 | 76, 105 | eqtrd 2777 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < -(⌊‘-𝐵)) ∧ 𝐵 ≤ 𝐴) → (⌊‘𝐴) = (-(⌊‘-𝐵) − 1)) |
| 107 | 77 | ad3antlr 731 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < -(⌊‘-𝐵)) ∧ 𝐵 ≤ 𝐴) → (-(⌊‘-𝐵) − 1) < 𝐵) |
| 108 | 106, 107 | eqbrtrd 5165 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < -(⌊‘-𝐵)) ∧ 𝐵 ≤ 𝐴) → (⌊‘𝐴) < 𝐵) |
| 109 | 108 | ex 412 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < -(⌊‘-𝐵)) → (𝐵 ≤ 𝐴 → (⌊‘𝐴) < 𝐵)) |
| 110 | | flle 13839 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ≤
𝐴) |
| 111 | 110 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(⌊‘𝐴) ≤
𝐴) |
| 112 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(⌊‘𝐴) ∈
ℝ) |
| 113 | | lelttr 11351 |
. . . . . . . 8
⊢
(((⌊‘𝐴)
∈ ℝ ∧ 𝐴
∈ ℝ ∧ 𝐵
∈ ℝ) → (((⌊‘𝐴) ≤ 𝐴 ∧ 𝐴 < 𝐵) → (⌊‘𝐴) < 𝐵)) |
| 114 | 113 | 3coml 1128 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧
(⌊‘𝐴) ∈
ℝ) → (((⌊‘𝐴) ≤ 𝐴 ∧ 𝐴 < 𝐵) → (⌊‘𝐴) < 𝐵)) |
| 115 | 112, 114 | mpd3an3 1464 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(((⌊‘𝐴) ≤
𝐴 ∧ 𝐴 < 𝐵) → (⌊‘𝐴) < 𝐵)) |
| 116 | 111, 115 | mpand 695 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → (⌊‘𝐴) < 𝐵)) |
| 117 | 63, 116 | sylbird 260 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (¬
𝐵 ≤ 𝐴 → (⌊‘𝐴) < 𝐵)) |
| 118 | 117 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < -(⌊‘-𝐵)) → (¬ 𝐵 ≤ 𝐴 → (⌊‘𝐴) < 𝐵)) |
| 119 | 109, 118 | pm2.61d 179 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < -(⌊‘-𝐵)) → (⌊‘𝐴) < 𝐵) |
| 120 | 74, 119 | impbida 801 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((⌊‘𝐴) <
𝐵 ↔ 𝐴 < -(⌊‘-𝐵))) |