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

Metamath Proof Explorer

Theorem fzonn0p1p1

Description: If a nonnegative integer is an element of a half-open range of nonnegative integers, increasing this integer by one results in an element of a half- open range of nonnegative integers with the upper bound increased by one. (Contributed by Alexander van der Vekens, 5-Aug-2018)

Ref Expression
Assertion fzonn0p1p1 ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )

Proof

Step Hyp Ref Expression
1 elfzo0 ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) )
2 peano2nn0 ⊢ ( 𝐼 ∈ ℕ0 → ( 𝐼 + 1 ) ∈ ℕ0 )
3 2 3ad2ant1 ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) → ( 𝐼 + 1 ) ∈ ℕ0 )
4 peano2nn ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
5 4 3ad2ant2 ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) → ( 𝑁 + 1 ) ∈ ℕ )
6 simp3 ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) → 𝐼 < 𝑁 )
7 nn0re ⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℝ )
8 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
9 1red ⊢ ( 𝐼 < 𝑁 → 1 ∈ ℝ )
10 ltadd1 ⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐼 < 𝑁 ↔ ( 𝐼 + 1 ) < ( 𝑁 + 1 ) ) )
11 7 8 9 10 syl3an ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) → ( 𝐼 < 𝑁 ↔ ( 𝐼 + 1 ) < ( 𝑁 + 1 ) ) )
12 6 11 mpbid ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) → ( 𝐼 + 1 ) < ( 𝑁 + 1 ) )
13 elfzo0 ⊢ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ↔ ( ( 𝐼 + 1 ) ∈ ℕ0 ∧ ( 𝑁 + 1 ) ∈ ℕ ∧ ( 𝐼 + 1 ) < ( 𝑁 + 1 ) ) )
14 3 5 12 13 syl3anbrc ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) → ( 𝐼 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
15 1 14 sylbi ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )