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

Proof

Step	Hyp	Ref	Expression
1		elfzo0	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) )
2	1	simp2bi	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝑁 ∈ ℕ )
3		fzo0sn0fzo1	⊢ ( 𝑁 ∈ ℕ → ( 0 ..^ 𝑁 ) = ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) )
4	3	eleq2d	⊢ ( 𝑁 ∈ ℕ → ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ↔ 𝐾 ∈ ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) ) )
5		elun	⊢ ( 𝐾 ∈ ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) ↔ ( 𝐾 ∈ { 0 } ∨ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) )
6		elsni	⊢ ( 𝐾 ∈ { 0 } → 𝐾 = 0 )
7	6	orim1i	⊢ ( ( 𝐾 ∈ { 0 } ∨ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) → ( 𝐾 = 0 ∨ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) )
8	5 7	sylbi	⊢ ( 𝐾 ∈ ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) → ( 𝐾 = 0 ∨ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) )
9	4 8	biimtrdi	⊢ ( 𝑁 ∈ ℕ → ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐾 = 0 ∨ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) ) )
10	2 9	mpcom	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐾 = 0 ∨ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) )