Step |
Hyp |
Ref |
Expression |
1 |
|
zre |
|- ( M e. ZZ -> M e. RR ) |
2 |
1
|
leidd |
|- ( M e. ZZ -> M <_ M ) |
3 |
2
|
adantr |
|- ( ( M e. ZZ /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> M <_ M ) |
4 |
|
breq1 |
|- ( k = M -> ( k <_ M <-> M <_ M ) ) |
5 |
|
breq1 |
|- ( k = M -> ( k <_ N <-> M <_ N ) ) |
6 |
4 5
|
bibi12d |
|- ( k = M -> ( ( k <_ M <-> k <_ N ) <-> ( M <_ M <-> M <_ N ) ) ) |
7 |
6
|
rspcva |
|- ( ( M e. ZZ /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> ( M <_ M <-> M <_ N ) ) |
8 |
3 7
|
mpbid |
|- ( ( M e. ZZ /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> M <_ N ) |
9 |
8
|
adantlr |
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> M <_ N ) |
10 |
|
zre |
|- ( N e. ZZ -> N e. RR ) |
11 |
10
|
leidd |
|- ( N e. ZZ -> N <_ N ) |
12 |
11
|
adantr |
|- ( ( N e. ZZ /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> N <_ N ) |
13 |
|
breq1 |
|- ( k = N -> ( k <_ M <-> N <_ M ) ) |
14 |
|
breq1 |
|- ( k = N -> ( k <_ N <-> N <_ N ) ) |
15 |
13 14
|
bibi12d |
|- ( k = N -> ( ( k <_ M <-> k <_ N ) <-> ( N <_ M <-> N <_ N ) ) ) |
16 |
15
|
rspcva |
|- ( ( N e. ZZ /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> ( N <_ M <-> N <_ N ) ) |
17 |
12 16
|
mpbird |
|- ( ( N e. ZZ /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> N <_ M ) |
18 |
17
|
adantll |
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> N <_ M ) |
19 |
9 18
|
jca |
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> ( M <_ N /\ N <_ M ) ) |
20 |
19
|
ex |
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( A. k e. ZZ ( k <_ M <-> k <_ N ) -> ( M <_ N /\ N <_ M ) ) ) |
21 |
|
letri3 |
|- ( ( M e. RR /\ N e. RR ) -> ( M = N <-> ( M <_ N /\ N <_ M ) ) ) |
22 |
1 10 21
|
syl2an |
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M = N <-> ( M <_ N /\ N <_ M ) ) ) |
23 |
20 22
|
sylibrd |
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( A. k e. ZZ ( k <_ M <-> k <_ N ) -> M = N ) ) |
24 |
23
|
3impia |
|- ( ( M e. ZZ /\ N e. ZZ /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> M = N ) |