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 ) |