| Step | Hyp | Ref
| Expression |
| 1 | | eldif 3961 |
. . 3
⊢ (𝑥 ∈ ((𝑀...𝑁) ∖ {𝑀}) ↔ (𝑥 ∈ (𝑀...𝑁) ∧ ¬ 𝑥 ∈ {𝑀})) |
| 2 | | elsng 4640 |
. . . . . 6
⊢ (𝑥 ∈ (𝑀...𝑁) → (𝑥 ∈ {𝑀} ↔ 𝑥 = 𝑀)) |
| 3 | 2 | necon3bbid 2978 |
. . . . 5
⊢ (𝑥 ∈ (𝑀...𝑁) → (¬ 𝑥 ∈ {𝑀} ↔ 𝑥 ≠ 𝑀)) |
| 4 | | fzne1 13644 |
. . . . 5
⊢ ((𝑥 ∈ (𝑀...𝑁) ∧ 𝑥 ≠ 𝑀) → 𝑥 ∈ ((𝑀 + 1)...𝑁)) |
| 5 | 3, 4 | sylbida 592 |
. . . 4
⊢ ((𝑥 ∈ (𝑀...𝑁) ∧ ¬ 𝑥 ∈ {𝑀}) → 𝑥 ∈ ((𝑀 + 1)...𝑁)) |
| 6 | | eluzel2 12883 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
| 7 | 6 | uzidd 12894 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (ℤ≥‘𝑀)) |
| 8 | | peano2uz 12943 |
. . . . . . . 8
⊢ (𝑀 ∈
(ℤ≥‘𝑀) → (𝑀 + 1) ∈
(ℤ≥‘𝑀)) |
| 9 | | fzss1 13603 |
. . . . . . . 8
⊢ ((𝑀 + 1) ∈
(ℤ≥‘𝑀) → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
| 10 | 7, 8, 9 | 3syl 18 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
| 11 | 10 | sselda 3983 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑥 ∈ ((𝑀 + 1)...𝑁)) → 𝑥 ∈ (𝑀...𝑁)) |
| 12 | | elfz2 13554 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑥 ∧ 𝑥 ≤ 𝑁))) |
| 13 | 6 | zred 12722 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℝ) |
| 14 | 13 | adantl 481 |
. . . . . . . . . . 11
⊢
(((((𝑀 + 1) ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑥 ∈
ℤ) ∧ ((𝑀 + 1)
≤ 𝑥 ∧ 𝑥 ≤ 𝑁)) ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ ℝ) |
| 15 | | simp3 1139 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ) → 𝑥 ∈
ℤ) |
| 16 | | zltp1le 12667 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑀 < 𝑥 ↔ (𝑀 + 1) ≤ 𝑥)) |
| 17 | 6, 15, 16 | syl2anr 597 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ) ∧ 𝑁 ∈
(ℤ≥‘𝑀)) → (𝑀 < 𝑥 ↔ (𝑀 + 1) ≤ 𝑥)) |
| 18 | 17 | biimprd 248 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ) ∧ 𝑁 ∈
(ℤ≥‘𝑀)) → ((𝑀 + 1) ≤ 𝑥 → 𝑀 < 𝑥)) |
| 19 | 18 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ) ∧ 𝑁 ∈
(ℤ≥‘𝑀)) → (𝑥 ≤ 𝑁 → ((𝑀 + 1) ≤ 𝑥 → 𝑀 < 𝑥))) |
| 20 | 19 | ex 412 |
. . . . . . . . . . . . 13
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘𝑀) → (𝑥 ≤ 𝑁 → ((𝑀 + 1) ≤ 𝑥 → 𝑀 < 𝑥)))) |
| 21 | 20 | com24 95 |
. . . . . . . . . . . 12
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ) → ((𝑀 + 1) ≤ 𝑥 → (𝑥 ≤ 𝑁 → (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 < 𝑥)))) |
| 22 | 21 | imp42 426 |
. . . . . . . . . . 11
⊢
(((((𝑀 + 1) ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑥 ∈
ℤ) ∧ ((𝑀 + 1)
≤ 𝑥 ∧ 𝑥 ≤ 𝑁)) ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → 𝑀 < 𝑥) |
| 23 | 14, 22 | gtned 11396 |
. . . . . . . . . 10
⊢
(((((𝑀 + 1) ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑥 ∈
ℤ) ∧ ((𝑀 + 1)
≤ 𝑥 ∧ 𝑥 ≤ 𝑁)) ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → 𝑥 ≠ 𝑀) |
| 24 | 23 | ex 412 |
. . . . . . . . 9
⊢ ((((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)) → (𝑁 ∈ (ℤ≥‘𝑀) → 𝑥 ≠ 𝑀)) |
| 25 | 12, 24 | sylbi 217 |
. . . . . . . 8
⊢ (𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝑁 ∈ (ℤ≥‘𝑀) → 𝑥 ≠ 𝑀)) |
| 26 | 25 | impcom 407 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑥 ∈ ((𝑀 + 1)...𝑁)) → 𝑥 ≠ 𝑀) |
| 27 | | nelsn 4666 |
. . . . . . 7
⊢ (𝑥 ≠ 𝑀 → ¬ 𝑥 ∈ {𝑀}) |
| 28 | 26, 27 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑥 ∈ ((𝑀 + 1)...𝑁)) → ¬ 𝑥 ∈ {𝑀}) |
| 29 | 11, 28 | jca 511 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑥 ∈ ((𝑀 + 1)...𝑁)) → (𝑥 ∈ (𝑀...𝑁) ∧ ¬ 𝑥 ∈ {𝑀})) |
| 30 | 29 | ex 412 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝑥 ∈ (𝑀...𝑁) ∧ ¬ 𝑥 ∈ {𝑀}))) |
| 31 | 5, 30 | impbid2 226 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝑥 ∈ (𝑀...𝑁) ∧ ¬ 𝑥 ∈ {𝑀}) ↔ 𝑥 ∈ ((𝑀 + 1)...𝑁))) |
| 32 | 1, 31 | bitrid 283 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑥 ∈ ((𝑀...𝑁) ∖ {𝑀}) ↔ 𝑥 ∈ ((𝑀 + 1)...𝑁))) |
| 33 | 32 | eqrdv 2735 |
1
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝑀...𝑁) ∖ {𝑀}) = ((𝑀 + 1)...𝑁)) |