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	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ↔ ( 𝑀 = 𝐽 ∧ 𝑁 = 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fzolb	⊢ ( 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) )
2	1	biranri	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) )
3		simpr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) )
4	2 3	eleqtrd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → 𝑀 ∈ ( 𝐽 ..^ 𝐾 ) )
5		elfzouz	⊢ ( 𝑀 ∈ ( 𝐽 ..^ 𝐾 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝐽 ) )
6		uzss	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝐽 ) → ( ℤ≥ ‘ 𝑀 ) ⊆ ( ℤ≥ ‘ 𝐽 ) )
7	4 5 6	3syl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → ( ℤ≥ ‘ 𝑀 ) ⊆ ( ℤ≥ ‘ 𝐽 ) )
8		eleq2	⊢ ( ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) → ( 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) ↔ 𝑀 ∈ ( 𝐽 ..^ 𝐾 ) ) )
9	8	adantl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → ( 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) ↔ 𝑀 ∈ ( 𝐽 ..^ 𝐾 ) ) )
10	2 9	mpbid	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → 𝑀 ∈ ( 𝐽 ..^ 𝐾 ) )
11		elfzolt3b	⊢ ( 𝑀 ∈ ( 𝐽 ..^ 𝐾 ) → 𝐽 ∈ ( 𝐽 ..^ 𝐾 ) )
12	10 11	syl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → 𝐽 ∈ ( 𝐽 ..^ 𝐾 ) )
13	12 3	eleqtrrd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) )
14		elfzouz	⊢ ( 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐽 ∈ ( ℤ≥ ‘ 𝑀 ) )
15		uzss	⊢ ( 𝐽 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝐽 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
16	13 14 15	3syl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → ( ℤ≥ ‘ 𝐽 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
17	7 16	eqssd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝐽 ) )
18		simpl1	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → 𝑀 ∈ ℤ )
19		uz11	⊢ ( 𝑀 ∈ ℤ → ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝐽 ) ↔ 𝑀 = 𝐽 ) )
20	18 19	syl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝐽 ) ↔ 𝑀 = 𝐽 ) )
21	17 20	mpbid	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → 𝑀 = 𝐽 )
22		fzoend	⊢ ( 𝐽 ∈ ( 𝐽 ..^ 𝐾 ) → ( 𝐾 − 1 ) ∈ ( 𝐽 ..^ 𝐾 ) )
23		elfzoel2	⊢ ( ( 𝐾 − 1 ) ∈ ( 𝐽 ..^ 𝐾 ) → 𝐾 ∈ ℤ )
24		eleq2	⊢ ( ( 𝐽 ..^ 𝐾 ) = ( 𝑀 ..^ 𝑁 ) → ( ( 𝐾 − 1 ) ∈ ( 𝐽 ..^ 𝐾 ) ↔ ( 𝐾 − 1 ) ∈ ( 𝑀 ..^ 𝑁 ) ) )
25	24	eqcoms	⊢ ( ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) → ( ( 𝐾 − 1 ) ∈ ( 𝐽 ..^ 𝐾 ) ↔ ( 𝐾 − 1 ) ∈ ( 𝑀 ..^ 𝑁 ) ) )
26		elfzo2	⊢ ( ( 𝐾 − 1 ) ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( ( 𝐾 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 − 1 ) < 𝑁 ) )
27		simpl	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐾 − 1 ) < 𝑁 ) ) → 𝐾 ∈ ℤ )
28		simprl	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐾 − 1 ) < 𝑁 ) ) → 𝑁 ∈ ℤ )
29		zlem1lt	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ≤ 𝑁 ↔ ( 𝐾 − 1 ) < 𝑁 ) )
30	29	ancoms	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ≤ 𝑁 ↔ ( 𝐾 − 1 ) < 𝑁 ) )
31	30	biimprd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 − 1 ) < 𝑁 → 𝐾 ≤ 𝑁 ) )
32	31	impancom	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐾 − 1 ) < 𝑁 ) → ( 𝐾 ∈ ℤ → 𝐾 ≤ 𝑁 ) )
33	32	impcom	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐾 − 1 ) < 𝑁 ) ) → 𝐾 ≤ 𝑁 )
34	27 28 33	3jca	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐾 − 1 ) < 𝑁 ) ) → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) )
35	34	expcom	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐾 − 1 ) < 𝑁 ) → ( 𝐾 ∈ ℤ → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) ) )
36	35	3adant1	⊢ ( ( ( 𝐾 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 − 1 ) < 𝑁 ) → ( 𝐾 ∈ ℤ → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) ) )
37	36	a1d	⊢ ( ( ( 𝐾 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 − 1 ) < 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( 𝐾 ∈ ℤ → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) ) ) )
38	26 37	sylbi	⊢ ( ( 𝐾 − 1 ) ∈ ( 𝑀 ..^ 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( 𝐾 ∈ ℤ → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) ) ) )
39	25 38	biimtrdi	⊢ ( ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) → ( ( 𝐾 − 1 ) ∈ ( 𝐽 ..^ 𝐾 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( 𝐾 ∈ ℤ → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) ) ) ) )
40	39	com23	⊢ ( ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( ( 𝐾 − 1 ) ∈ ( 𝐽 ..^ 𝐾 ) → ( 𝐾 ∈ ℤ → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) ) ) ) )
41	40	impcom	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → ( ( 𝐾 − 1 ) ∈ ( 𝐽 ..^ 𝐾 ) → ( 𝐾 ∈ ℤ → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) ) ) )
42	41	com13	⊢ ( 𝐾 ∈ ℤ → ( ( 𝐾 − 1 ) ∈ ( 𝐽 ..^ 𝐾 ) → ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) ) ) )
43	23 42	mpcom	⊢ ( ( 𝐾 − 1 ) ∈ ( 𝐽 ..^ 𝐾 ) → ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) ) )
44	22 43	syl	⊢ ( 𝐽 ∈ ( 𝐽 ..^ 𝐾 ) → ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) ) )
45	12 44	mpcom	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) )
46		eluz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) )
47	46	biimpri	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
48		uzss	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝐾 ) )
49	45 47 48	3syl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝐾 ) )
50	1	biimpri	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) )
51		fzoend	⊢ ( 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑁 − 1 ) ∈ ( 𝑀 ..^ 𝑁 ) )
52		eleq2	⊢ ( ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) → ( ( 𝑁 − 1 ) ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑁 − 1 ) ∈ ( 𝐽 ..^ 𝐾 ) ) )
53		elfzo2	⊢ ( ( 𝑁 − 1 ) ∈ ( 𝐽 ..^ 𝐾 ) ↔ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝐽 ) ∧ 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) )
54		pm3.2	⊢ ( 𝑁 ∈ ℤ → ( ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) → ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) ) ) )
55	54	3ad2ant2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) → ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) ) ) )
56	55	com12	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) ) ) )
57	56	3adant1	⊢ ( ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝐽 ) ∧ 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) ) ) )
58	53 57	sylbi	⊢ ( ( 𝑁 − 1 ) ∈ ( 𝐽 ..^ 𝐾 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) ) ) )
59	52 58	biimtrdi	⊢ ( ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) → ( ( 𝑁 − 1 ) ∈ ( 𝑀 ..^ 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) ) ) ) )
60	59	com3l	⊢ ( ( 𝑁 − 1 ) ∈ ( 𝑀 ..^ 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) → ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) ) ) ) )
61	51 60	syl	⊢ ( 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) → ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) ) ) ) )
62	50 61	mpcom	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) → ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) ) ) )
63	62	imp	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) ) )
64		simpl	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) ) → 𝑁 ∈ ℤ )
65		simprl	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) ) → 𝐾 ∈ ℤ )
66		zlem1lt	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 ≤ 𝐾 ↔ ( 𝑁 − 1 ) < 𝐾 ) )
67	66	ancoms	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ≤ 𝐾 ↔ ( 𝑁 − 1 ) < 𝐾 ) )
68	67	biimprd	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 − 1 ) < 𝐾 → 𝑁 ≤ 𝐾 ) )
69	68	impancom	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) → ( 𝑁 ∈ ℤ → 𝑁 ≤ 𝐾 ) )
70	69	impcom	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) ) → 𝑁 ≤ 𝐾 )
71		eluz2	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ≤ 𝐾 ) )
72	64 65 70 71	syl3anbrc	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) < 𝐾 ) ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) )
73		uzss	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ℤ≥ ‘ 𝐾 ) ⊆ ( ℤ≥ ‘ 𝑁 ) )
74	63 72 73	3syl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → ( ℤ≥ ‘ 𝐾 ) ⊆ ( ℤ≥ ‘ 𝑁 ) )
75	49 74	eqssd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝐾 ) )
76		simpl2	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → 𝑁 ∈ ℤ )
77		uz11	⊢ ( 𝑁 ∈ ℤ → ( ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝐾 ) ↔ 𝑁 = 𝐾 ) )
78	76 77	syl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → ( ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝐾 ) ↔ 𝑁 = 𝐾 ) )
79	75 78	mpbid	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → 𝑁 = 𝐾 )
80	21 79	jca	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ∧ ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ) → ( 𝑀 = 𝐽 ∧ 𝑁 = 𝐾 ) )
81	80	ex	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) → ( 𝑀 = 𝐽 ∧ 𝑁 = 𝐾 ) ) )
82		oveq12	⊢ ( ( 𝑀 = 𝐽 ∧ 𝑁 = 𝐾 ) → ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) )
83	81 82	impbid1	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → ( ( 𝑀 ..^ 𝑁 ) = ( 𝐽 ..^ 𝐾 ) ↔ ( 𝑀 = 𝐽 ∧ 𝑁 = 𝐾 ) ) )