This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ..^ 𝑁 ) )