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