Theorem fzossfzop1

Description: A half-open range of nonnegative integers is a subset 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	fzossfzop1	|- ( N e. NN0 -> ( 0 ..^ N ) C_ ( 0 ..^ ( N + 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nn0z	|- ( N e. NN0 -> N e. ZZ )
2		id	|- ( N e. ZZ -> N e. ZZ )
3		peano2z	|- ( N e. ZZ -> ( N + 1 ) e. ZZ )
4		zre	|- ( N e. ZZ -> N e. RR )
5	4	lep1d	|- ( N e. ZZ -> N <_ ( N + 1 ) )
6	2 3 5	3jca	|- ( N e. ZZ -> ( N e. ZZ /\ ( N + 1 ) e. ZZ /\ N <_ ( N + 1 ) ) )
7	1 6	syl	|- ( N e. NN0 -> ( N e. ZZ /\ ( N + 1 ) e. ZZ /\ N <_ ( N + 1 ) ) )
8		eluz2	|- ( ( N + 1 ) e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ ( N + 1 ) e. ZZ /\ N <_ ( N + 1 ) ) )
9	7 8	sylibr	|- ( N e. NN0 -> ( N + 1 ) e. ( ZZ>= ` N ) )
10		fzoss2	|- ( ( N + 1 ) e. ( ZZ>= ` N ) -> ( 0 ..^ N ) C_ ( 0 ..^ ( N + 1 ) ) )
11	9 10	syl	|- ( N e. NN0 -> ( 0 ..^ N ) C_ ( 0 ..^ ( N + 1 ) ) )