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