Theorem elfzom1b

Description: An integer is a member of a 1-based finite set of sequential integers iff its predecessor is a member of the corresponding 0-based set. (Contributed by Mario Carneiro, 27-Sep-2015)

	Ref	Expression
Assertion	elfzom1b	|- ( ( K e. ZZ /\ N e. ZZ ) -> ( K e. ( 1 ..^ N ) <-> ( K - 1 ) e. ( 0 ..^ ( N - 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		peano2zm	|- ( N e. ZZ -> ( N - 1 ) e. ZZ )
2		elfzm1b	|- ( ( K e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( K e. ( 1 ... ( N - 1 ) ) <-> ( K - 1 ) e. ( 0 ... ( ( N - 1 ) - 1 ) ) ) )
3	1 2	sylan2	|- ( ( K e. ZZ /\ N e. ZZ ) -> ( K e. ( 1 ... ( N - 1 ) ) <-> ( K - 1 ) e. ( 0 ... ( ( N - 1 ) - 1 ) ) ) )
4		fzoval	|- ( N e. ZZ -> ( 1 ..^ N ) = ( 1 ... ( N - 1 ) ) )
5	4	adantl	|- ( ( K e. ZZ /\ N e. ZZ ) -> ( 1 ..^ N ) = ( 1 ... ( N - 1 ) ) )
6	5	eleq2d	|- ( ( K e. ZZ /\ N e. ZZ ) -> ( K e. ( 1 ..^ N ) <-> K e. ( 1 ... ( N - 1 ) ) ) )
7	1	adantl	|- ( ( K e. ZZ /\ N e. ZZ ) -> ( N - 1 ) e. ZZ )
8		fzoval	|- ( ( N - 1 ) e. ZZ -> ( 0 ..^ ( N - 1 ) ) = ( 0 ... ( ( N - 1 ) - 1 ) ) )
9	7 8	syl	|- ( ( K e. ZZ /\ N e. ZZ ) -> ( 0 ..^ ( N - 1 ) ) = ( 0 ... ( ( N - 1 ) - 1 ) ) )
10	9	eleq2d	|- ( ( K e. ZZ /\ N e. ZZ ) -> ( ( K - 1 ) e. ( 0 ..^ ( N - 1 ) ) <-> ( K - 1 ) e. ( 0 ... ( ( N - 1 ) - 1 ) ) ) )
11	3 6 10	3bitr4d	|- ( ( K e. ZZ /\ N e. ZZ ) -> ( K e. ( 1 ..^ N ) <-> ( K - 1 ) e. ( 0 ..^ ( N - 1 ) ) ) )