Theorem elfzo1elm1fzo0

Description: Membership of a positive integer decremented by one in a half-open range of nonnegative integers. (Contributed by AV, 20-Mar-2021)

	Ref	Expression
Assertion	elfzo1elm1fzo0	|- ( I e. ( 1 ..^ N ) -> ( I - 1 ) e. ( 0 ..^ ( N - 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfzoelz	|- ( I e. ( 1 ..^ N ) -> I e. ZZ )
2		elfzoel2	|- ( I e. ( 1 ..^ N ) -> N e. ZZ )
3	1 2	jca	|- ( I e. ( 1 ..^ N ) -> ( I e. ZZ /\ N e. ZZ ) )
4		elfzom1b	|- ( ( I e. ZZ /\ N e. ZZ ) -> ( I e. ( 1 ..^ N ) <-> ( I - 1 ) e. ( 0 ..^ ( N - 1 ) ) ) )
5	4	biimpd	|- ( ( I e. ZZ /\ N e. ZZ ) -> ( I e. ( 1 ..^ N ) -> ( I - 1 ) e. ( 0 ..^ ( N - 1 ) ) ) )
6	3 5	mpcom	|- ( I e. ( 1 ..^ N ) -> ( I - 1 ) e. ( 0 ..^ ( N - 1 ) ) )