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