Metamath Proof Explorer


Theorem elfz1b

Description: Membership in a 1-based finite set of sequential integers. (Contributed by AV, 30-Oct-2018) (Proof shortened by AV, 23-Jan-2022)

Ref Expression
Assertion elfz1b
|- ( N e. ( 1 ... M ) <-> ( N e. NN /\ M e. NN /\ N <_ M ) )

Proof

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