# 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 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}<{N}\right)\to \left(\left({M}..^{N}\right)=\left({J}..^{K}\right)↔\left({M}={J}\wedge {N}={K}\right)\right)$

### Proof

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