Proof of Theorem flqeqceilz
Step | Hyp | Ref
| Expression |
1 | | flid 9286 |
. . 3
⊢ (𝐴 ∈ ℤ →
(⌊‘𝐴) = 𝐴) |
2 | | ceilid 9317 |
. . 3
⊢ (𝐴 ∈ ℤ →
(⌈‘𝐴) = 𝐴) |
3 | 1, 2 | eqtr4d 2116 |
. 2
⊢ (𝐴 ∈ ℤ →
(⌊‘𝐴) =
(⌈‘𝐴)) |
4 | | flqcl 9277 |
. . . . . 6
⊢ (𝐴 ∈ ℚ →
(⌊‘𝐴) ∈
ℤ) |
5 | | zq 8711 |
. . . . . 6
⊢
((⌊‘𝐴)
∈ ℤ → (⌊‘𝐴) ∈ ℚ) |
6 | 4, 5 | syl 14 |
. . . . 5
⊢ (𝐴 ∈ ℚ →
(⌊‘𝐴) ∈
ℚ) |
7 | | qdceq 9256 |
. . . . 5
⊢
(((⌊‘𝐴)
∈ ℚ ∧ 𝐴
∈ ℚ) → DECID (⌊‘𝐴) = 𝐴) |
8 | 6, 7 | mpancom 413 |
. . . 4
⊢ (𝐴 ∈ ℚ →
DECID (⌊‘𝐴) = 𝐴) |
9 | | exmiddc 777 |
. . . 4
⊢
(DECID (⌊‘𝐴) = 𝐴 → ((⌊‘𝐴) = 𝐴 ∨ ¬ (⌊‘𝐴) = 𝐴)) |
10 | 8, 9 | syl 14 |
. . 3
⊢ (𝐴 ∈ ℚ →
((⌊‘𝐴) = 𝐴 ∨ ¬ (⌊‘𝐴) = 𝐴)) |
11 | | eqeq1 2087 |
. . . . . . 7
⊢
((⌊‘𝐴) =
𝐴 →
((⌊‘𝐴) =
(⌈‘𝐴) ↔
𝐴 = (⌈‘𝐴))) |
12 | 11 | adantr 270 |
. . . . . 6
⊢
(((⌊‘𝐴)
= 𝐴 ∧ 𝐴 ∈ ℚ) →
((⌊‘𝐴) =
(⌈‘𝐴) ↔
𝐴 = (⌈‘𝐴))) |
13 | | ceilqidz 9318 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℚ → (𝐴 ∈ ℤ ↔
(⌈‘𝐴) = 𝐴)) |
14 | | eqcom 2083 |
. . . . . . . . 9
⊢
((⌈‘𝐴) =
𝐴 ↔ 𝐴 = (⌈‘𝐴)) |
15 | 13, 14 | syl6bb 194 |
. . . . . . . 8
⊢ (𝐴 ∈ ℚ → (𝐴 ∈ ℤ ↔ 𝐴 = (⌈‘𝐴))) |
16 | 15 | biimprd 156 |
. . . . . . 7
⊢ (𝐴 ∈ ℚ → (𝐴 = (⌈‘𝐴) → 𝐴 ∈ ℤ)) |
17 | 16 | adantl 271 |
. . . . . 6
⊢
(((⌊‘𝐴)
= 𝐴 ∧ 𝐴 ∈ ℚ) → (𝐴 = (⌈‘𝐴) → 𝐴 ∈ ℤ)) |
18 | 12, 17 | sylbid 148 |
. . . . 5
⊢
(((⌊‘𝐴)
= 𝐴 ∧ 𝐴 ∈ ℚ) →
((⌊‘𝐴) =
(⌈‘𝐴) →
𝐴 ∈
ℤ)) |
19 | 18 | ex 113 |
. . . 4
⊢
((⌊‘𝐴) =
𝐴 → (𝐴 ∈ ℚ → ((⌊‘𝐴) = (⌈‘𝐴) → 𝐴 ∈ ℤ))) |
20 | | flqle 9280 |
. . . . 5
⊢ (𝐴 ∈ ℚ →
(⌊‘𝐴) ≤
𝐴) |
21 | | df-ne 2246 |
. . . . . 6
⊢
((⌊‘𝐴)
≠ 𝐴 ↔ ¬
(⌊‘𝐴) = 𝐴) |
22 | | necom 2329 |
. . . . . . 7
⊢
((⌊‘𝐴)
≠ 𝐴 ↔ 𝐴 ≠ (⌊‘𝐴)) |
23 | | qltlen 8725 |
. . . . . . . . . . 11
⊢
(((⌊‘𝐴)
∈ ℚ ∧ 𝐴
∈ ℚ) → ((⌊‘𝐴) < 𝐴 ↔ ((⌊‘𝐴) ≤ 𝐴 ∧ 𝐴 ≠ (⌊‘𝐴)))) |
24 | 6, 23 | mpancom 413 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℚ →
((⌊‘𝐴) <
𝐴 ↔
((⌊‘𝐴) ≤
𝐴 ∧ 𝐴 ≠ (⌊‘𝐴)))) |
25 | | breq1 3788 |
. . . . . . . . . . . . . 14
⊢
((⌊‘𝐴) =
(⌈‘𝐴) →
((⌊‘𝐴) <
𝐴 ↔
(⌈‘𝐴) <
𝐴)) |
26 | 25 | adantl 271 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℚ ∧
(⌊‘𝐴) =
(⌈‘𝐴)) →
((⌊‘𝐴) <
𝐴 ↔
(⌈‘𝐴) <
𝐴)) |
27 | | ceilqge 9312 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℚ → 𝐴 ≤ (⌈‘𝐴)) |
28 | | qre 8710 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℝ) |
29 | | ceilqcl 9310 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℚ →
(⌈‘𝐴) ∈
ℤ) |
30 | 29 | zred 8469 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℚ →
(⌈‘𝐴) ∈
ℝ) |
31 | 28, 30 | lenltd 7227 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℚ → (𝐴 ≤ (⌈‘𝐴) ↔ ¬
(⌈‘𝐴) <
𝐴)) |
32 | | pm2.21 579 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(⌈‘𝐴) <
𝐴 →
((⌈‘𝐴) <
𝐴 → 𝐴 ∈ ℤ)) |
33 | 31, 32 | syl6bi 161 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℚ → (𝐴 ≤ (⌈‘𝐴) → ((⌈‘𝐴) < 𝐴 → 𝐴 ∈ ℤ))) |
34 | 27, 33 | mpd 13 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℚ →
((⌈‘𝐴) <
𝐴 → 𝐴 ∈ ℤ)) |
35 | 34 | adantr 270 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℚ ∧
(⌊‘𝐴) =
(⌈‘𝐴)) →
((⌈‘𝐴) <
𝐴 → 𝐴 ∈ ℤ)) |
36 | 26, 35 | sylbid 148 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℚ ∧
(⌊‘𝐴) =
(⌈‘𝐴)) →
((⌊‘𝐴) <
𝐴 → 𝐴 ∈ ℤ)) |
37 | 36 | ex 113 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℚ →
((⌊‘𝐴) =
(⌈‘𝐴) →
((⌊‘𝐴) <
𝐴 → 𝐴 ∈ ℤ))) |
38 | 37 | com23 77 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℚ →
((⌊‘𝐴) <
𝐴 →
((⌊‘𝐴) =
(⌈‘𝐴) →
𝐴 ∈
ℤ))) |
39 | 24, 38 | sylbird 168 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℚ →
(((⌊‘𝐴) ≤
𝐴 ∧ 𝐴 ≠ (⌊‘𝐴)) → ((⌊‘𝐴) = (⌈‘𝐴) → 𝐴 ∈ ℤ))) |
40 | 39 | expd 254 |
. . . . . . . 8
⊢ (𝐴 ∈ ℚ →
((⌊‘𝐴) ≤
𝐴 → (𝐴 ≠ (⌊‘𝐴) → ((⌊‘𝐴) = (⌈‘𝐴) → 𝐴 ∈ ℤ)))) |
41 | 40 | com3r 78 |
. . . . . . 7
⊢ (𝐴 ≠ (⌊‘𝐴) → (𝐴 ∈ ℚ → ((⌊‘𝐴) ≤ 𝐴 → ((⌊‘𝐴) = (⌈‘𝐴) → 𝐴 ∈ ℤ)))) |
42 | 22, 41 | sylbi 119 |
. . . . . 6
⊢
((⌊‘𝐴)
≠ 𝐴 → (𝐴 ∈ ℚ →
((⌊‘𝐴) ≤
𝐴 →
((⌊‘𝐴) =
(⌈‘𝐴) →
𝐴 ∈
ℤ)))) |
43 | 21, 42 | sylbir 133 |
. . . . 5
⊢ (¬
(⌊‘𝐴) = 𝐴 → (𝐴 ∈ ℚ → ((⌊‘𝐴) ≤ 𝐴 → ((⌊‘𝐴) = (⌈‘𝐴) → 𝐴 ∈ ℤ)))) |
44 | 20, 43 | mpdi 42 |
. . . 4
⊢ (¬
(⌊‘𝐴) = 𝐴 → (𝐴 ∈ ℚ → ((⌊‘𝐴) = (⌈‘𝐴) → 𝐴 ∈ ℤ))) |
45 | 19, 44 | jaoi 668 |
. . 3
⊢
(((⌊‘𝐴)
= 𝐴 ∨ ¬
(⌊‘𝐴) = 𝐴) → (𝐴 ∈ ℚ → ((⌊‘𝐴) = (⌈‘𝐴) → 𝐴 ∈ ℤ))) |
46 | 10, 45 | mpcom 36 |
. 2
⊢ (𝐴 ∈ ℚ →
((⌊‘𝐴) =
(⌈‘𝐴) →
𝐴 ∈
ℤ)) |
47 | 3, 46 | impbid2 141 |
1
⊢ (𝐴 ∈ ℚ → (𝐴 ∈ ℤ ↔
(⌊‘𝐴) =
(⌈‘𝐴))) |