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	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝐾 = 0 ∨ 𝐾 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzlmr	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝐾 = 0 ∨ 𝐾 ∈ ( ( 0 + 1 ) ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) )
2		biid	⊢ ( 𝐾 = 0 ↔ 𝐾 = 0 )
3		0p1e1	⊢ ( 0 + 1 ) = 1
4	3	oveq1i	⊢ ( ( 0 + 1 ) ..^ 𝑁 ) = ( 1 ..^ 𝑁 )
5	4	eleq2i	⊢ ( 𝐾 ∈ ( ( 0 + 1 ) ..^ 𝑁 ) ↔ 𝐾 ∈ ( 1 ..^ 𝑁 ) )
6		biid	⊢ ( 𝐾 = 𝑁 ↔ 𝐾 = 𝑁 )
7	2 5 6	3orbi123i	⊢ ( ( 𝐾 = 0 ∨ 𝐾 ∈ ( ( 0 + 1 ) ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) ↔ ( 𝐾 = 0 ∨ 𝐾 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) )
8	1 7	sylib	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝐾 = 0 ∨ 𝐾 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) )