Theorem elfzo0l

Description: A member of a half-open range of nonnegative integers is either 0 or a member of the corresponding half-open range of positive integers. (Contributed by AV, 5-Feb-2021)

	Ref	Expression
Assertion	elfzo0l	|- ( K e. ( 0 ..^ N ) -> ( K = 0 \/ K e. ( 1 ..^ N ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfzo0	|- ( K e. ( 0 ..^ N ) <-> ( K e. NN0 /\ N e. NN /\ K < N ) )
2	1	simp2bi	|- ( K e. ( 0 ..^ N ) -> N e. NN )
3		fzo0sn0fzo1	|- ( N e. NN -> ( 0 ..^ N ) = ( { 0 } u. ( 1 ..^ N ) ) )
4	3	eleq2d	|- ( N e. NN -> ( K e. ( 0 ..^ N ) <-> K e. ( { 0 } u. ( 1 ..^ N ) ) ) )
5		elun	|- ( K e. ( { 0 } u. ( 1 ..^ N ) ) <-> ( K e. { 0 } \/ K e. ( 1 ..^ N ) ) )
6		elsni	|- ( K e. { 0 } -> K = 0 )
7	6	orim1i	|- ( ( K e. { 0 } \/ K e. ( 1 ..^ N ) ) -> ( K = 0 \/ K e. ( 1 ..^ N ) ) )
8	5 7	sylbi	|- ( K e. ( { 0 } u. ( 1 ..^ N ) ) -> ( K = 0 \/ K e. ( 1 ..^ N ) ) )
9	4 8	biimtrdi	|- ( N e. NN -> ( K e. ( 0 ..^ N ) -> ( K = 0 \/ K e. ( 1 ..^ N ) ) ) )
10	2 9	mpcom	|- ( K e. ( 0 ..^ N ) -> ( K = 0 \/ K e. ( 1 ..^ N ) ) )