Theorem nn0fz0

Description: A nonnegative integer is always part of the finite set of sequential nonnegative integers with this integer as upper bound. (Contributed by Scott Fenton, 21-Mar-2018)

	Ref	Expression
Assertion	nn0fz0	|- ( N e. NN0 <-> N e. ( 0 ... N ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( N e. NN0 -> N e. NN0 )
2		nn0re	|- ( N e. NN0 -> N e. RR )
3	2	leidd	|- ( N e. NN0 -> N <_ N )
4		fznn0	|- ( N e. NN0 -> ( N e. ( 0 ... N ) <-> ( N e. NN0 /\ N <_ N ) ) )
5	1 3 4	mpbir2and	|- ( N e. NN0 -> N e. ( 0 ... N ) )
6		elfz3nn0	|- ( N e. ( 0 ... N ) -> N e. NN0 )
7	5 6	impbii	|- ( N e. NN0 <-> N e. ( 0 ... N ) )