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\in {\mathbb{Z}}_{\ge M}\to \left(\left(M\dots N\right)=\left(J\dots K\right)\leftrightarrow \left(M=J\wedge N=K\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eluzfz1	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \left(M\dots N\right)$$
2	1	adantr	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to M\in \left(M\dots N\right)$$
3		simpr	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to \left(M\dots N\right)=\left(J\dots K\right)$$
4	2 3	eleqtrd	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to M\in \left(J\dots K\right)$$
5		elfzuz	$$⊢M\in \left(J\dots K\right)\to M\in {\mathbb{Z}}_{\ge J}$$
6		uzss	$$⊢M\in {\mathbb{Z}}_{\ge J}\to {\mathbb{Z}}_{\ge M}\subseteq {\mathbb{Z}}_{\ge J}$$
7	4 5 6	3syl	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to {\mathbb{Z}}_{\ge M}\subseteq {\mathbb{Z}}_{\ge J}$$
8		elfzuz2	$$⊢M\in \left(J\dots K\right)\to K\in {\mathbb{Z}}_{\ge J}$$
9		eluzfz1	$$⊢K\in {\mathbb{Z}}_{\ge J}\to J\in \left(J\dots K\right)$$
10	4 8 9	3syl	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to J\in \left(J\dots K\right)$$
11	10 3	eleqtrrd	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to J\in \left(M\dots N\right)$$
12		elfzuz	$$⊢J\in \left(M\dots N\right)\to J\in {\mathbb{Z}}_{\ge M}$$
13		uzss	$$⊢J\in {\mathbb{Z}}_{\ge M}\to {\mathbb{Z}}_{\ge J}\subseteq {\mathbb{Z}}_{\ge M}$$
14	11 12 13	3syl	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to {\mathbb{Z}}_{\ge J}\subseteq {\mathbb{Z}}_{\ge M}$$
15	7 14	eqssd	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to {\mathbb{Z}}_{\ge M}={\mathbb{Z}}_{\ge J}$$
16		eluzel2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$
17	16	adantr	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to M\in \mathbb{Z}$$
18		uz11	$$⊢M\in \mathbb{Z}\to \left({\mathbb{Z}}_{\ge M}={\mathbb{Z}}_{\ge J}\leftrightarrow M=J\right)$$
19	17 18	syl	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to \left({\mathbb{Z}}_{\ge M}={\mathbb{Z}}_{\ge J}\leftrightarrow M=J\right)$$
20	15 19	mpbid	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to M=J$$
21		eluzfz2	$$⊢K\in {\mathbb{Z}}_{\ge J}\to K\in \left(J\dots K\right)$$
22	4 8 21	3syl	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to K\in \left(J\dots K\right)$$
23	22 3	eleqtrrd	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to K\in \left(M\dots N\right)$$
24		elfzuz3	$$⊢K\in \left(M\dots N\right)\to N\in {\mathbb{Z}}_{\ge K}$$
25		uzss	$$⊢N\in {\mathbb{Z}}_{\ge K}\to {\mathbb{Z}}_{\ge N}\subseteq {\mathbb{Z}}_{\ge K}$$
26	23 24 25	3syl	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to {\mathbb{Z}}_{\ge N}\subseteq {\mathbb{Z}}_{\ge K}$$
27		eluzfz2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \left(M\dots N\right)$$
28	27	adantr	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to N\in \left(M\dots N\right)$$
29	28 3	eleqtrd	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to N\in \left(J\dots K\right)$$
30		elfzuz3	$$⊢N\in \left(J\dots K\right)\to K\in {\mathbb{Z}}_{\ge N}$$
31		uzss	$$⊢K\in {\mathbb{Z}}_{\ge N}\to {\mathbb{Z}}_{\ge K}\subseteq {\mathbb{Z}}_{\ge N}$$
32	29 30 31	3syl	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to {\mathbb{Z}}_{\ge K}\subseteq {\mathbb{Z}}_{\ge N}$$
33	26 32	eqssd	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to {\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge K}$$
34		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$
35	34	adantr	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to N\in \mathbb{Z}$$
36		uz11	$$⊢N\in \mathbb{Z}\to \left({\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge K}\leftrightarrow N=K\right)$$
37	35 36	syl	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to \left({\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge K}\leftrightarrow N=K\right)$$
38	33 37	mpbid	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to N=K$$
39	20 38	jca	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge \left(M\dots N\right)=\left(J\dots K\right)\right)\to \left(M=J\wedge N=K\right)$$
40	39	ex	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\left(M\dots N\right)=\left(J\dots K\right)\to \left(M=J\wedge N=K\right)\right)$$
41		oveq12	$$⊢\left(M=J\wedge N=K\right)\to \left(M\dots N\right)=\left(J\dots K\right)$$
42	40 41	impbid1	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\left(M\dots N\right)=\left(J\dots K\right)\leftrightarrow \left(M=J\wedge N=K\right)\right)$$