Metamath Proof Explorer

Theorem fzonn0p1p1

Description: If a nonnegative integer is 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 ⊢ I ∈ 0 ..^ N → I + 1 ∈ 0 ..^ N + 1

Proof

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