Metamath Proof Explorer

Theorem zextle

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

Ref Expression
Assertion zextle ⊢M∈ℤ∧N∈ℤ∧∀k∈ℤk≤M↔k≤N→M=N

Proof

Step Hyp Ref Expression
1 zre ⊢M∈ℤ→M∈ℝ
2 1 leidd ⊢M∈ℤ→M≤M
3 2 adantr ⊢M∈ℤ∧∀k∈ℤk≤M↔k≤N→M≤M
4 breq1 ⊢k=M→k≤M↔M≤M
5 breq1 ⊢k=M→k≤N↔M≤N
6 4 5 bibi12d ⊢k=M→k≤M↔k≤N↔M≤M↔M≤N
7 6 rspcva ⊢M∈ℤ∧∀k∈ℤk≤M↔k≤N→M≤M↔M≤N
8 3 7 mpbid ⊢M∈ℤ∧∀k∈ℤk≤M↔k≤N→M≤N
9 8 adantlr ⊢M∈ℤ∧N∈ℤ∧∀k∈ℤk≤M↔k≤N→M≤N
10 zre ⊢N∈ℤ→N∈ℝ
11 10 leidd ⊢N∈ℤ→N≤N
12 11 adantr ⊢N∈ℤ∧∀k∈ℤk≤M↔k≤N→N≤N
13 breq1 ⊢k=N→k≤M↔N≤M
14 breq1 ⊢k=N→k≤N↔N≤N
15 13 14 bibi12d ⊢k=N→k≤M↔k≤N↔N≤M↔N≤N
16 15 rspcva ⊢N∈ℤ∧∀k∈ℤk≤M↔k≤N→N≤M↔N≤N
17 12 16 mpbird ⊢N∈ℤ∧∀k∈ℤk≤M↔k≤N→N≤M
18 17 adantll ⊢M∈ℤ∧N∈ℤ∧∀k∈ℤk≤M↔k≤N→N≤M
19 9 18 jca ⊢M∈ℤ∧N∈ℤ∧∀k∈ℤk≤M↔k≤N→M≤N∧N≤M
20 19 ex ⊢M∈ℤ∧N∈ℤ→∀k∈ℤk≤M↔k≤N→M≤N∧N≤M
21 letri3 ⊢M∈ℝ∧N∈ℝ→M=N↔M≤N∧N≤M
22 1 10 21 syl2an ⊢M∈ℤ∧N∈ℤ→M=N↔M≤N∧N≤M
23 20 22 sylibrd ⊢M∈ℤ∧N∈ℤ→∀k∈ℤk≤M↔k≤N→M=N
24 23 3impia ⊢M∈ℤ∧N∈ℤ∧∀k∈ℤk≤M↔k≤N→M=N