Step |
Hyp |
Ref |
Expression |
1 |
|
eldif |
⊢ ( 𝑥 ∈ ( ( 𝑀 ... 𝑁 ) ∖ { 𝑀 } ) ↔ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ∧ ¬ 𝑥 ∈ { 𝑀 } ) ) |
2 |
|
elsng |
⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑥 ∈ { 𝑀 } ↔ 𝑥 = 𝑀 ) ) |
3 |
2
|
necon3bbid |
⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( ¬ 𝑥 ∈ { 𝑀 } ↔ 𝑥 ≠ 𝑀 ) ) |
4 |
|
fzne1 |
⊢ ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ≠ 𝑀 ) → 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) |
5 |
3 4
|
sylbida |
⊢ ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ∧ ¬ 𝑥 ∈ { 𝑀 } ) → 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) |
6 |
|
eluzel2 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ ) |
7 |
6
|
uzidd |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
8 |
|
peano2uz |
⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) |
9 |
|
fzss1 |
⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) ) |
10 |
7 8 9
|
3syl |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) ) |
11 |
10
|
sselda |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) |
12 |
|
elfz2 |
⊢ ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↔ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑀 + 1 ) ≤ 𝑥 ∧ 𝑥 ≤ 𝑁 ) ) ) |
13 |
6
|
zred |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℝ ) |
14 |
13
|
adantl |
⊢ ( ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑀 + 1 ) ≤ 𝑥 ∧ 𝑥 ≤ 𝑁 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ∈ ℝ ) |
15 |
|
simp3 |
⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℤ ) |
16 |
|
zltp1le |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑀 < 𝑥 ↔ ( 𝑀 + 1 ) ≤ 𝑥 ) ) |
17 |
6 15 16
|
syl2anr |
⊢ ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑀 < 𝑥 ↔ ( 𝑀 + 1 ) ≤ 𝑥 ) ) |
18 |
17
|
biimprd |
⊢ ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑀 + 1 ) ≤ 𝑥 → 𝑀 < 𝑥 ) ) |
19 |
18
|
a1d |
⊢ ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑥 ≤ 𝑁 → ( ( 𝑀 + 1 ) ≤ 𝑥 → 𝑀 < 𝑥 ) ) ) |
20 |
19
|
ex |
⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑥 ≤ 𝑁 → ( ( 𝑀 + 1 ) ≤ 𝑥 → 𝑀 < 𝑥 ) ) ) ) |
21 |
20
|
com24 |
⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( ( 𝑀 + 1 ) ≤ 𝑥 → ( 𝑥 ≤ 𝑁 → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 < 𝑥 ) ) ) ) |
22 |
21
|
imp42 |
⊢ ( ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑀 + 1 ) ≤ 𝑥 ∧ 𝑥 ≤ 𝑁 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 < 𝑥 ) |
23 |
14 22
|
gtned |
⊢ ( ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑀 + 1 ) ≤ 𝑥 ∧ 𝑥 ≤ 𝑁 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑥 ≠ 𝑀 ) |
24 |
23
|
ex |
⊢ ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑀 + 1 ) ≤ 𝑥 ∧ 𝑥 ≤ 𝑁 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑥 ≠ 𝑀 ) ) |
25 |
12 24
|
sylbi |
⊢ ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑥 ≠ 𝑀 ) ) |
26 |
25
|
impcom |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑥 ≠ 𝑀 ) |
27 |
|
nelsn |
⊢ ( 𝑥 ≠ 𝑀 → ¬ 𝑥 ∈ { 𝑀 } ) |
28 |
26 27
|
syl |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ¬ 𝑥 ∈ { 𝑀 } ) |
29 |
11 28
|
jca |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ∧ ¬ 𝑥 ∈ { 𝑀 } ) ) |
30 |
29
|
ex |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ∧ ¬ 𝑥 ∈ { 𝑀 } ) ) ) |
31 |
5 30
|
impbid2 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ∧ ¬ 𝑥 ∈ { 𝑀 } ) ↔ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) |
32 |
1 31
|
bitrid |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑥 ∈ ( ( 𝑀 ... 𝑁 ) ∖ { 𝑀 } ) ↔ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) |
33 |
32
|
eqrdv |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 ... 𝑁 ) ∖ { 𝑀 } ) = ( ( 𝑀 + 1 ) ... 𝑁 ) ) |