Step | Hyp | Ref
| Expression |
1 | | elin 3290 |
. . . . . . 7
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) ↔ (𝑘 ∈ (0...𝑁) ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1)))) |
2 | 1 | simprbi 273 |
. . . . . 6
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈
(ℤ≥‘(𝑁 + 1))) |
3 | | eluzle 9452 |
. . . . . 6
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → (𝑁 + 1) ≤ 𝑘) |
4 | 2, 3 | syl 14 |
. . . . 5
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → (𝑁 + 1) ≤ 𝑘) |
5 | | eluzel2 9445 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → (𝑁 + 1) ∈ ℤ) |
6 | 2, 5 | syl 14 |
. . . . . 6
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → (𝑁 + 1) ∈
ℤ) |
7 | | eluzelz 9449 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → 𝑘 ∈ ℤ) |
8 | 2, 7 | syl 14 |
. . . . . 6
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈
ℤ) |
9 | | zlem1lt 9224 |
. . . . . 6
⊢ (((𝑁 + 1) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑁 + 1) ≤ 𝑘 ↔ ((𝑁 + 1) − 1) < 𝑘)) |
10 | 6, 8, 9 | syl2anc 409 |
. . . . 5
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → ((𝑁 + 1) ≤ 𝑘 ↔ ((𝑁 + 1) − 1) < 𝑘)) |
11 | 4, 10 | mpbid 146 |
. . . 4
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → ((𝑁 + 1) − 1) < 𝑘) |
12 | 1 | simplbi 272 |
. . . . . 6
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈ (0...𝑁)) |
13 | | elfzle2 9931 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ≤ 𝑁) |
14 | 12, 13 | syl 14 |
. . . . 5
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑘 ≤ 𝑁) |
15 | 8 | zred 9287 |
. . . . . . 7
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈
ℝ) |
16 | | elfzel2 9927 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑁) → 𝑁 ∈ ℤ) |
17 | 16 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑘 ∈ (0...𝑁) ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ ℤ) |
18 | 1, 17 | sylbi 120 |
. . . . . . . 8
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ ℤ) |
19 | 18 | zred 9287 |
. . . . . . 7
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ ℝ) |
20 | 15, 19 | lenltd 7994 |
. . . . . 6
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → (𝑘 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑘)) |
21 | 18 | zcnd 9288 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ ℂ) |
22 | | pncan1 8253 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
23 | 21, 22 | syl 14 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → ((𝑁 + 1) − 1) = 𝑁) |
24 | 23 | eqcomd 2163 |
. . . . . . . 8
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑁 = ((𝑁 + 1) − 1)) |
25 | 24 | breq1d 3976 |
. . . . . . 7
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → (𝑁 < 𝑘 ↔ ((𝑁 + 1) − 1) < 𝑘)) |
26 | 25 | notbid 657 |
. . . . . 6
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → (¬ 𝑁 < 𝑘 ↔ ¬ ((𝑁 + 1) − 1) < 𝑘)) |
27 | 20, 26 | bitrd 187 |
. . . . 5
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → (𝑘 ≤ 𝑁 ↔ ¬ ((𝑁 + 1) − 1) < 𝑘)) |
28 | 14, 27 | mpbid 146 |
. . . 4
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → ¬ ((𝑁 + 1) − 1) < 𝑘) |
29 | 11, 28 | pm2.21dd 610 |
. . 3
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈
∅) |
30 | 29 | ssriv 3132 |
. 2
⊢
((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) ⊆ ∅ |
31 | | ss0 3434 |
. 2
⊢
(((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) ⊆ ∅ → ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) = ∅) |
32 | 30, 31 | ax-mp 5 |
1
⊢
((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) = ∅ |