Metamath Proof Explorer

Theorem elfzom1p1elfzo

Description: Increasing an element of a half-open range of nonnegative integers by 1 results in an element of the half-open range of nonnegative integers with an upper bound increased by 1. (Contributed by Alexander van der Vekens, 1-Aug-2018) (Proof shortened by Thierry Arnoux, 14-Dec-2023)

Ref Expression
Assertion elfzom1p1elfzo ⊢ N ∈ ℕ ∧ X ∈ 0 ..^ N − 1 → X + 1 ∈ 0 ..^ N

Proof

Step Hyp Ref Expression
1 nnz ⊢ N ∈ ℕ → N ∈ ℤ
2 elfzom1elp1fzo ⊢ N ∈ ℤ ∧ X ∈ 0 ..^ N − 1 → X + 1 ∈ 0 ..^ N
3 1 2 sylan ⊢ N ∈ ℕ ∧ X ∈ 0 ..^ N − 1 → X + 1 ∈ 0 ..^ N