Step |
Hyp |
Ref |
Expression |
1 |
|
elfz2 |
|- ( N e. ( 1 ... M ) <-> ( ( 1 e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 <_ N /\ N <_ M ) ) ) |
2 |
|
simpl2 |
|- ( ( ( 1 e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 <_ N /\ N <_ M ) ) -> M e. ZZ ) |
3 |
|
1red |
|- ( ( 1 e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> 1 e. RR ) |
4 |
|
zre |
|- ( N e. ZZ -> N e. RR ) |
5 |
4
|
3ad2ant3 |
|- ( ( 1 e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> N e. RR ) |
6 |
|
zre |
|- ( M e. ZZ -> M e. RR ) |
7 |
6
|
3ad2ant2 |
|- ( ( 1 e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> M e. RR ) |
8 |
|
letr |
|- ( ( 1 e. RR /\ N e. RR /\ M e. RR ) -> ( ( 1 <_ N /\ N <_ M ) -> 1 <_ M ) ) |
9 |
3 5 7 8
|
syl3anc |
|- ( ( 1 e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( 1 <_ N /\ N <_ M ) -> 1 <_ M ) ) |
10 |
9
|
imp |
|- ( ( ( 1 e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 <_ N /\ N <_ M ) ) -> 1 <_ M ) |
11 |
|
elnnz1 |
|- ( M e. NN <-> ( M e. ZZ /\ 1 <_ M ) ) |
12 |
2 10 11
|
sylanbrc |
|- ( ( ( 1 e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 <_ N /\ N <_ M ) ) -> M e. NN ) |
13 |
1 12
|
sylbi |
|- ( N e. ( 1 ... M ) -> M e. NN ) |
14 |
|
elfzel2 |
|- ( N e. ( 1 ... M ) -> M e. ZZ ) |
15 |
|
fznn |
|- ( M e. ZZ -> ( N e. ( 1 ... M ) <-> ( N e. NN /\ N <_ M ) ) ) |
16 |
15
|
biimpd |
|- ( M e. ZZ -> ( N e. ( 1 ... M ) -> ( N e. NN /\ N <_ M ) ) ) |
17 |
14 16
|
mpcom |
|- ( N e. ( 1 ... M ) -> ( N e. NN /\ N <_ M ) ) |
18 |
|
3anan12 |
|- ( ( N e. NN /\ M e. NN /\ N <_ M ) <-> ( M e. NN /\ ( N e. NN /\ N <_ M ) ) ) |
19 |
13 17 18
|
sylanbrc |
|- ( N e. ( 1 ... M ) -> ( N e. NN /\ M e. NN /\ N <_ M ) ) |
20 |
|
nnz |
|- ( M e. NN -> M e. ZZ ) |
21 |
20 15
|
syl |
|- ( M e. NN -> ( N e. ( 1 ... M ) <-> ( N e. NN /\ N <_ M ) ) ) |
22 |
21
|
biimprd |
|- ( M e. NN -> ( ( N e. NN /\ N <_ M ) -> N e. ( 1 ... M ) ) ) |
23 |
22
|
expd |
|- ( M e. NN -> ( N e. NN -> ( N <_ M -> N e. ( 1 ... M ) ) ) ) |
24 |
23
|
3imp21 |
|- ( ( N e. NN /\ M e. NN /\ N <_ M ) -> N e. ( 1 ... M ) ) |
25 |
19 24
|
impbii |
|- ( N e. ( 1 ... M ) <-> ( N e. NN /\ M e. NN /\ N <_ M ) ) |