Metamath Proof Explorer


Theorem fzrev3

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

Ref Expression
Assertion fzrev3 ( 𝐾 ∈ ℤ → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝐾 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ℤ )
2 elfzel1 ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ∈ ℤ )
3 2 adantl ( ( 𝐾 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ∈ ℤ )
4 elfzel2 ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ℤ )
5 4 adantl ( ( 𝐾 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ℤ )
6 1 3 5 3jca ( ( 𝐾 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
7 simpl ( ( 𝐾 ∈ ℤ ∧ ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ℤ )
8 elfzel1 ( ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ∈ ℤ )
9 8 adantl ( ( 𝐾 ∈ ℤ ∧ ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ∈ ℤ )
10 elfzel2 ( ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ℤ )
11 10 adantl ( ( 𝐾 ∈ ℤ ∧ ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ℤ )
12 7 9 11 3jca ( ( 𝐾 ∈ ℤ ∧ ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
13 zcn ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
14 zcn ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
15 pncan ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
16 pncan2 ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑀 + 𝑁 ) − 𝑀 ) = 𝑁 )
17 15 16 oveq12d ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( ( 𝑀 + 𝑁 ) − 𝑁 ) ... ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) = ( 𝑀 ... 𝑁 ) )
18 13 14 17 syl2an ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑀 + 𝑁 ) − 𝑁 ) ... ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) = ( 𝑀 ... 𝑁 ) )
19 18 eleq2d ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( ( ( 𝑀 + 𝑁 ) − 𝑁 ) ... ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ↔ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) )
20 19 3adant1 ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( ( ( 𝑀 + 𝑁 ) − 𝑁 ) ... ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ↔ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) )
21 3simpc ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
22 zaddcl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
23 22 3adant1 ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
24 simp1 ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ℤ )
25 fzrev ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 ∈ ( ( ( 𝑀 + 𝑁 ) − 𝑁 ) ... ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ↔ ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) )
26 21 23 24 25 syl12anc ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( ( ( 𝑀 + 𝑁 ) − 𝑁 ) ... ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) ↔ ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) )
27 20 26 bitr3d ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) )
28 6 12 27 pm5.21nd ( 𝐾 ∈ ℤ → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑀 + 𝑁 ) − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) )