Metamath Proof Explorer

Theorem fzoopth

Description: A half-open integer range can represent an ordered pair, analogous to fzopth . (Contributed by Alexander van der Vekens, 1-Jul-2018)

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

Proof

Step Hyp Ref Expression
1 fzolb 
 |-  ( M e. ( M ..^ N ) <-> ( M e. ZZ /\ N e. ZZ /\ M < N ) )
2 1 biranri 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> M e. ( M ..^ N ) )
3 simpr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> ( M ..^ N ) = ( J ..^ K ) )
4 2 3 eleqtrd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> M e. ( J ..^ K ) )
5 elfzouz 
 |-  ( M e. ( J ..^ K ) -> M e. ( ZZ>= ` J ) )
6 uzss 
 |-  ( M e. ( ZZ>= ` J ) -> ( ZZ>= ` M ) C_ ( ZZ>= ` J ) )
7 4 5 6 3syl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> ( ZZ>= ` M ) C_ ( ZZ>= ` J ) )
8 eleq2 
 |-  ( ( M ..^ N ) = ( J ..^ K ) -> ( M e. ( M ..^ N ) <-> M e. ( J ..^ K ) ) )
9 8 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> ( M e. ( M ..^ N ) <-> M e. ( J ..^ K ) ) )
10 2 9 mpbid 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> M e. ( J ..^ K ) )
11 elfzolt3b 
 |-  ( M e. ( J ..^ K ) -> J e. ( J ..^ K ) )
12 10 11 syl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> J e. ( J ..^ K ) )
13 12 3 eleqtrrd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> J e. ( M ..^ N ) )
14 elfzouz 
 |-  ( J e. ( M ..^ N ) -> J e. ( ZZ>= ` M ) )
15 uzss 
 |-  ( J e. ( ZZ>= ` M ) -> ( ZZ>= ` J ) C_ ( ZZ>= ` M ) )
16 13 14 15 3syl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> ( ZZ>= ` J ) C_ ( ZZ>= ` M ) )
17 7 16 eqssd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> ( ZZ>= ` M ) = ( ZZ>= ` J ) )
18 simpl1 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> M e. ZZ )
19 uz11 
 |-  ( M e. ZZ -> ( ( ZZ>= ` M ) = ( ZZ>= ` J ) <-> M = J ) )
20 18 19 syl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> ( ( ZZ>= ` M ) = ( ZZ>= ` J ) <-> M = J ) )
21 17 20 mpbid 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> M = J )
22 fzoend 
 |-  ( J e. ( J ..^ K ) -> ( K - 1 ) e. ( J ..^ K ) )
23 elfzoel2 
 |-  ( ( K - 1 ) e. ( J ..^ K ) -> K e. ZZ )
24 eleq2 
 |-  ( ( J ..^ K ) = ( M ..^ N ) -> ( ( K - 1 ) e. ( J ..^ K ) <-> ( K - 1 ) e. ( M ..^ N ) ) )
25 24 eqcoms 
 |-  ( ( M ..^ N ) = ( J ..^ K ) -> ( ( K - 1 ) e. ( J ..^ K ) <-> ( K - 1 ) e. ( M ..^ N ) ) )
26 elfzo2 
 |-  ( ( K - 1 ) e. ( M ..^ N ) <-> ( ( K - 1 ) e. ( ZZ>= ` M ) /\ N e. ZZ /\ ( K - 1 ) < N ) )
27 simpl 
 |-  ( ( K e. ZZ /\ ( N e. ZZ /\ ( K - 1 ) < N ) ) -> K e. ZZ )
28 simprl 
 |-  ( ( K e. ZZ /\ ( N e. ZZ /\ ( K - 1 ) < N ) ) -> N e. ZZ )
29 zlem1lt 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( K <_ N <-> ( K - 1 ) < N ) )
30 29 ancoms 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( K <_ N <-> ( K - 1 ) < N ) )
31 30 biimprd 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( ( K - 1 ) < N -> K <_ N ) )
32 31 impancom 
 |-  ( ( N e. ZZ /\ ( K - 1 ) < N ) -> ( K e. ZZ -> K <_ N ) )
33 32 impcom 
 |-  ( ( K e. ZZ /\ ( N e. ZZ /\ ( K - 1 ) < N ) ) -> K <_ N )
34 27 28 33 3jca 
 |-  ( ( K e. ZZ /\ ( N e. ZZ /\ ( K - 1 ) < N ) ) -> ( K e. ZZ /\ N e. ZZ /\ K <_ N ) )
35 34 expcom 
 |-  ( ( N e. ZZ /\ ( K - 1 ) < N ) -> ( K e. ZZ -> ( K e. ZZ /\ N e. ZZ /\ K <_ N ) ) )
36 35 3adant1 
 |-  ( ( ( K - 1 ) e. ( ZZ>= ` M ) /\ N e. ZZ /\ ( K - 1 ) < N ) -> ( K e. ZZ -> ( K e. ZZ /\ N e. ZZ /\ K <_ N ) ) )
37 36 a1d 
 |-  ( ( ( K - 1 ) e. ( ZZ>= ` M ) /\ N e. ZZ /\ ( K - 1 ) < N ) -> ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( K e. ZZ -> ( K e. ZZ /\ N e. ZZ /\ K <_ N ) ) ) )
38 26 37 sylbi 
 |-  ( ( K - 1 ) e. ( M ..^ N ) -> ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( K e. ZZ -> ( K e. ZZ /\ N e. ZZ /\ K <_ N ) ) ) )
39 25 38 biimtrdi 
 |-  ( ( M ..^ N ) = ( J ..^ K ) -> ( ( K - 1 ) e. ( J ..^ K ) -> ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( K e. ZZ -> ( K e. ZZ /\ N e. ZZ /\ K <_ N ) ) ) ) )
40 39 com23 
 |-  ( ( M ..^ N ) = ( J ..^ K ) -> ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( ( K - 1 ) e. ( J ..^ K ) -> ( K e. ZZ -> ( K e. ZZ /\ N e. ZZ /\ K <_ N ) ) ) ) )
41 40 impcom 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> ( ( K - 1 ) e. ( J ..^ K ) -> ( K e. ZZ -> ( K e. ZZ /\ N e. ZZ /\ K <_ N ) ) ) )
42 41 com13 
 |-  ( K e. ZZ -> ( ( K - 1 ) e. ( J ..^ K ) -> ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> ( K e. ZZ /\ N e. ZZ /\ K <_ N ) ) ) )
43 23 42 mpcom 
 |-  ( ( K - 1 ) e. ( J ..^ K ) -> ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> ( K e. ZZ /\ N e. ZZ /\ K <_ N ) ) )
44 22 43 syl 
 |-  ( J e. ( J ..^ K ) -> ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> ( K e. ZZ /\ N e. ZZ /\ K <_ N ) ) )
45 12 44 mpcom 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> ( K e. ZZ /\ N e. ZZ /\ K <_ N ) )
46 eluz2 
 |-  ( N e. ( ZZ>= ` K ) <-> ( K e. ZZ /\ N e. ZZ /\ K <_ N ) )
47 46 biimpri 
 |-  ( ( K e. ZZ /\ N e. ZZ /\ K <_ N ) -> N e. ( ZZ>= ` K ) )
48 uzss 
 |-  ( N e. ( ZZ>= ` K ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` K ) )
49 45 47 48 3syl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` K ) )
50 1 biimpri 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> M e. ( M ..^ N ) )
51 fzoend 
 |-  ( M e. ( M ..^ N ) -> ( N - 1 ) e. ( M ..^ N ) )
52 eleq2 
 |-  ( ( M ..^ N ) = ( J ..^ K ) -> ( ( N - 1 ) e. ( M ..^ N ) <-> ( N - 1 ) e. ( J ..^ K ) ) )
53 elfzo2 
 |-  ( ( N - 1 ) e. ( J ..^ K ) <-> ( ( N - 1 ) e. ( ZZ>= ` J ) /\ K e. ZZ /\ ( N - 1 ) < K ) )
54 pm3.2 
 |-  ( N e. ZZ -> ( ( K e. ZZ /\ ( N - 1 ) < K ) -> ( N e. ZZ /\ ( K e. ZZ /\ ( N - 1 ) < K ) ) ) )
55 54 3ad2ant2 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( ( K e. ZZ /\ ( N - 1 ) < K ) -> ( N e. ZZ /\ ( K e. ZZ /\ ( N - 1 ) < K ) ) ) )
56 55 com12 
 |-  ( ( K e. ZZ /\ ( N - 1 ) < K ) -> ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( N e. ZZ /\ ( K e. ZZ /\ ( N - 1 ) < K ) ) ) )
57 56 3adant1 
 |-  ( ( ( N - 1 ) e. ( ZZ>= ` J ) /\ K e. ZZ /\ ( N - 1 ) < K ) -> ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( N e. ZZ /\ ( K e. ZZ /\ ( N - 1 ) < K ) ) ) )
58 53 57 sylbi 
 |-  ( ( N - 1 ) e. ( J ..^ K ) -> ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( N e. ZZ /\ ( K e. ZZ /\ ( N - 1 ) < K ) ) ) )
59 52 58 biimtrdi 
 |-  ( ( M ..^ N ) = ( J ..^ K ) -> ( ( N - 1 ) e. ( M ..^ N ) -> ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( N e. ZZ /\ ( K e. ZZ /\ ( N - 1 ) < K ) ) ) ) )
60 59 com3l 
 |-  ( ( N - 1 ) e. ( M ..^ N ) -> ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( ( M ..^ N ) = ( J ..^ K ) -> ( N e. ZZ /\ ( K e. ZZ /\ ( N - 1 ) < K ) ) ) ) )
61 51 60 syl 
 |-  ( M e. ( M ..^ N ) -> ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( ( M ..^ N ) = ( J ..^ K ) -> ( N e. ZZ /\ ( K e. ZZ /\ ( N - 1 ) < K ) ) ) ) )
62 50 61 mpcom 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( ( M ..^ N ) = ( J ..^ K ) -> ( N e. ZZ /\ ( K e. ZZ /\ ( N - 1 ) < K ) ) ) )
63 62 imp 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> ( N e. ZZ /\ ( K e. ZZ /\ ( N - 1 ) < K ) ) )
64 simpl 
 |-  ( ( N e. ZZ /\ ( K e. ZZ /\ ( N - 1 ) < K ) ) -> N e. ZZ )
65 simprl 
 |-  ( ( N e. ZZ /\ ( K e. ZZ /\ ( N - 1 ) < K ) ) -> K e. ZZ )
66 zlem1lt 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( N <_ K <-> ( N - 1 ) < K ) )
67 66 ancoms 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( N <_ K <-> ( N - 1 ) < K ) )
68 67 biimprd 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( ( N - 1 ) < K -> N <_ K ) )
69 68 impancom 
 |-  ( ( K e. ZZ /\ ( N - 1 ) < K ) -> ( N e. ZZ -> N <_ K ) )
70 69 impcom 
 |-  ( ( N e. ZZ /\ ( K e. ZZ /\ ( N - 1 ) < K ) ) -> N <_ K )
71 eluz2 
 |-  ( K e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ K e. ZZ /\ N <_ K ) )
72 64 65 70 71 syl3anbrc 
 |-  ( ( N e. ZZ /\ ( K e. ZZ /\ ( N - 1 ) < K ) ) -> K e. ( ZZ>= ` N ) )
73 uzss 
 |-  ( K e. ( ZZ>= ` N ) -> ( ZZ>= ` K ) C_ ( ZZ>= ` N ) )
74 63 72 73 3syl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> ( ZZ>= ` K ) C_ ( ZZ>= ` N ) )
75 49 74 eqssd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> ( ZZ>= ` N ) = ( ZZ>= ` K ) )
76 simpl2 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> N e. ZZ )
77 uz11 
 |-  ( N e. ZZ -> ( ( ZZ>= ` N ) = ( ZZ>= ` K ) <-> N = K ) )
78 76 77 syl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> ( ( ZZ>= ` N ) = ( ZZ>= ` K ) <-> N = K ) )
79 75 78 mpbid 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> N = K )
80 21 79 jca 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ M < N ) /\ ( M ..^ N ) = ( J ..^ K ) ) -> ( M = J /\ N = K ) )
81 80 ex 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( ( M ..^ N ) = ( J ..^ K ) -> ( M = J /\ N = K ) ) )
82 oveq12 
 |-  ( ( M = J /\ N = K ) -> ( M ..^ N ) = ( J ..^ K ) )
83 81 82 impbid1 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( ( M ..^ N ) = ( J ..^ K ) <-> ( M = J /\ N = K ) ) )