Metamath Proof Explorer


Theorem fzrev3i

Description: The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005)

Ref Expression
Assertion fzrev3i
|- ( K e. ( M ... N ) -> ( ( M + N ) - K ) e. ( M ... N ) )

Proof

Step Hyp Ref Expression
1 elfzelz
 |-  ( K e. ( M ... N ) -> K e. ZZ )
2 fzrev3
 |-  ( K e. ZZ -> ( K e. ( M ... N ) <-> ( ( M + N ) - K ) e. ( M ... N ) ) )
3 1 2 syl
 |-  ( K e. ( M ... N ) -> ( K e. ( M ... N ) <-> ( ( M + N ) - K ) e. ( M ... N ) ) )
4 3 ibi
 |-  ( K e. ( M ... N ) -> ( ( M + N ) - K ) e. ( M ... N ) )