Metamath Proof Explorer


Theorem fzopth

Description: A finite set of sequential integers has the ordered pair property (compare opth ) under certain conditions. (Contributed by NM, 31-Oct-2005) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fzopth
|- ( N e. ( ZZ>= ` M ) -> ( ( M ... N ) = ( J ... K ) <-> ( M = J /\ N = K ) ) )

Proof

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 ) ) )