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	⊢ ( 𝐼 ∈ ( 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 ) ) )