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

Metamath Proof Explorer

Theorem fznatpl1

Description: Shift membership in a finite sequence of naturals. (Contributed by Scott Fenton, 17-Jul-2013)

Ref Expression
Assertion fznatpl1 
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( I + 1 ) e. ( 1 ... N ) )

Proof

Step Hyp Ref Expression
1 1red 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> 1 e. RR )
2 elfzelz 
 |-  ( I e. ( 1 ... ( N - 1 ) ) -> I e. ZZ )
3 2 zred 
 |-  ( I e. ( 1 ... ( N - 1 ) ) -> I e. RR )
4 3 adantl 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> I e. RR )
5 peano2re 
 |-  ( I e. RR -> ( I + 1 ) e. RR )
6 4 5 syl 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( I + 1 ) e. RR )
7 peano2re 
 |-  ( 1 e. RR -> ( 1 + 1 ) e. RR )
8 1 7 syl 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( 1 + 1 ) e. RR )
9 1 ltp1d 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> 1 < ( 1 + 1 ) )
10 elfzle1 
 |-  ( I e. ( 1 ... ( N - 1 ) ) -> 1 <_ I )
11 10 adantl 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> 1 <_ I )
12 1re 
 |-  1 e. RR
13 leadd1 
 |-  ( ( 1 e. RR /\ I e. RR /\ 1 e. RR ) -> ( 1 <_ I <-> ( 1 + 1 ) <_ ( I + 1 ) ) )
14 12 12 13 mp3an13 
 |-  ( I e. RR -> ( 1 <_ I <-> ( 1 + 1 ) <_ ( I + 1 ) ) )
15 4 14 syl 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( 1 <_ I <-> ( 1 + 1 ) <_ ( I + 1 ) ) )
16 11 15 mpbid 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( 1 + 1 ) <_ ( I + 1 ) )
17 1 8 6 9 16 ltletrd 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> 1 < ( I + 1 ) )
18 1 6 17 ltled 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> 1 <_ ( I + 1 ) )
19 elfzle2 
 |-  ( I e. ( 1 ... ( N - 1 ) ) -> I <_ ( N - 1 ) )
20 19 adantl 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> I <_ ( N - 1 ) )
21 nnz 
 |-  ( N e. NN -> N e. ZZ )
22 21 adantr 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> N e. ZZ )
23 22 zred 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> N e. RR )
24 leaddsub 
 |-  ( ( I e. RR /\ 1 e. RR /\ N e. RR ) -> ( ( I + 1 ) <_ N <-> I <_ ( N - 1 ) ) )
25 12 24 mp3an2 
 |-  ( ( I e. RR /\ N e. RR ) -> ( ( I + 1 ) <_ N <-> I <_ ( N - 1 ) ) )
26 3 23 25 syl2an2 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( ( I + 1 ) <_ N <-> I <_ ( N - 1 ) ) )
27 20 26 mpbird 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( I + 1 ) <_ N )
28 2 peano2zd 
 |-  ( I e. ( 1 ... ( N - 1 ) ) -> ( I + 1 ) e. ZZ )
29 1z 
 |-  1 e. ZZ
30 elfz 
 |-  ( ( ( I + 1 ) e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( ( I + 1 ) e. ( 1 ... N ) <-> ( 1 <_ ( I + 1 ) /\ ( I + 1 ) <_ N ) ) )
31 29 30 mp3an2 
 |-  ( ( ( I + 1 ) e. ZZ /\ N e. ZZ ) -> ( ( I + 1 ) e. ( 1 ... N ) <-> ( 1 <_ ( I + 1 ) /\ ( I + 1 ) <_ N ) ) )
32 28 22 31 syl2an2 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( ( I + 1 ) e. ( 1 ... N ) <-> ( 1 <_ ( I + 1 ) /\ ( I + 1 ) <_ N ) ) )
33 18 27 32 mpbir2and 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( I + 1 ) e. ( 1 ... N ) )