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	⊢ ( 𝐼 ∈ ( 1 ..^ 𝑁 ) → ( 𝐼 − 1 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfzoelz	⊢ ( 𝐼 ∈ ( 1 ..^ 𝑁 ) → 𝐼 ∈ ℤ )
2		elfzoel2	⊢ ( 𝐼 ∈ ( 1 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
3	1 2	jca	⊢ ( 𝐼 ∈ ( 1 ..^ 𝑁 ) → ( 𝐼 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
4		elfzom1b	⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐼 ∈ ( 1 ..^ 𝑁 ) ↔ ( 𝐼 − 1 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) )
5	4	biimpd	⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐼 ∈ ( 1 ..^ 𝑁 ) → ( 𝐼 − 1 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) )
6	3 5	mpcom	⊢ ( 𝐼 ∈ ( 1 ..^ 𝑁 ) → ( 𝐼 − 1 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )