Step |
Hyp |
Ref |
Expression |
1 |
|
eldif |
|- ( x e. ( ( M ... N ) \ { M } ) <-> ( x e. ( M ... N ) /\ -. x e. { M } ) ) |
2 |
|
elsng |
|- ( x e. ( M ... N ) -> ( x e. { M } <-> x = M ) ) |
3 |
2
|
necon3bbid |
|- ( x e. ( M ... N ) -> ( -. x e. { M } <-> x =/= M ) ) |
4 |
|
fzne1 |
|- ( ( x e. ( M ... N ) /\ x =/= M ) -> x e. ( ( M + 1 ) ... N ) ) |
5 |
3 4
|
sylbida |
|- ( ( x e. ( M ... N ) /\ -. x e. { M } ) -> x e. ( ( M + 1 ) ... N ) ) |
6 |
|
eluzel2 |
|- ( N e. ( ZZ>= ` M ) -> M e. ZZ ) |
7 |
6
|
uzidd |
|- ( N e. ( ZZ>= ` M ) -> M e. ( ZZ>= ` M ) ) |
8 |
|
peano2uz |
|- ( M e. ( ZZ>= ` M ) -> ( M + 1 ) e. ( ZZ>= ` M ) ) |
9 |
|
fzss1 |
|- ( ( M + 1 ) e. ( ZZ>= ` M ) -> ( ( M + 1 ) ... N ) C_ ( M ... N ) ) |
10 |
7 8 9
|
3syl |
|- ( N e. ( ZZ>= ` M ) -> ( ( M + 1 ) ... N ) C_ ( M ... N ) ) |
11 |
10
|
sselda |
|- ( ( N e. ( ZZ>= ` M ) /\ x e. ( ( M + 1 ) ... N ) ) -> x e. ( M ... N ) ) |
12 |
|
elfz2 |
|- ( x e. ( ( M + 1 ) ... N ) <-> ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ x e. ZZ ) /\ ( ( M + 1 ) <_ x /\ x <_ N ) ) ) |
13 |
6
|
zred |
|- ( N e. ( ZZ>= ` M ) -> M e. RR ) |
14 |
13
|
adantl |
|- ( ( ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ x e. ZZ ) /\ ( ( M + 1 ) <_ x /\ x <_ N ) ) /\ N e. ( ZZ>= ` M ) ) -> M e. RR ) |
15 |
|
simp3 |
|- ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ x e. ZZ ) -> x e. ZZ ) |
16 |
|
zltp1le |
|- ( ( M e. ZZ /\ x e. ZZ ) -> ( M < x <-> ( M + 1 ) <_ x ) ) |
17 |
6 15 16
|
syl2anr |
|- ( ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ x e. ZZ ) /\ N e. ( ZZ>= ` M ) ) -> ( M < x <-> ( M + 1 ) <_ x ) ) |
18 |
17
|
biimprd |
|- ( ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ x e. ZZ ) /\ N e. ( ZZ>= ` M ) ) -> ( ( M + 1 ) <_ x -> M < x ) ) |
19 |
18
|
a1d |
|- ( ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ x e. ZZ ) /\ N e. ( ZZ>= ` M ) ) -> ( x <_ N -> ( ( M + 1 ) <_ x -> M < x ) ) ) |
20 |
19
|
ex |
|- ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ x e. ZZ ) -> ( N e. ( ZZ>= ` M ) -> ( x <_ N -> ( ( M + 1 ) <_ x -> M < x ) ) ) ) |
21 |
20
|
com24 |
|- ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ x e. ZZ ) -> ( ( M + 1 ) <_ x -> ( x <_ N -> ( N e. ( ZZ>= ` M ) -> M < x ) ) ) ) |
22 |
21
|
imp42 |
|- ( ( ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ x e. ZZ ) /\ ( ( M + 1 ) <_ x /\ x <_ N ) ) /\ N e. ( ZZ>= ` M ) ) -> M < x ) |
23 |
14 22
|
gtned |
|- ( ( ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ x e. ZZ ) /\ ( ( M + 1 ) <_ x /\ x <_ N ) ) /\ N e. ( ZZ>= ` M ) ) -> x =/= M ) |
24 |
23
|
ex |
|- ( ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ x e. ZZ ) /\ ( ( M + 1 ) <_ x /\ x <_ N ) ) -> ( N e. ( ZZ>= ` M ) -> x =/= M ) ) |
25 |
12 24
|
sylbi |
|- ( x e. ( ( M + 1 ) ... N ) -> ( N e. ( ZZ>= ` M ) -> x =/= M ) ) |
26 |
25
|
impcom |
|- ( ( N e. ( ZZ>= ` M ) /\ x e. ( ( M + 1 ) ... N ) ) -> x =/= M ) |
27 |
|
nelsn |
|- ( x =/= M -> -. x e. { M } ) |
28 |
26 27
|
syl |
|- ( ( N e. ( ZZ>= ` M ) /\ x e. ( ( M + 1 ) ... N ) ) -> -. x e. { M } ) |
29 |
11 28
|
jca |
|- ( ( N e. ( ZZ>= ` M ) /\ x e. ( ( M + 1 ) ... N ) ) -> ( x e. ( M ... N ) /\ -. x e. { M } ) ) |
30 |
29
|
ex |
|- ( N e. ( ZZ>= ` M ) -> ( x e. ( ( M + 1 ) ... N ) -> ( x e. ( M ... N ) /\ -. x e. { M } ) ) ) |
31 |
5 30
|
impbid2 |
|- ( N e. ( ZZ>= ` M ) -> ( ( x e. ( M ... N ) /\ -. x e. { M } ) <-> x e. ( ( M + 1 ) ... N ) ) ) |
32 |
1 31
|
bitrid |
|- ( N e. ( ZZ>= ` M ) -> ( x e. ( ( M ... N ) \ { M } ) <-> x e. ( ( M + 1 ) ... N ) ) ) |
33 |
32
|
eqrdv |
|- ( N e. ( ZZ>= ` M ) -> ( ( M ... N ) \ { M } ) = ( ( M + 1 ) ... N ) ) |