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