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