Metamath Proof Explorer

Theorem fzrev2

Description: Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( J e. ZZ /\ K e. ZZ ) -> J e. ZZ )
2 zsubcl 
 |-  ( ( J e. ZZ /\ K e. ZZ ) -> ( J - K ) e. ZZ )
3 1 2 jca 
 |-  ( ( J e. ZZ /\ K e. ZZ ) -> ( J e. ZZ /\ ( J - K ) e. ZZ ) )
4 fzrev 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ ( J - K ) e. ZZ ) ) -> ( ( J - K ) e. ( ( J - N ) ... ( J - M ) ) <-> ( J - ( J - K ) ) e. ( M ... N ) ) )
5 3 4 sylan2 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( ( J - K ) e. ( ( J - N ) ... ( J - M ) ) <-> ( J - ( J - K ) ) e. ( M ... N ) ) )
6 zcn 
 |-  ( J e. ZZ -> J e. CC )
7 zcn 
 |-  ( K e. ZZ -> K e. CC )
8 nncan 
 |-  ( ( J e. CC /\ K e. CC ) -> ( J - ( J - K ) ) = K )
9 6 7 8 syl2an 
 |-  ( ( J e. ZZ /\ K e. ZZ ) -> ( J - ( J - K ) ) = K )
10 9 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( J - ( J - K ) ) = K )
11 10 eleq1d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( ( J - ( J - K ) ) e. ( M ... N ) <-> K e. ( M ... N ) ) )
12 5 11 bitr2d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( K e. ( M ... N ) <-> ( J - K ) e. ( ( J - N ) ... ( J - M ) ) ) )