Description: The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | fzrev3i | ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzelz | ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ℤ ) | |
2 | fzrev3 | ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) ) | |
3 | 1 2 | syl | ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) ) |
4 | 3 | ibi | ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) |