Theorem elfzonn0

Description: A member of a half-open range of nonnegative integers is a nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018)

	Ref	Expression
Assertion	elfzonn0	|- ( K e. ( 0 ..^ N ) -> K e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		elfzouz	|- ( K e. ( 0 ..^ N ) -> K e. ( ZZ>= ` 0 ) )
2		elnn0uz	|- ( K e. NN0 <-> K e. ( ZZ>= ` 0 ) )
3	1 2	sylibr	|- ( K e. ( 0 ..^ N ) -> K e. NN0 )