This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )