Theorem fzonn0p1

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

	Ref	Expression
Assertion	fzonn0p1	|- ( N e. NN0 -> N e. ( 0 ..^ ( N + 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( N e. NN0 -> N e. NN0 )
2		nn0p1nn	|- ( N e. NN0 -> ( N + 1 ) e. NN )
3		nn0re	|- ( N e. NN0 -> N e. RR )
4	3	ltp1d	|- ( N e. NN0 -> N < ( N + 1 ) )
5		elfzo0	|- ( N e. ( 0 ..^ ( N + 1 ) ) <-> ( N e. NN0 /\ ( N + 1 ) e. NN /\ N < ( N + 1 ) ) )
6	1 2 4 5	syl3anbrc	|- ( N e. NN0 -> N e. ( 0 ..^ ( N + 1 ) ) )