Theorem elfz0lmr

Description: A member of a finite interval of nonnegative integers is either 0 or its upper bound or an element of its interior. (Contributed by AV, 5-Feb-2021)

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

Proof

Step	Hyp	Ref	Expression
1		elfzlmr	|- ( K e. ( 0 ... N ) -> ( K = 0 \/ K e. ( ( 0 + 1 ) ..^ N ) \/ K = N ) )
2		biid	|- ( K = 0 <-> K = 0 )
3		0p1e1	|- ( 0 + 1 ) = 1
4	3	oveq1i	|- ( ( 0 + 1 ) ..^ N ) = ( 1 ..^ N )
5	4	eleq2i	|- ( K e. ( ( 0 + 1 ) ..^ N ) <-> K e. ( 1 ..^ N ) )
6		biid	|- ( K = N <-> K = N )
7	2 5 6	3orbi123i	|- ( ( K = 0 \/ K e. ( ( 0 + 1 ) ..^ N ) \/ K = N ) <-> ( K = 0 \/ K e. ( 1 ..^ N ) \/ K = N ) )
8	1 7	sylib	|- ( K e. ( 0 ... N ) -> ( K = 0 \/ K e. ( 1 ..^ N ) \/ K = N ) )