Step | Hyp | Ref
| Expression |
1 | | flltp1 13400 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → 𝐴 < ((⌊‘𝐴) + 1)) |
2 | 1 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → 𝐴 < ((⌊‘𝐴) + 1)) |
3 | | flval 13394 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ →
(⌊‘𝐵) =
(℩𝑥 ∈
ℤ (𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1)))) |
4 | 3 | ad3antlr 731 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → (⌊‘𝐵) = (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1)))) |
5 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → (⌊‘𝐴) ≤ 𝐵) |
6 | 1 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 < ((⌊‘𝐴) + 1)) |
7 | | reflcl 13396 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
8 | | peano2re 11030 |
. . . . . . . . . . . . . . 15
⊢
((⌊‘𝐴)
∈ ℝ → ((⌊‘𝐴) + 1) ∈ ℝ) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ →
((⌊‘𝐴) + 1)
∈ ℝ) |
10 | 9 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) →
((⌊‘𝐴) + 1)
∈ ℝ) |
11 | | lttr 10934 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧
((⌊‘𝐴) + 1)
∈ ℝ) → ((𝐵
< 𝐴 ∧ 𝐴 < ((⌊‘𝐴) + 1)) → 𝐵 < ((⌊‘𝐴) + 1))) |
12 | 10, 11 | mpd3an3 1464 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝐵 < 𝐴 ∧ 𝐴 < ((⌊‘𝐴) + 1)) → 𝐵 < ((⌊‘𝐴) + 1))) |
13 | 12 | ancoms 462 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐵 < 𝐴 ∧ 𝐴 < ((⌊‘𝐴) + 1)) → 𝐵 < ((⌊‘𝐴) + 1))) |
14 | 6, 13 | mpan2d 694 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 < 𝐴 → 𝐵 < ((⌊‘𝐴) + 1))) |
15 | 14 | imp 410 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → 𝐵 < ((⌊‘𝐴) + 1)) |
16 | 15 | adantlr 715 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → 𝐵 < ((⌊‘𝐴) + 1)) |
17 | | flcl 13395 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℤ) |
18 | | rebtwnz 12568 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ →
∃!𝑥 ∈ ℤ
(𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1))) |
19 | | breq1 5071 |
. . . . . . . . . . . 12
⊢ (𝑥 = (⌊‘𝐴) → (𝑥 ≤ 𝐵 ↔ (⌊‘𝐴) ≤ 𝐵)) |
20 | | oveq1 7239 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (⌊‘𝐴) → (𝑥 + 1) = ((⌊‘𝐴) + 1)) |
21 | 20 | breq2d 5080 |
. . . . . . . . . . . 12
⊢ (𝑥 = (⌊‘𝐴) → (𝐵 < (𝑥 + 1) ↔ 𝐵 < ((⌊‘𝐴) + 1))) |
22 | 19, 21 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑥 = (⌊‘𝐴) → ((𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1)) ↔ ((⌊‘𝐴) ≤ 𝐵 ∧ 𝐵 < ((⌊‘𝐴) + 1)))) |
23 | 22 | riota2 7215 |
. . . . . . . . . 10
⊢
(((⌊‘𝐴)
∈ ℤ ∧ ∃!𝑥 ∈ ℤ (𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1))) → (((⌊‘𝐴) ≤ 𝐵 ∧ 𝐵 < ((⌊‘𝐴) + 1)) ↔ (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1))) = (⌊‘𝐴))) |
24 | 17, 18, 23 | syl2an 599 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(((⌊‘𝐴) ≤
𝐵 ∧ 𝐵 < ((⌊‘𝐴) + 1)) ↔ (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1))) = (⌊‘𝐴))) |
25 | 24 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → (((⌊‘𝐴) ≤ 𝐵 ∧ 𝐵 < ((⌊‘𝐴) + 1)) ↔ (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1))) = (⌊‘𝐴))) |
26 | 5, 16, 25 | mpbi2and 712 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐵 ∧ 𝐵 < (𝑥 + 1))) = (⌊‘𝐴)) |
27 | 4, 26 | eqtrd 2778 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → (⌊‘𝐵) = (⌊‘𝐴)) |
28 | 27 | oveq1d 7247 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → ((⌊‘𝐵) + 1) = ((⌊‘𝐴) + 1)) |
29 | 2, 28 | breqtrrd 5096 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) ∧ 𝐵 < 𝐴) → 𝐴 < ((⌊‘𝐵) + 1)) |
30 | 29 | ex 416 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) → (𝐵 < 𝐴 → 𝐴 < ((⌊‘𝐵) + 1))) |
31 | | lenlt 10936 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
32 | | flltp1 13400 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ → 𝐵 < ((⌊‘𝐵) + 1)) |
33 | 32 | adantl 485 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 < ((⌊‘𝐵) + 1)) |
34 | | reflcl 13396 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ →
(⌊‘𝐵) ∈
ℝ) |
35 | | peano2re 11030 |
. . . . . . . . 9
⊢
((⌊‘𝐵)
∈ ℝ → ((⌊‘𝐵) + 1) ∈ ℝ) |
36 | 34, 35 | syl 17 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ →
((⌊‘𝐵) + 1)
∈ ℝ) |
37 | 36 | adantl 485 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((⌊‘𝐵) + 1)
∈ ℝ) |
38 | | lelttr 10948 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧
((⌊‘𝐵) + 1)
∈ ℝ) → ((𝐴
≤ 𝐵 ∧ 𝐵 < ((⌊‘𝐵) + 1)) → 𝐴 < ((⌊‘𝐵) + 1))) |
39 | 37, 38 | mpd3an3 1464 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < ((⌊‘𝐵) + 1)) → 𝐴 < ((⌊‘𝐵) + 1))) |
40 | 33, 39 | mpan2d 694 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 → 𝐴 < ((⌊‘𝐵) + 1))) |
41 | 31, 40 | sylbird 263 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (¬
𝐵 < 𝐴 → 𝐴 < ((⌊‘𝐵) + 1))) |
42 | 41 | adantr 484 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) → (¬ 𝐵 < 𝐴 → 𝐴 < ((⌊‘𝐵) + 1))) |
43 | 30, 42 | pm2.61d 182 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(⌊‘𝐴) ≤
𝐵) → 𝐴 < ((⌊‘𝐵) + 1)) |
44 | | flval 13394 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) =
(℩𝑥 ∈
ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1)))) |
45 | 44 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) ∧ 𝐵 < 𝐴) → (⌊‘𝐴) = (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1)))) |
46 | 34 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → (⌊‘𝐵) ∈ ℝ) |
47 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → 𝐴 ∈ ℝ) |
48 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → 𝐵 ∈ ℝ) |
49 | | flle 13399 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ →
(⌊‘𝐵) ≤
𝐵) |
50 | 49 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → (⌊‘𝐵) ≤ 𝐵) |
51 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → 𝐵 < 𝐴) |
52 | 46, 48, 47, 50, 51 | lelttrd 11015 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → (⌊‘𝐵) < 𝐴) |
53 | 46, 47, 52 | ltled 11005 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → (⌊‘𝐵) ≤ 𝐴) |
54 | 53 | adantlr 715 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) ∧ 𝐵 < 𝐴) → (⌊‘𝐵) ≤ 𝐴) |
55 | | simplr 769 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) ∧ 𝐵 < 𝐴) → 𝐴 < ((⌊‘𝐵) + 1)) |
56 | | flcl 13395 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ →
(⌊‘𝐵) ∈
ℤ) |
57 | | rebtwnz 12568 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
∃!𝑥 ∈ ℤ
(𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) |
58 | | breq1 5071 |
. . . . . . . . . . 11
⊢ (𝑥 = (⌊‘𝐵) → (𝑥 ≤ 𝐴 ↔ (⌊‘𝐵) ≤ 𝐴)) |
59 | | oveq1 7239 |
. . . . . . . . . . . 12
⊢ (𝑥 = (⌊‘𝐵) → (𝑥 + 1) = ((⌊‘𝐵) + 1)) |
60 | 59 | breq2d 5080 |
. . . . . . . . . . 11
⊢ (𝑥 = (⌊‘𝐵) → (𝐴 < (𝑥 + 1) ↔ 𝐴 < ((⌊‘𝐵) + 1))) |
61 | 58, 60 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑥 = (⌊‘𝐵) → ((𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1)) ↔ ((⌊‘𝐵) ≤ 𝐴 ∧ 𝐴 < ((⌊‘𝐵) + 1)))) |
62 | 61 | riota2 7215 |
. . . . . . . . 9
⊢
(((⌊‘𝐵)
∈ ℤ ∧ ∃!𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) → (((⌊‘𝐵) ≤ 𝐴 ∧ 𝐴 < ((⌊‘𝐵) + 1)) ↔ (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) = (⌊‘𝐵))) |
63 | 56, 57, 62 | syl2anr 600 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(((⌊‘𝐵) ≤
𝐴 ∧ 𝐴 < ((⌊‘𝐵) + 1)) ↔ (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) = (⌊‘𝐵))) |
64 | 63 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) ∧ 𝐵 < 𝐴) → (((⌊‘𝐵) ≤ 𝐴 ∧ 𝐴 < ((⌊‘𝐵) + 1)) ↔ (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) = (⌊‘𝐵))) |
65 | 54, 55, 64 | mpbi2and 712 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) ∧ 𝐵 < 𝐴) → (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) = (⌊‘𝐵)) |
66 | 45, 65 | eqtrd 2778 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) ∧ 𝐵 < 𝐴) → (⌊‘𝐴) = (⌊‘𝐵)) |
67 | 49 | ad3antlr 731 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) ∧ 𝐵 < 𝐴) → (⌊‘𝐵) ≤ 𝐵) |
68 | 66, 67 | eqbrtrd 5090 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) ∧ 𝐵 < 𝐴) → (⌊‘𝐴) ≤ 𝐵) |
69 | 68 | ex 416 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) → (𝐵 < 𝐴 → (⌊‘𝐴) ≤ 𝐵)) |
70 | | flle 13399 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ≤
𝐴) |
71 | 70 | adantr 484 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(⌊‘𝐴) ≤
𝐴) |
72 | 7 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(⌊‘𝐴) ∈
ℝ) |
73 | | letr 10951 |
. . . . . . . 8
⊢
(((⌊‘𝐴)
∈ ℝ ∧ 𝐴
∈ ℝ ∧ 𝐵
∈ ℝ) → (((⌊‘𝐴) ≤ 𝐴 ∧ 𝐴 ≤ 𝐵) → (⌊‘𝐴) ≤ 𝐵)) |
74 | 73 | 3coml 1129 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧
(⌊‘𝐴) ∈
ℝ) → (((⌊‘𝐴) ≤ 𝐴 ∧ 𝐴 ≤ 𝐵) → (⌊‘𝐴) ≤ 𝐵)) |
75 | 72, 74 | mpd3an3 1464 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(((⌊‘𝐴) ≤
𝐴 ∧ 𝐴 ≤ 𝐵) → (⌊‘𝐴) ≤ 𝐵)) |
76 | 71, 75 | mpand 695 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 → (⌊‘𝐴) ≤ 𝐵)) |
77 | 31, 76 | sylbird 263 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (¬
𝐵 < 𝐴 → (⌊‘𝐴) ≤ 𝐵)) |
78 | 77 | adantr 484 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) → (¬ 𝐵 < 𝐴 → (⌊‘𝐴) ≤ 𝐵)) |
79 | 69, 78 | pm2.61d 182 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < ((⌊‘𝐵) + 1)) →
(⌊‘𝐴) ≤
𝐵) |
80 | 43, 79 | impbida 801 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((⌊‘𝐴) ≤
𝐵 ↔ 𝐴 < ((⌊‘𝐵) + 1))) |