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