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