Step |
Hyp |
Ref |
Expression |
1 |
|
uzid |
|- ( M e. ZZ -> M e. ( ZZ>= ` M ) ) |
2 |
|
eleq2 |
|- ( ( ZZ>= ` M ) = ( ZZ>= ` N ) -> ( M e. ( ZZ>= ` M ) <-> M e. ( ZZ>= ` N ) ) ) |
3 |
|
eluzel2 |
|- ( M e. ( ZZ>= ` N ) -> N e. ZZ ) |
4 |
2 3
|
syl6bi |
|- ( ( ZZ>= ` M ) = ( ZZ>= ` N ) -> ( M e. ( ZZ>= ` M ) -> N e. ZZ ) ) |
5 |
1 4
|
mpan9 |
|- ( ( M e. ZZ /\ ( ZZ>= ` M ) = ( ZZ>= ` N ) ) -> N e. ZZ ) |
6 |
|
uzid |
|- ( N e. ZZ -> N e. ( ZZ>= ` N ) ) |
7 |
|
eleq2 |
|- ( ( ZZ>= ` M ) = ( ZZ>= ` N ) -> ( N e. ( ZZ>= ` M ) <-> N e. ( ZZ>= ` N ) ) ) |
8 |
6 7
|
syl5ibr |
|- ( ( ZZ>= ` M ) = ( ZZ>= ` N ) -> ( N e. ZZ -> N e. ( ZZ>= ` M ) ) ) |
9 |
|
eluzle |
|- ( N e. ( ZZ>= ` M ) -> M <_ N ) |
10 |
8 9
|
syl6 |
|- ( ( ZZ>= ` M ) = ( ZZ>= ` N ) -> ( N e. ZZ -> M <_ N ) ) |
11 |
1 2
|
syl5ib |
|- ( ( ZZ>= ` M ) = ( ZZ>= ` N ) -> ( M e. ZZ -> M e. ( ZZ>= ` N ) ) ) |
12 |
|
eluzle |
|- ( M e. ( ZZ>= ` N ) -> N <_ M ) |
13 |
11 12
|
syl6 |
|- ( ( ZZ>= ` M ) = ( ZZ>= ` N ) -> ( M e. ZZ -> N <_ M ) ) |
14 |
10 13
|
anim12d |
|- ( ( ZZ>= ` M ) = ( ZZ>= ` N ) -> ( ( N e. ZZ /\ M e. ZZ ) -> ( M <_ N /\ N <_ M ) ) ) |
15 |
14
|
impl |
|- ( ( ( ( ZZ>= ` M ) = ( ZZ>= ` N ) /\ N e. ZZ ) /\ M e. ZZ ) -> ( M <_ N /\ N <_ M ) ) |
16 |
15
|
ancoms |
|- ( ( M e. ZZ /\ ( ( ZZ>= ` M ) = ( ZZ>= ` N ) /\ N e. ZZ ) ) -> ( M <_ N /\ N <_ M ) ) |
17 |
16
|
anassrs |
|- ( ( ( M e. ZZ /\ ( ZZ>= ` M ) = ( ZZ>= ` N ) ) /\ N e. ZZ ) -> ( M <_ N /\ N <_ M ) ) |
18 |
|
zre |
|- ( M e. ZZ -> M e. RR ) |
19 |
|
zre |
|- ( N e. ZZ -> N e. RR ) |
20 |
|
letri3 |
|- ( ( M e. RR /\ N e. RR ) -> ( M = N <-> ( M <_ N /\ N <_ M ) ) ) |
21 |
18 19 20
|
syl2an |
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M = N <-> ( M <_ N /\ N <_ M ) ) ) |
22 |
21
|
adantlr |
|- ( ( ( M e. ZZ /\ ( ZZ>= ` M ) = ( ZZ>= ` N ) ) /\ N e. ZZ ) -> ( M = N <-> ( M <_ N /\ N <_ M ) ) ) |
23 |
17 22
|
mpbird |
|- ( ( ( M e. ZZ /\ ( ZZ>= ` M ) = ( ZZ>= ` N ) ) /\ N e. ZZ ) -> M = N ) |
24 |
5 23
|
mpdan |
|- ( ( M e. ZZ /\ ( ZZ>= ` M ) = ( ZZ>= ` N ) ) -> M = N ) |
25 |
24
|
ex |
|- ( M e. ZZ -> ( ( ZZ>= ` M ) = ( ZZ>= ` N ) -> M = N ) ) |
26 |
|
fveq2 |
|- ( M = N -> ( ZZ>= ` M ) = ( ZZ>= ` N ) ) |
27 |
25 26
|
impbid1 |
|- ( M e. ZZ -> ( ( ZZ>= ` M ) = ( ZZ>= ` N ) <-> M = N ) ) |