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 \in (1 ..^N) \to I - 1 \in (0 ..^N - 1)$

Step	Hyp	Ref	Expression
1		elfzoelz	$⊢ I \in (1 ..^N) \to I \in ℤ$
2		elfzoel2	$⊢ I \in (1 ..^N) \to N \in ℤ$
3	1 2	jca	$⊢ I \in (1 ..^N) \to (I \in ℤ \land N \in ℤ)$
4		elfzom1b	$⊢ (I \in ℤ \land N \in ℤ) \to (I \in (1 ..^N) \leftrightarrow I - 1 \in (0 ..^N - 1))$
5	4	biimpd	$⊢ (I \in ℤ \land N \in ℤ) \to (I \in (1 ..^N) \to I - 1 \in (0 ..^N - 1))$
6	3 5	mpcom	$⊢ I \in (1 ..^N) \to I - 1 \in (0 ..^N - 1)$

Metamath Proof Explorer