Proof of Theorem fleqceilz
| Step | Hyp | Ref
| Expression |
| 1 | | flid 13848 |
. . 3
⊢ (𝐴 ∈ ℤ →
(⌊‘𝐴) = 𝐴) |
| 2 | | ceilid 13891 |
. . 3
⊢ (𝐴 ∈ ℤ →
(⌈‘𝐴) = 𝐴) |
| 3 | 1, 2 | eqtr4d 2780 |
. 2
⊢ (𝐴 ∈ ℤ →
(⌊‘𝐴) =
(⌈‘𝐴)) |
| 4 | | eqeq1 2741 |
. . . . . 6
⊢
((⌊‘𝐴) =
𝐴 →
((⌊‘𝐴) =
(⌈‘𝐴) ↔
𝐴 = (⌈‘𝐴))) |
| 5 | 4 | adantr 480 |
. . . . 5
⊢
(((⌊‘𝐴)
= 𝐴 ∧ 𝐴 ∈ ℝ) →
((⌊‘𝐴) =
(⌈‘𝐴) ↔
𝐴 = (⌈‘𝐴))) |
| 6 | | ceilidz 13892 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℤ ↔
(⌈‘𝐴) = 𝐴)) |
| 7 | | eqcom 2744 |
. . . . . . . 8
⊢
((⌈‘𝐴) =
𝐴 ↔ 𝐴 = (⌈‘𝐴)) |
| 8 | 6, 7 | bitrdi 287 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℤ ↔ 𝐴 = (⌈‘𝐴))) |
| 9 | 8 | biimprd 248 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (𝐴 = (⌈‘𝐴) → 𝐴 ∈ ℤ)) |
| 10 | 9 | adantl 481 |
. . . . 5
⊢
(((⌊‘𝐴)
= 𝐴 ∧ 𝐴 ∈ ℝ) → (𝐴 = (⌈‘𝐴) → 𝐴 ∈ ℤ)) |
| 11 | 5, 10 | sylbid 240 |
. . . 4
⊢
(((⌊‘𝐴)
= 𝐴 ∧ 𝐴 ∈ ℝ) →
((⌊‘𝐴) =
(⌈‘𝐴) →
𝐴 ∈
ℤ)) |
| 12 | 11 | ex 412 |
. . 3
⊢
((⌊‘𝐴) =
𝐴 → (𝐴 ∈ ℝ → ((⌊‘𝐴) = (⌈‘𝐴) → 𝐴 ∈ ℤ))) |
| 13 | | flle 13839 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ≤
𝐴) |
| 14 | | df-ne 2941 |
. . . . 5
⊢
((⌊‘𝐴)
≠ 𝐴 ↔ ¬
(⌊‘𝐴) = 𝐴) |
| 15 | | necom 2994 |
. . . . . 6
⊢
((⌊‘𝐴)
≠ 𝐴 ↔ 𝐴 ≠ (⌊‘𝐴)) |
| 16 | | reflcl 13836 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
| 17 | | id 22 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ) |
| 18 | 16, 17 | ltlend 11406 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
((⌊‘𝐴) <
𝐴 ↔
((⌊‘𝐴) ≤
𝐴 ∧ 𝐴 ≠ (⌊‘𝐴)))) |
| 19 | | breq1 5146 |
. . . . . . . . . . . . 13
⊢
((⌊‘𝐴) =
(⌈‘𝐴) →
((⌊‘𝐴) <
𝐴 ↔
(⌈‘𝐴) <
𝐴)) |
| 20 | 19 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) =
(⌈‘𝐴)) →
((⌊‘𝐴) <
𝐴 ↔
(⌈‘𝐴) <
𝐴)) |
| 21 | | ceilge 13885 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (⌈‘𝐴)) |
| 22 | | ceilcl 13882 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℝ →
(⌈‘𝐴) ∈
ℤ) |
| 23 | 22 | zred 12722 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℝ →
(⌈‘𝐴) ∈
ℝ) |
| 24 | 17, 23 | lenltd 11407 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ → (𝐴 ≤ (⌈‘𝐴) ↔ ¬
(⌈‘𝐴) <
𝐴)) |
| 25 | | pm2.21 123 |
. . . . . . . . . . . . . . 15
⊢ (¬
(⌈‘𝐴) <
𝐴 →
((⌈‘𝐴) <
𝐴 → 𝐴 ∈ ℤ)) |
| 26 | 24, 25 | biimtrdi 253 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ → (𝐴 ≤ (⌈‘𝐴) → ((⌈‘𝐴) < 𝐴 → 𝐴 ∈ ℤ))) |
| 27 | 21, 26 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ →
((⌈‘𝐴) <
𝐴 → 𝐴 ∈ ℤ)) |
| 28 | 27 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) =
(⌈‘𝐴)) →
((⌈‘𝐴) <
𝐴 → 𝐴 ∈ ℤ)) |
| 29 | 20, 28 | sylbid 240 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) =
(⌈‘𝐴)) →
((⌊‘𝐴) <
𝐴 → 𝐴 ∈ ℤ)) |
| 30 | 29 | ex 412 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ →
((⌊‘𝐴) =
(⌈‘𝐴) →
((⌊‘𝐴) <
𝐴 → 𝐴 ∈ ℤ))) |
| 31 | 30 | com23 86 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
((⌊‘𝐴) <
𝐴 →
((⌊‘𝐴) =
(⌈‘𝐴) →
𝐴 ∈
ℤ))) |
| 32 | 18, 31 | sylbird 260 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ →
(((⌊‘𝐴) ≤
𝐴 ∧ 𝐴 ≠ (⌊‘𝐴)) → ((⌊‘𝐴) = (⌈‘𝐴) → 𝐴 ∈ ℤ))) |
| 33 | 32 | expd 415 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
((⌊‘𝐴) ≤
𝐴 → (𝐴 ≠ (⌊‘𝐴) → ((⌊‘𝐴) = (⌈‘𝐴) → 𝐴 ∈ ℤ)))) |
| 34 | 33 | com3r 87 |
. . . . . 6
⊢ (𝐴 ≠ (⌊‘𝐴) → (𝐴 ∈ ℝ → ((⌊‘𝐴) ≤ 𝐴 → ((⌊‘𝐴) = (⌈‘𝐴) → 𝐴 ∈ ℤ)))) |
| 35 | 15, 34 | sylbi 217 |
. . . . 5
⊢
((⌊‘𝐴)
≠ 𝐴 → (𝐴 ∈ ℝ →
((⌊‘𝐴) ≤
𝐴 →
((⌊‘𝐴) =
(⌈‘𝐴) →
𝐴 ∈
ℤ)))) |
| 36 | 14, 35 | sylbir 235 |
. . . 4
⊢ (¬
(⌊‘𝐴) = 𝐴 → (𝐴 ∈ ℝ → ((⌊‘𝐴) ≤ 𝐴 → ((⌊‘𝐴) = (⌈‘𝐴) → 𝐴 ∈ ℤ)))) |
| 37 | 13, 36 | mpdi 45 |
. . 3
⊢ (¬
(⌊‘𝐴) = 𝐴 → (𝐴 ∈ ℝ → ((⌊‘𝐴) = (⌈‘𝐴) → 𝐴 ∈ ℤ))) |
| 38 | 12, 37 | pm2.61i 182 |
. 2
⊢ (𝐴 ∈ ℝ →
((⌊‘𝐴) =
(⌈‘𝐴) →
𝐴 ∈
ℤ)) |
| 39 | 3, 38 | impbid2 226 |
1
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℤ ↔
(⌊‘𝐴) =
(⌈‘𝐴))) |