Step |
Hyp |
Ref |
Expression |
1 |
|
eluzfz1 |
|- ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) ) |
2 |
1
|
adantr |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> M e. ( M ... N ) ) |
3 |
|
simpr |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> ( M ... N ) = ( J ... K ) ) |
4 |
2 3
|
eleqtrd |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> M e. ( J ... K ) ) |
5 |
|
elfzuz |
|- ( M e. ( J ... K ) -> M e. ( ZZ>= ` J ) ) |
6 |
|
uzss |
|- ( M e. ( ZZ>= ` J ) -> ( ZZ>= ` M ) C_ ( ZZ>= ` J ) ) |
7 |
4 5 6
|
3syl |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> ( ZZ>= ` M ) C_ ( ZZ>= ` J ) ) |
8 |
|
elfzuz2 |
|- ( M e. ( J ... K ) -> K e. ( ZZ>= ` J ) ) |
9 |
|
eluzfz1 |
|- ( K e. ( ZZ>= ` J ) -> J e. ( J ... K ) ) |
10 |
4 8 9
|
3syl |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> J e. ( J ... K ) ) |
11 |
10 3
|
eleqtrrd |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> J e. ( M ... N ) ) |
12 |
|
elfzuz |
|- ( J e. ( M ... N ) -> J e. ( ZZ>= ` M ) ) |
13 |
|
uzss |
|- ( J e. ( ZZ>= ` M ) -> ( ZZ>= ` J ) C_ ( ZZ>= ` M ) ) |
14 |
11 12 13
|
3syl |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> ( ZZ>= ` J ) C_ ( ZZ>= ` M ) ) |
15 |
7 14
|
eqssd |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> ( ZZ>= ` M ) = ( ZZ>= ` J ) ) |
16 |
|
eluzel2 |
|- ( N e. ( ZZ>= ` M ) -> M e. ZZ ) |
17 |
16
|
adantr |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> M e. ZZ ) |
18 |
|
uz11 |
|- ( M e. ZZ -> ( ( ZZ>= ` M ) = ( ZZ>= ` J ) <-> M = J ) ) |
19 |
17 18
|
syl |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> ( ( ZZ>= ` M ) = ( ZZ>= ` J ) <-> M = J ) ) |
20 |
15 19
|
mpbid |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> M = J ) |
21 |
|
eluzfz2 |
|- ( K e. ( ZZ>= ` J ) -> K e. ( J ... K ) ) |
22 |
4 8 21
|
3syl |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> K e. ( J ... K ) ) |
23 |
22 3
|
eleqtrrd |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> K e. ( M ... N ) ) |
24 |
|
elfzuz3 |
|- ( K e. ( M ... N ) -> N e. ( ZZ>= ` K ) ) |
25 |
|
uzss |
|- ( N e. ( ZZ>= ` K ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` K ) ) |
26 |
23 24 25
|
3syl |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` K ) ) |
27 |
|
eluzfz2 |
|- ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) ) |
28 |
27
|
adantr |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> N e. ( M ... N ) ) |
29 |
28 3
|
eleqtrd |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> N e. ( J ... K ) ) |
30 |
|
elfzuz3 |
|- ( N e. ( J ... K ) -> K e. ( ZZ>= ` N ) ) |
31 |
|
uzss |
|- ( K e. ( ZZ>= ` N ) -> ( ZZ>= ` K ) C_ ( ZZ>= ` N ) ) |
32 |
29 30 31
|
3syl |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> ( ZZ>= ` K ) C_ ( ZZ>= ` N ) ) |
33 |
26 32
|
eqssd |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> ( ZZ>= ` N ) = ( ZZ>= ` K ) ) |
34 |
|
eluzelz |
|- ( N e. ( ZZ>= ` M ) -> N e. ZZ ) |
35 |
34
|
adantr |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> N e. ZZ ) |
36 |
|
uz11 |
|- ( N e. ZZ -> ( ( ZZ>= ` N ) = ( ZZ>= ` K ) <-> N = K ) ) |
37 |
35 36
|
syl |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> ( ( ZZ>= ` N ) = ( ZZ>= ` K ) <-> N = K ) ) |
38 |
33 37
|
mpbid |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> N = K ) |
39 |
20 38
|
jca |
|- ( ( N e. ( ZZ>= ` M ) /\ ( M ... N ) = ( J ... K ) ) -> ( M = J /\ N = K ) ) |
40 |
39
|
ex |
|- ( N e. ( ZZ>= ` M ) -> ( ( M ... N ) = ( J ... K ) -> ( M = J /\ N = K ) ) ) |
41 |
|
oveq12 |
|- ( ( M = J /\ N = K ) -> ( M ... N ) = ( J ... K ) ) |
42 |
40 41
|
impbid1 |
|- ( N e. ( ZZ>= ` M ) -> ( ( M ... N ) = ( J ... K ) <-> ( M = J /\ N = K ) ) ) |