| Step | Hyp | Ref
| Expression |
| 1 | | flltp1 13840 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → 𝐴 < ((⌊‘𝐴) + 1)) |
| 2 | 1 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → 𝐴 < ((⌊‘𝐴) + 1)) |
| 3 | | flval 13834 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ →
(⌊‘𝐵) =
(℩𝑥 ∈
ℤ (𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1)))) |
| 4 | 3 | ad3antlr 731 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → (⌊‘𝐵) = (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1)))) |
| 5 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → (⌊‘𝐴) ≤ 𝐵) |
| 6 | 1 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 < ((⌊‘𝐴) + 1)) |
| 7 | | reflcl 13836 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
| 8 | | peano2re 11434 |
. . . . . . . . . . . . . . 15
⊢
((⌊‘𝐴)
∈ ℝ → ((⌊‘𝐴) + 1) ∈ ℝ) |
| 9 | 7, 8 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ →
((⌊‘𝐴) + 1)
∈ ℝ) |
| 10 | 9 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) →
((⌊‘𝐴) + 1)
∈ ℝ) |
| 11 | | lttr 11337 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧
((⌊‘𝐴) + 1)
∈ ℝ) → ((𝐵
< 𝐴 ∧ 𝐴 < ((⌊‘𝐴) + 1)) → 𝐵 < ((⌊‘𝐴) + 1))) |
| 12 | 10, 11 | mpd3an3 1464 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝐵 < 𝐴 ∧ 𝐴 < ((⌊‘𝐴) + 1)) → 𝐵 < ((⌊‘𝐴) + 1))) |
| 13 | 12 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐵 < 𝐴 ∧ 𝐴 < ((⌊‘𝐴) + 1)) → 𝐵 < ((⌊‘𝐴) + 1))) |
| 14 | 6, 13 | mpan2d 694 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 < 𝐴 → 𝐵 < ((⌊‘𝐴) + 1))) |
| 15 | 14 | imp 406 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → 𝐵 < ((⌊‘𝐴) + 1)) |
| 16 | 15 | adantlr 715 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → 𝐵 < ((⌊‘𝐴) + 1)) |
| 17 | | flcl 13835 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℤ) |
| 18 | | rebtwnz 12989 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ →
∃!𝑥 ∈ ℤ
(𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1))) |
| 19 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝑥 = (⌊‘𝐴) → (𝑥 ≤ 𝐵 ↔ (⌊‘𝐴) ≤ 𝐵)) |
| 20 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (⌊‘𝐴) → (𝑥 + 1) = ((⌊‘𝐴) + 1)) |
| 21 | 20 | breq2d 5155 |
. . . . . . . . . . . 12
⊢ (𝑥 = (⌊‘𝐴) → (𝐵 < (𝑥 + 1) ↔ 𝐵 < ((⌊‘𝐴) + 1))) |
| 22 | 19, 21 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑥 = (⌊‘𝐴) → ((𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1)) ↔ ((⌊‘𝐴) ≤ 𝐵 ∧ 𝐵 < ((⌊‘𝐴) + 1)))) |
| 23 | 22 | riota2 7413 |
. . . . . . . . . 10
⊢
(((⌊‘𝐴)
∈ ℤ ∧ ∃!𝑥 ∈ ℤ (𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1))) → (((⌊‘𝐴) ≤ 𝐵 ∧ 𝐵 < ((⌊‘𝐴) + 1)) ↔ (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1))) = (⌊‘𝐴))) |
| 24 | 17, 18, 23 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(((⌊‘𝐴) ≤
𝐵 ∧ 𝐵 < ((⌊‘𝐴) + 1)) ↔ (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1))) = (⌊‘𝐴))) |
| 25 | 24 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → (((⌊‘𝐴) ≤ 𝐵 ∧ 𝐵 < ((⌊‘𝐴) + 1)) ↔ (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1))) = (⌊‘𝐴))) |
| 26 | 5, 16, 25 | mpbi2and 712 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1))) = (⌊‘𝐴)) |
| 27 | 4, 26 | eqtrd 2777 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → (⌊‘𝐵) = (⌊‘𝐴)) |
| 28 | 27 | oveq1d 7446 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → ((⌊‘𝐵) + 1) = ((⌊‘𝐴) + 1)) |
| 29 | 2, 28 | breqtrrd 5171 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → 𝐴 < ((⌊‘𝐵) + 1)) |
| 30 | 29 | ex 412 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) → (𝐵 < 𝐴 → 𝐴 < ((⌊‘𝐵) + 1))) |
| 31 | | lenlt 11339 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
| 32 | | flltp1 13840 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ → 𝐵 < ((⌊‘𝐵) + 1)) |
| 33 | 32 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 < ((⌊‘𝐵) + 1)) |
| 34 | | reflcl 13836 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ →
(⌊‘𝐵) ∈
ℝ) |
| 35 | | peano2re 11434 |
. . . . . . . . 9
⊢
((⌊‘𝐵)
∈ ℝ → ((⌊‘𝐵) + 1) ∈ ℝ) |
| 36 | 34, 35 | syl 17 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ →
((⌊‘𝐵) + 1)
∈ ℝ) |
| 37 | 36 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((⌊‘𝐵) + 1)
∈ ℝ) |
| 38 | | lelttr 11351 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧
((⌊‘𝐵) + 1)
∈ ℝ) → ((𝐴
≤ 𝐵 ∧ 𝐵 < ((⌊‘𝐵) + 1)) → 𝐴 < ((⌊‘𝐵) + 1))) |
| 39 | 37, 38 | mpd3an3 1464 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < ((⌊‘𝐵) + 1)) → 𝐴 < ((⌊‘𝐵) + 1))) |
| 40 | 33, 39 | mpan2d 694 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 → 𝐴 < ((⌊‘𝐵) + 1))) |
| 41 | 31, 40 | sylbird 260 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (¬
𝐵 < 𝐴 → 𝐴 < ((⌊‘𝐵) + 1))) |
| 42 | 41 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) → (¬ 𝐵 < 𝐴 → 𝐴 < ((⌊‘𝐵) + 1))) |
| 43 | 30, 42 | pm2.61d 179 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) → 𝐴 < ((⌊‘𝐵) + 1)) |
| 44 | | flval 13834 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) =
(℩𝑥 ∈
ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1)))) |
| 45 | 44 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) ∧ 𝐵 < 𝐴) → (⌊‘𝐴) = (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1)))) |
| 46 | 34 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → (⌊‘𝐵) ∈ ℝ) |
| 47 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → 𝐴 ∈ ℝ) |
| 48 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → 𝐵 ∈ ℝ) |
| 49 | | flle 13839 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ →
(⌊‘𝐵) ≤
𝐵) |
| 50 | 49 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → (⌊‘𝐵) ≤ 𝐵) |
| 51 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → 𝐵 < 𝐴) |
| 52 | 46, 48, 47, 50, 51 | lelttrd 11419 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → (⌊‘𝐵) < 𝐴) |
| 53 | 46, 47, 52 | ltled 11409 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → (⌊‘𝐵) ≤ 𝐴) |
| 54 | 53 | adantlr 715 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) ∧ 𝐵 < 𝐴) → (⌊‘𝐵) ≤ 𝐴) |
| 55 | | simplr 769 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) ∧ 𝐵 < 𝐴) → 𝐴 < ((⌊‘𝐵) + 1)) |
| 56 | | flcl 13835 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ →
(⌊‘𝐵) ∈
ℤ) |
| 57 | | rebtwnz 12989 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
∃!𝑥 ∈ ℤ
(𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) |
| 58 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑥 = (⌊‘𝐵) → (𝑥 ≤ 𝐴 ↔ (⌊‘𝐵) ≤ 𝐴)) |
| 59 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑥 = (⌊‘𝐵) → (𝑥 + 1) = ((⌊‘𝐵) + 1)) |
| 60 | 59 | breq2d 5155 |
. . . . . . . . . . 11
⊢ (𝑥 = (⌊‘𝐵) → (𝐴 < (𝑥 + 1) ↔ 𝐴 < ((⌊‘𝐵) + 1))) |
| 61 | 58, 60 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑥 = (⌊‘𝐵) → ((𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1)) ↔ ((⌊‘𝐵) ≤ 𝐴 ∧ 𝐴 < ((⌊‘𝐵) + 1)))) |
| 62 | 61 | riota2 7413 |
. . . . . . . . 9
⊢
(((⌊‘𝐵)
∈ ℤ ∧ ∃!𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) → (((⌊‘𝐵) ≤ 𝐴 ∧ 𝐴 < ((⌊‘𝐵) + 1)) ↔ (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) = (⌊‘𝐵))) |
| 63 | 56, 57, 62 | syl2anr 597 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(((⌊‘𝐵) ≤
𝐴 ∧ 𝐴 < ((⌊‘𝐵) + 1)) ↔ (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) = (⌊‘𝐵))) |
| 64 | 63 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) ∧ 𝐵 < 𝐴) → (((⌊‘𝐵) ≤ 𝐴 ∧ 𝐴 < ((⌊‘𝐵) + 1)) ↔ (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) = (⌊‘𝐵))) |
| 65 | 54, 55, 64 | mpbi2and 712 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) ∧ 𝐵 < 𝐴) → (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) = (⌊‘𝐵)) |
| 66 | 45, 65 | eqtrd 2777 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) ∧ 𝐵 < 𝐴) → (⌊‘𝐴) = (⌊‘𝐵)) |
| 67 | 49 | ad3antlr 731 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) ∧ 𝐵 < 𝐴) → (⌊‘𝐵) ≤ 𝐵) |
| 68 | 66, 67 | eqbrtrd 5165 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) ∧ 𝐵 < 𝐴) → (⌊‘𝐴) ≤ 𝐵) |
| 69 | 68 | ex 412 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) → (𝐵 < 𝐴 → (⌊‘𝐴) ≤ 𝐵)) |
| 70 | | flle 13839 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ≤
𝐴) |
| 71 | 70 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(⌊‘𝐴) ≤
𝐴) |
| 72 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(⌊‘𝐴) ∈
ℝ) |
| 73 | | letr 11355 |
. . . . . . . 8
⊢
(((⌊‘𝐴)
∈ ℝ ∧ 𝐴
∈ ℝ ∧ 𝐵
∈ ℝ) → (((⌊‘𝐴) ≤ 𝐴 ∧ 𝐴 ≤ 𝐵) → (⌊‘𝐴) ≤ 𝐵)) |
| 74 | 73 | 3coml 1128 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧
(⌊‘𝐴) ∈
ℝ) → (((⌊‘𝐴) ≤ 𝐴 ∧ 𝐴 ≤ 𝐵) → (⌊‘𝐴) ≤ 𝐵)) |
| 75 | 72, 74 | mpd3an3 1464 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(((⌊‘𝐴) ≤
𝐴 ∧ 𝐴 ≤ 𝐵) → (⌊‘𝐴) ≤ 𝐵)) |
| 76 | 71, 75 | mpand 695 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 → (⌊‘𝐴) ≤ 𝐵)) |
| 77 | 31, 76 | sylbird 260 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (¬
𝐵 < 𝐴 → (⌊‘𝐴) ≤ 𝐵)) |
| 78 | 77 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) → (¬ 𝐵 < 𝐴 → (⌊‘𝐴) ≤ 𝐵)) |
| 79 | 69, 78 | pm2.61d 179 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) →
(⌊‘𝐴) ≤
𝐵) |
| 80 | 43, 79 | impbida 801 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((⌊‘𝐴) ≤
𝐵 ↔ 𝐴 < ((⌊‘𝐵) + 1))) |