Theorem elfzom1elp1fzo1

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

	Ref	Expression
Assertion	elfzom1elp1fzo1	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝐼 + 1 ) ∈ ( 1 ..^ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzoelz	⊢ ( 𝐼 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → 𝐼 ∈ ℤ )
2	1	zcnd	⊢ ( 𝐼 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → 𝐼 ∈ ℂ )
3		pncan1	⊢ ( 𝐼 ∈ ℂ → ( ( 𝐼 + 1 ) − 1 ) = 𝐼 )
4	2 3	syl	⊢ ( 𝐼 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → ( ( 𝐼 + 1 ) − 1 ) = 𝐼 )
5		id	⊢ ( 𝐼 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → 𝐼 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )
6	4 5	eqeltrd	⊢ ( 𝐼 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → ( ( 𝐼 + 1 ) − 1 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )
7	6	adantl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( ( 𝐼 + 1 ) − 1 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )
8	1	peano2zd	⊢ ( 𝐼 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) → ( 𝐼 + 1 ) ∈ ℤ )
9	8	anim1i	⊢ ( ( 𝐼 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐼 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
10	9	ancoms	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( ( 𝐼 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
11		elfzom1b	⊢ ( ( ( 𝐼 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐼 + 1 ) ∈ ( 1 ..^ 𝑁 ) ↔ ( ( 𝐼 + 1 ) − 1 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) )
12	10 11	syl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( ( 𝐼 + 1 ) ∈ ( 1 ..^ 𝑁 ) ↔ ( ( 𝐼 + 1 ) − 1 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) )
13	7 12	mpbird	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝐼 + 1 ) ∈ ( 1 ..^ 𝑁 ) )