Step | Hyp | Ref
| Expression |
1 | | elin 3229 |
. . . . . . 7
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) ↔ (𝑘 ∈ (0...𝑁) ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1)))) |
2 | 1 | simprbi 273 |
. . . . . 6
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈
(ℤ≥‘(𝑁 + 1))) |
3 | | eluzle 9306 |
. . . . . 6
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → (𝑁 + 1) ≤ 𝑘) |
4 | 2, 3 | syl 14 |
. . . . 5
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → (𝑁 + 1) ≤ 𝑘) |
5 | | eluzel2 9299 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → (𝑁 + 1) ∈ ℤ) |
6 | 2, 5 | syl 14 |
. . . . . 6
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → (𝑁 + 1) ∈
ℤ) |
7 | | eluzelz 9303 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → 𝑘 ∈ ℤ) |
8 | 2, 7 | syl 14 |
. . . . . 6
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈
ℤ) |
9 | | zlem1lt 9078 |
. . . . . 6
⊢ (((𝑁 + 1) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑁 + 1) ≤ 𝑘 ↔ ((𝑁 + 1) − 1) < 𝑘)) |
10 | 6, 8, 9 | syl2anc 408 |
. . . . 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 9776 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ≤ 𝑁) |
14 | 12, 13 | syl 14 |
. . . . 5
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑘 ≤ 𝑁) |
15 | 8 | zred 9141 |
. . . . . . 7
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈
ℝ) |
16 | | elfzel2 9772 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑁) → 𝑁 ∈ ℤ) |
17 | 16 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑘 ∈ (0...𝑁) ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ ℤ) |
18 | 1, 17 | sylbi 120 |
. . . . . . . 8
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ ℤ) |
19 | 18 | zred 9141 |
. . . . . . 7
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ ℝ) |
20 | 15, 19 | lenltd 7848 |
. . . . . 6
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → (𝑘 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑘)) |
21 | 18 | zcnd 9142 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ ℂ) |
22 | | pncan1 8107 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
23 | 21, 22 | syl 14 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → ((𝑁 + 1) − 1) = 𝑁) |
24 | 23 | eqcomd 2123 |
. . . . . . . 8
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑁 = ((𝑁 + 1) − 1)) |
25 | 24 | breq1d 3909 |
. . . . . . 7
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → (𝑁 < 𝑘 ↔ ((𝑁 + 1) − 1) < 𝑘)) |
26 | 25 | notbid 641 |
. . . . . 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 594 |
. . 3
⊢ (𝑘 ∈ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈
∅) |
30 | 29 | ssriv 3071 |
. 2
⊢
((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) ⊆ ∅ |
31 | | ss0 3373 |
. 2
⊢
(((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) ⊆ ∅ → ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) = ∅) |
32 | 30, 31 | ax-mp 5 |
1
⊢
((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) = ∅ |