This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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