Step | Hyp | Ref
| Expression |
1 | | elin 3155 |
. . . . . . 7
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) ↔ (𝑘 ∈ (0...𝑁) ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1)))) |
2 | 1 | simprbi 269 |
. . . . . 6
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈
(ℤ≥‘(𝑁 + 1))) |
3 | | eluzle 8631 |
. . . . . 6
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → (𝑁 + 1) ≤ 𝑘) |
4 | 2, 3 | syl 14 |
. . . . 5
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → (𝑁 + 1) ≤ 𝑘) |
5 | | eluzel2 8624 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → (𝑁 + 1) ∈ ℤ) |
6 | 2, 5 | syl 14 |
. . . . . 6
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → (𝑁 + 1) ∈
ℤ) |
7 | | eluzelz 8628 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → 𝑘 ∈ ℤ) |
8 | 2, 7 | syl 14 |
. . . . . 6
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈
ℤ) |
9 | | zlem1lt 8407 |
. . . . . 6
⊢ (((𝑁 + 1) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑁 + 1) ≤ 𝑘 ↔ ((𝑁 + 1) − 1) < 𝑘)) |
10 | 6, 8, 9 | syl2anc 403 |
. . . . 5
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → ((𝑁 + 1) ≤ 𝑘 ↔ ((𝑁 + 1) − 1) < 𝑘)) |
11 | 4, 10 | mpbid 145 |
. . . 4
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → ((𝑁 + 1) − 1) < 𝑘) |
12 | 1 | simplbi 268 |
. . . . . 6
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈ (0...𝑁)) |
13 | | elfzle2 9047 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ≤ 𝑁) |
14 | 12, 13 | syl 14 |
. . . . 5
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑘 ≤ 𝑁) |
15 | 8 | zred 8469 |
. . . . . . 7
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈
ℝ) |
16 | | elfzel2 9043 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑁) → 𝑁 ∈ ℤ) |
17 | 16 | adantr 270 |
. . . . . . . . 9
⊢ ((𝑘 ∈ (0...𝑁) ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ ℤ) |
18 | 1, 17 | sylbi 119 |
. . . . . . . 8
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ ℤ) |
19 | 18 | zred 8469 |
. . . . . . 7
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ ℝ) |
20 | 15, 19 | lenltd 7227 |
. . . . . 6
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → (𝑘 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑘)) |
21 | 18 | zcnd 8470 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ ℂ) |
22 | | pncan1 7481 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
23 | 21, 22 | syl 14 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → ((𝑁 + 1) − 1) = 𝑁) |
24 | 23 | eqcomd 2086 |
. . . . . . . 8
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑁 = ((𝑁 + 1) − 1)) |
25 | 24 | breq1d 3795 |
. . . . . . 7
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → (𝑁 < 𝑘 ↔ ((𝑁 + 1) − 1) < 𝑘)) |
26 | 25 | notbid 624 |
. . . . . 6
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → (¬ 𝑁 < 𝑘 ↔ ¬ ((𝑁 + 1) − 1) < 𝑘)) |
27 | 20, 26 | bitrd 186 |
. . . . 5
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → (𝑘 ≤ 𝑁 ↔ ¬ ((𝑁 + 1) − 1) < 𝑘)) |
28 | 14, 27 | mpbid 145 |
. . . 4
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → ¬ ((𝑁 + 1) − 1) < 𝑘) |
29 | 11, 28 | pm2.21dd 582 |
. . 3
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈
∅) |
30 | 29 | ssriv 3003 |
. 2
⊢
((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) ⊆ ∅ |
31 | | ss0 3284 |
. 2
⊢
(((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) ⊆ ∅ → ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) = ∅) |
32 | 30, 31 | ax-mp 7 |
1
⊢
((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) = ∅ |