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

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	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑋 + 1 ) ∈ ( 0 ..^ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
2		elfzom1elp1fzo	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑋 + 1 ) ∈ ( 0 ..^ 𝑁 ) )
3	1 2	sylan	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → ( 𝑋 + 1 ) ∈ ( 0 ..^ 𝑁 ) )