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 ⊢ N ∈ ℤ ∧ I ∈ 0 ..^ N − 1 → I + 1 ∈ 1 ..^ N

Proof

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