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