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