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