Metamath Proof Explorer

Theorem fzopth

Description: A finite set of sequential integers has the ordered pair property (compare opth ) under certain conditions. (Contributed by NM, 31-Oct-2005) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fzopth ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ↔ ( 𝑀 = 𝐽 ∧ 𝑁 = 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
2 1 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
3 simpr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) )
4 2 3 eleqtrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → 𝑀 ∈ ( 𝐽 ... 𝐾 ) )
5 elfzuz ⊢ ( 𝑀 ∈ ( 𝐽 ... 𝐾 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝐽 ) )
6 uzss ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝐽 ) → ( ℤ≥ ‘ 𝑀 ) ⊆ ( ℤ≥ ‘ 𝐽 ) )
7 4 5 6 3syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → ( ℤ≥ ‘ 𝑀 ) ⊆ ( ℤ≥ ‘ 𝐽 ) )
8 elfzuz2 ⊢ ( 𝑀 ∈ ( 𝐽 ... 𝐾 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝐽 ) )
9 eluzfz1 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝐽 ) → 𝐽 ∈ ( 𝐽 ... 𝐾 ) )
10 4 8 9 3syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → 𝐽 ∈ ( 𝐽 ... 𝐾 ) )
11 10 3 eleqtrrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → 𝐽 ∈ ( 𝑀 ... 𝑁 ) )
12 elfzuz ⊢ ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) → 𝐽 ∈ ( ℤ≥ ‘ 𝑀 ) )
13 uzss ⊢ ( 𝐽 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝐽 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
14 11 12 13 3syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → ( ℤ≥ ‘ 𝐽 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
15 7 14 eqssd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝐽 ) )
16 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
17 16 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → 𝑀 ∈ ℤ )
18 uz11 ⊢ ( 𝑀 ∈ ℤ → ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝐽 ) ↔ 𝑀 = 𝐽 ) )
19 17 18 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝐽 ) ↔ 𝑀 = 𝐽 ) )
20 15 19 mpbid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → 𝑀 = 𝐽 )
21 eluzfz2 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝐽 ) → 𝐾 ∈ ( 𝐽 ... 𝐾 ) )
22 4 8 21 3syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → 𝐾 ∈ ( 𝐽 ... 𝐾 ) )
23 22 3 eleqtrrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )
24 elfzuz3 ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
25 uzss ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝐾 ) )
26 23 24 25 3syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝐾 ) )
27 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
28 27 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
29 28 3 eleqtrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → 𝑁 ∈ ( 𝐽 ... 𝐾 ) )
30 elfzuz3 ⊢ ( 𝑁 ∈ ( 𝐽 ... 𝐾 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) )
31 uzss ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ℤ≥ ‘ 𝐾 ) ⊆ ( ℤ≥ ‘ 𝑁 ) )
32 29 30 31 3syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → ( ℤ≥ ‘ 𝐾 ) ⊆ ( ℤ≥ ‘ 𝑁 ) )
33 26 32 eqssd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝐾 ) )
34 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
35 34 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → 𝑁 ∈ ℤ )
36 uz11 ⊢ ( 𝑁 ∈ ℤ → ( ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝐾 ) ↔ 𝑁 = 𝐾 ) )
37 35 36 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → ( ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝐾 ) ↔ 𝑁 = 𝐾 ) )
38 33 37 mpbid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → 𝑁 = 𝐾 )
39 20 38 jca ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ) → ( 𝑀 = 𝐽 ∧ 𝑁 = 𝐾 ) )
40 39 ex ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) → ( 𝑀 = 𝐽 ∧ 𝑁 = 𝐾 ) ) )
41 oveq12 ⊢ ( ( 𝑀 = 𝐽 ∧ 𝑁 = 𝐾 ) → ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) )
42 40 41 impbid1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 ... 𝑁 ) = ( 𝐽 ... 𝐾 ) ↔ ( 𝑀 = 𝐽 ∧ 𝑁 = 𝐾 ) ) )