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 \in (M \dots N) \to M + N - K \in (M \dots N)$

Step	Hyp	Ref	Expression
1		elfzelz	$⊢ K \in (M \dots N) \to K \in ℤ$
2		fzrev3	$⊢ K \in ℤ \to (K \in (M \dots N) \leftrightarrow M + N - K \in (M \dots N))$
3	1 2	syl	$⊢ K \in (M \dots N) \to (K \in (M \dots N) \leftrightarrow M + N - K \in (M \dots N))$
4	3	ibi	$⊢ K \in (M \dots N) \to M + N - K \in (M \dots N)$