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	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ∀ 𝑘 ∈ ℤ ( 𝑘 < 𝑀 ↔ 𝑘 < 𝑁 ) ) → 𝑀 = 𝑁 )