Metamath Proof Explorer


Theorem elfzp12

Description: Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010)

Ref Expression
Assertion elfzp12
|- ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... N ) <-> ( K = M \/ K e. ( ( M + 1 ) ... N ) ) ) )

Proof

Step Hyp Ref Expression
1 elex
 |-  ( K e. ( M ... N ) -> K e. _V )
2 1 anim2i
 |-  ( ( N e. ( ZZ>= ` M ) /\ K e. ( M ... N ) ) -> ( N e. ( ZZ>= ` M ) /\ K e. _V ) )
3 elfvex
 |-  ( N e. ( ZZ>= ` M ) -> M e. _V )
4 eleq1
 |-  ( K = M -> ( K e. _V <-> M e. _V ) )
5 3 4 syl5ibrcom
 |-  ( N e. ( ZZ>= ` M ) -> ( K = M -> K e. _V ) )
6 5 imdistani
 |-  ( ( N e. ( ZZ>= ` M ) /\ K = M ) -> ( N e. ( ZZ>= ` M ) /\ K e. _V ) )
7 elex
 |-  ( K e. ( ( M + 1 ) ... N ) -> K e. _V )
8 7 anim2i
 |-  ( ( N e. ( ZZ>= ` M ) /\ K e. ( ( M + 1 ) ... N ) ) -> ( N e. ( ZZ>= ` M ) /\ K e. _V ) )
9 6 8 jaodan
 |-  ( ( N e. ( ZZ>= ` M ) /\ ( K = M \/ K e. ( ( M + 1 ) ... N ) ) ) -> ( N e. ( ZZ>= ` M ) /\ K e. _V ) )
10 fzpred
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( { M } u. ( ( M + 1 ) ... N ) ) )
11 10 eleq2d
 |-  ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... N ) <-> K e. ( { M } u. ( ( M + 1 ) ... N ) ) ) )
12 elun
 |-  ( K e. ( { M } u. ( ( M + 1 ) ... N ) ) <-> ( K e. { M } \/ K e. ( ( M + 1 ) ... N ) ) )
13 11 12 bitrdi
 |-  ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... N ) <-> ( K e. { M } \/ K e. ( ( M + 1 ) ... N ) ) ) )
14 elsng
 |-  ( K e. _V -> ( K e. { M } <-> K = M ) )
15 14 orbi1d
 |-  ( K e. _V -> ( ( K e. { M } \/ K e. ( ( M + 1 ) ... N ) ) <-> ( K = M \/ K e. ( ( M + 1 ) ... N ) ) ) )
16 13 15 sylan9bb
 |-  ( ( N e. ( ZZ>= ` M ) /\ K e. _V ) -> ( K e. ( M ... N ) <-> ( K = M \/ K e. ( ( M + 1 ) ... N ) ) ) )
17 2 9 16 pm5.21nd
 |-  ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... N ) <-> ( K = M \/ K e. ( ( M + 1 ) ... N ) ) ) )