Metamath Proof Explorer

Theorem zextlt

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

Ref Expression
Assertion zextlt ⊢M∈ℤ∧N∈ℤ∧∀k∈ℤk<M↔k<N→M=N

Proof

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