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	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzelz	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ℤ )
2		fzrev3	⊢ ( 𝐾 ∈ ℤ → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) )
3	1 2	syl	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) )
4	3	ibi	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) )