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 )