This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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