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