Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> N = ( M - 1 ) ) |
2 |
|
zre |
|- ( M e. ZZ -> M e. RR ) |
3 |
2
|
ad2antlr |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> M e. RR ) |
4 |
3
|
ltm1d |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( M - 1 ) < M ) |
5 |
1 4
|
eqbrtrd |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> N < M ) |
6 |
|
simplr |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> M e. ZZ ) |
7 |
|
eluzelz |
|- ( N e. ( ZZ>= ` ( M - 1 ) ) -> N e. ZZ ) |
8 |
7
|
ad2antrr |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> N e. ZZ ) |
9 |
|
fzn |
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( N < M <-> ( M ... N ) = (/) ) ) |
10 |
6 8 9
|
syl2anc |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( N < M <-> ( M ... N ) = (/) ) ) |
11 |
5 10
|
mpbid |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( M ... N ) = (/) ) |
12 |
|
difid |
|- ( { M } \ { M } ) = (/) |
13 |
12
|
a1i |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( { M } \ { M } ) = (/) ) |
14 |
13
|
eqcomd |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> (/) = ( { M } \ { M } ) ) |
15 |
|
oveq1 |
|- ( N = ( M - 1 ) -> ( N + 1 ) = ( ( M - 1 ) + 1 ) ) |
16 |
15
|
adantl |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( N + 1 ) = ( ( M - 1 ) + 1 ) ) |
17 |
2
|
recnd |
|- ( M e. ZZ -> M e. CC ) |
18 |
17
|
ad2antlr |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> M e. CC ) |
19 |
|
1cnd |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> 1 e. CC ) |
20 |
18 19
|
npcand |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( ( M - 1 ) + 1 ) = M ) |
21 |
16 20
|
eqtrd |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( N + 1 ) = M ) |
22 |
21
|
oveq2d |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( M ... ( N + 1 ) ) = ( M ... M ) ) |
23 |
|
fzsn |
|- ( M e. ZZ -> ( M ... M ) = { M } ) |
24 |
23
|
ad2antlr |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( M ... M ) = { M } ) |
25 |
22 24
|
eqtr2d |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> { M } = ( M ... ( N + 1 ) ) ) |
26 |
21
|
eqcomd |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> M = ( N + 1 ) ) |
27 |
26
|
sneqd |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> { M } = { ( N + 1 ) } ) |
28 |
25 27
|
difeq12d |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( { M } \ { M } ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) ) |
29 |
11 14 28
|
3eqtrd |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ N = ( M - 1 ) ) -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) ) |
30 |
|
simplr |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> M e. ZZ ) |
31 |
7
|
ad2antrr |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> N e. ZZ ) |
32 |
2
|
ad2antlr |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> M e. RR ) |
33 |
|
1red |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> 1 e. RR ) |
34 |
32 33
|
resubcld |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> ( M - 1 ) e. RR ) |
35 |
31
|
zred |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> N e. RR ) |
36 |
|
eluzle |
|- ( N e. ( ZZ>= ` ( M - 1 ) ) -> ( M - 1 ) <_ N ) |
37 |
36
|
ad2antrr |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> ( M - 1 ) <_ N ) |
38 |
|
neqne |
|- ( -. N = ( M - 1 ) -> N =/= ( M - 1 ) ) |
39 |
38
|
adantl |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> N =/= ( M - 1 ) ) |
40 |
34 35 37 39
|
leneltd |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> ( M - 1 ) < N ) |
41 |
|
zlem1lt |
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( M - 1 ) < N ) ) |
42 |
30 31 41
|
syl2anc |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> ( M <_ N <-> ( M - 1 ) < N ) ) |
43 |
40 42
|
mpbird |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> M <_ N ) |
44 |
30 31 43
|
3jca |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) ) |
45 |
|
eluz2 |
|- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) ) |
46 |
44 45
|
sylibr |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> N e. ( ZZ>= ` M ) ) |
47 |
|
fzdifsuc |
|- ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) ) |
48 |
46 47
|
syl |
|- ( ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) /\ -. N = ( M - 1 ) ) -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) ) |
49 |
29 48
|
pm2.61dan |
|- ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ M e. ZZ ) -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) ) |
50 |
|
eluzel2 |
|- ( N e. ( ZZ>= ` M ) -> M e. ZZ ) |
51 |
50
|
con3i |
|- ( -. M e. ZZ -> -. N e. ( ZZ>= ` M ) ) |
52 |
|
fzn0 |
|- ( ( M ... N ) =/= (/) <-> N e. ( ZZ>= ` M ) ) |
53 |
51 52
|
sylnibr |
|- ( -. M e. ZZ -> -. ( M ... N ) =/= (/) ) |
54 |
|
nne |
|- ( -. ( M ... N ) =/= (/) <-> ( M ... N ) = (/) ) |
55 |
53 54
|
sylib |
|- ( -. M e. ZZ -> ( M ... N ) = (/) ) |
56 |
|
eluzel2 |
|- ( ( N + 1 ) e. ( ZZ>= ` M ) -> M e. ZZ ) |
57 |
56
|
con3i |
|- ( -. M e. ZZ -> -. ( N + 1 ) e. ( ZZ>= ` M ) ) |
58 |
|
fzn0 |
|- ( ( M ... ( N + 1 ) ) =/= (/) <-> ( N + 1 ) e. ( ZZ>= ` M ) ) |
59 |
57 58
|
sylnibr |
|- ( -. M e. ZZ -> -. ( M ... ( N + 1 ) ) =/= (/) ) |
60 |
|
nne |
|- ( -. ( M ... ( N + 1 ) ) =/= (/) <-> ( M ... ( N + 1 ) ) = (/) ) |
61 |
59 60
|
sylib |
|- ( -. M e. ZZ -> ( M ... ( N + 1 ) ) = (/) ) |
62 |
61
|
difeq1d |
|- ( -. M e. ZZ -> ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) = ( (/) \ { ( N + 1 ) } ) ) |
63 |
|
0dif |
|- ( (/) \ { ( N + 1 ) } ) = (/) |
64 |
63
|
a1i |
|- ( -. M e. ZZ -> ( (/) \ { ( N + 1 ) } ) = (/) ) |
65 |
62 64
|
eqtr2d |
|- ( -. M e. ZZ -> (/) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) ) |
66 |
55 65
|
eqtrd |
|- ( -. M e. ZZ -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) ) |
67 |
66
|
adantl |
|- ( ( N e. ( ZZ>= ` ( M - 1 ) ) /\ -. M e. ZZ ) -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) ) |
68 |
49 67
|
pm2.61dan |
|- ( N e. ( ZZ>= ` ( M - 1 ) ) -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) ) |