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

Metamath Proof Explorer

Theorem zextlt

Description: An extensionality-like property for integer ordering. (Contributed by NM, 29-Oct-2005)

Ref Expression
Assertion zextlt ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ∀ 𝑘 ∈ ℤ ( 𝑘 < 𝑀 ↔ 𝑘 < 𝑁 ) ) → 𝑀 = 𝑁 )

Proof

Step Hyp Ref Expression
1 zltlem1 ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑘 < 𝑀 ↔ 𝑘 ≤ ( 𝑀 − 1 ) ) )
2 1 adantrr ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑘 < 𝑀 ↔ 𝑘 ≤ ( 𝑀 − 1 ) ) )
3 zltlem1 ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑘 < 𝑁 ↔ 𝑘 ≤ ( 𝑁 − 1 ) ) )
4 3 adantrl ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑘 < 𝑁 ↔ 𝑘 ≤ ( 𝑁 − 1 ) ) )
5 2 4 bibi12d ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑘 < 𝑀 ↔ 𝑘 < 𝑁 ) ↔ ( 𝑘 ≤ ( 𝑀 − 1 ) ↔ 𝑘 ≤ ( 𝑁 − 1 ) ) ) )
6 5 ancoms ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑘 < 𝑀 ↔ 𝑘 < 𝑁 ) ↔ ( 𝑘 ≤ ( 𝑀 − 1 ) ↔ 𝑘 ≤ ( 𝑁 − 1 ) ) ) )
7 6 ralbidva ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ∀ 𝑘 ∈ ℤ ( 𝑘 < 𝑀 ↔ 𝑘 < 𝑁 ) ↔ ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ ( 𝑀 − 1 ) ↔ 𝑘 ≤ ( 𝑁 − 1 ) ) ) )
8 peano2zm ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 − 1 ) ∈ ℤ )
9 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
10 zextle ⊢ ( ( ( 𝑀 − 1 ) ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ∧ ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ ( 𝑀 − 1 ) ↔ 𝑘 ≤ ( 𝑁 − 1 ) ) ) → ( 𝑀 − 1 ) = ( 𝑁 − 1 ) )
11 10 3expia ⊢ ( ( ( 𝑀 − 1 ) ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ ( 𝑀 − 1 ) ↔ 𝑘 ≤ ( 𝑁 − 1 ) ) → ( 𝑀 − 1 ) = ( 𝑁 − 1 ) ) )
12 8 9 11 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ ( 𝑀 − 1 ) ↔ 𝑘 ≤ ( 𝑁 − 1 ) ) → ( 𝑀 − 1 ) = ( 𝑁 − 1 ) ) )
13 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
14 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
15 ax-1cn ⊢ 1 ∈ ℂ
16 subcan2 ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 − 1 ) = ( 𝑁 − 1 ) ↔ 𝑀 = 𝑁 ) )
17 15 16 mp3an3 ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑀 − 1 ) = ( 𝑁 − 1 ) ↔ 𝑀 = 𝑁 ) )
18 13 14 17 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 − 1 ) = ( 𝑁 − 1 ) ↔ 𝑀 = 𝑁 ) )
19 12 18 sylibd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ ( 𝑀 − 1 ) ↔ 𝑘 ≤ ( 𝑁 − 1 ) ) → 𝑀 = 𝑁 ) )
20 7 19 sylbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ∀ 𝑘 ∈ ℤ ( 𝑘 < 𝑀 ↔ 𝑘 < 𝑁 ) → 𝑀 = 𝑁 ) )
21 20 3impia ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ∀ 𝑘 ∈ ℤ ( 𝑘 < 𝑀 ↔ 𝑘 < 𝑁 ) ) → 𝑀 = 𝑁 )