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