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 \in ℤ \land N \in ℤ \land M < N) \to ((M ..^N) = (J ..^K) \leftrightarrow (M = J \land N = K))$

Proof

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

Metamath Proof Explorer

Theorem fzoopth

Proof