Metamath Proof Explorer

Theorem zextlt

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

Ref Expression
Assertion zextlt 
|- ( ( M e. ZZ /\ N e. ZZ /\ A. k e. ZZ ( k < M <-> k < N ) ) -> M = N )

Proof

Step Hyp Ref Expression
1 zltlem1 
 |-  ( ( k e. ZZ /\ M e. ZZ ) -> ( k < M <-> k <_ ( M - 1 ) ) )
2 1 adantrr 
 |-  ( ( k e. ZZ /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( k < M <-> k <_ ( M - 1 ) ) )
3 zltlem1 
 |-  ( ( k e. ZZ /\ N e. ZZ ) -> ( k < N <-> k <_ ( N - 1 ) ) )
4 3 adantrl 
 |-  ( ( k e. ZZ /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( k < N <-> k <_ ( N - 1 ) ) )
5 2 4 bibi12d 
 |-  ( ( k e. ZZ /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( k < M <-> k < N ) <-> ( k <_ ( M - 1 ) <-> k <_ ( N - 1 ) ) ) )
6 5 ancoms 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ k e. ZZ ) -> ( ( k < M <-> k < N ) <-> ( k <_ ( M - 1 ) <-> k <_ ( N - 1 ) ) ) )
7 6 ralbidva 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( A. k e. ZZ ( k < M <-> k < N ) <-> A. k e. ZZ ( k <_ ( M - 1 ) <-> k <_ ( N - 1 ) ) ) )
8 peano2zm 
 |-  ( M e. ZZ -> ( M - 1 ) e. ZZ )
9 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
10 zextle 
 |-  ( ( ( M - 1 ) e. ZZ /\ ( N - 1 ) e. ZZ /\ A. k e. ZZ ( k <_ ( M - 1 ) <-> k <_ ( N - 1 ) ) ) -> ( M - 1 ) = ( N - 1 ) )
11 10 3expia 
 |-  ( ( ( M - 1 ) e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( A. k e. ZZ ( k <_ ( M - 1 ) <-> k <_ ( N - 1 ) ) -> ( M - 1 ) = ( N - 1 ) ) )
12 8 9 11 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( A. k e. ZZ ( k <_ ( M - 1 ) <-> k <_ ( N - 1 ) ) -> ( M - 1 ) = ( N - 1 ) ) )
13 zcn 
 |-  ( M e. ZZ -> M e. CC )
14 zcn 
 |-  ( N e. ZZ -> N e. CC )
15 ax-1cn 
 |-  1 e. CC
16 subcan2 
 |-  ( ( M e. CC /\ N e. CC /\ 1 e. CC ) -> ( ( M - 1 ) = ( N - 1 ) <-> M = N ) )
17 15 16 mp3an3 
 |-  ( ( M e. CC /\ N e. CC ) -> ( ( M - 1 ) = ( N - 1 ) <-> M = N ) )
18 13 14 17 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M - 1 ) = ( N - 1 ) <-> M = N ) )
19 12 18 sylibd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( A. k e. ZZ ( k <_ ( M - 1 ) <-> k <_ ( N - 1 ) ) -> M = N ) )
20 7 19 sylbid 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( A. k e. ZZ ( k < M <-> k < N ) -> M = N ) )
21 20 3impia 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A. k e. ZZ ( k < M <-> k < N ) ) -> M = N )