Metamath Proof Explorer

Theorem fzsubel

Description: Membership of a difference in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005)

Ref Expression
Assertion fzsubel 
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( J e. ( M ... N ) <-> ( J - K ) e. ( ( M - K ) ... ( N - K ) ) ) )

Proof

Step Hyp Ref Expression
1 znegcl 
 |-  ( K e. ZZ -> -u K e. ZZ )
2 fzaddel 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ -u K e. ZZ ) ) -> ( J e. ( M ... N ) <-> ( J + -u K ) e. ( ( M + -u K ) ... ( N + -u K ) ) ) )
3 1 2 sylanr2 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( J e. ( M ... N ) <-> ( J + -u K ) e. ( ( M + -u K ) ... ( N + -u K ) ) ) )
4 zcn 
 |-  ( M e. ZZ -> M e. CC )
5 zcn 
 |-  ( N e. ZZ -> N e. CC )
6 4 5 anim12i 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M e. CC /\ N e. CC ) )
7 zcn 
 |-  ( J e. ZZ -> J e. CC )
8 zcn 
 |-  ( K e. ZZ -> K e. CC )
9 7 8 anim12i 
 |-  ( ( J e. ZZ /\ K e. ZZ ) -> ( J e. CC /\ K e. CC ) )
10 negsub 
 |-  ( ( J e. CC /\ K e. CC ) -> ( J + -u K ) = ( J - K ) )
11 10 adantl 
 |-  ( ( ( M e. CC /\ N e. CC ) /\ ( J e. CC /\ K e. CC ) ) -> ( J + -u K ) = ( J - K ) )
12 negsub 
 |-  ( ( M e. CC /\ K e. CC ) -> ( M + -u K ) = ( M - K ) )
13 negsub 
 |-  ( ( N e. CC /\ K e. CC ) -> ( N + -u K ) = ( N - K ) )
14 12 13 oveqan12d 
 |-  ( ( ( M e. CC /\ K e. CC ) /\ ( N e. CC /\ K e. CC ) ) -> ( ( M + -u K ) ... ( N + -u K ) ) = ( ( M - K ) ... ( N - K ) ) )
15 14 anandirs 
 |-  ( ( ( M e. CC /\ N e. CC ) /\ K e. CC ) -> ( ( M + -u K ) ... ( N + -u K ) ) = ( ( M - K ) ... ( N - K ) ) )
16 15 adantrl 
 |-  ( ( ( M e. CC /\ N e. CC ) /\ ( J e. CC /\ K e. CC ) ) -> ( ( M + -u K ) ... ( N + -u K ) ) = ( ( M - K ) ... ( N - K ) ) )
17 11 16 eleq12d 
 |-  ( ( ( M e. CC /\ N e. CC ) /\ ( J e. CC /\ K e. CC ) ) -> ( ( J + -u K ) e. ( ( M + -u K ) ... ( N + -u K ) ) <-> ( J - K ) e. ( ( M - K ) ... ( N - K ) ) ) )
18 6 9 17 syl2an 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( ( J + -u K ) e. ( ( M + -u K ) ... ( N + -u K ) ) <-> ( J - K ) e. ( ( M - K ) ... ( N - K ) ) ) )
19 3 18 bitrd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( J e. ( M ... N ) <-> ( J - K ) e. ( ( M - K ) ... ( N - K ) ) ) )