This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqreznegel

Description: Two ways to express the image under negation of a set of integers. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion eqreznegel ( 𝐴 ⊆ ℤ → { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } = { 𝑧 ∈ ℤ ∣ - 𝑧 ∈ 𝐴 } )

Proof

Step Hyp Ref Expression
1 ssel ⊢ ( 𝐴 ⊆ ℤ → ( - 𝑤 ∈ 𝐴 → - 𝑤 ∈ ℤ ) )
2 recn ⊢ ( 𝑤 ∈ ℝ → 𝑤 ∈ ℂ )
3 negid ⊢ ( 𝑤 ∈ ℂ → ( 𝑤 + - 𝑤 ) = 0 )
4 0z ⊢ 0 ∈ ℤ
5 3 4 eqeltrdi ⊢ ( 𝑤 ∈ ℂ → ( 𝑤 + - 𝑤 ) ∈ ℤ )
6 5 pm4.71i ⊢ ( 𝑤 ∈ ℂ ↔ ( 𝑤 ∈ ℂ ∧ ( 𝑤 + - 𝑤 ) ∈ ℤ ) )
7 zrevaddcl ⊢ ( - 𝑤 ∈ ℤ → ( ( 𝑤 ∈ ℂ ∧ ( 𝑤 + - 𝑤 ) ∈ ℤ ) ↔ 𝑤 ∈ ℤ ) )
8 6 7 bitrid ⊢ ( - 𝑤 ∈ ℤ → ( 𝑤 ∈ ℂ ↔ 𝑤 ∈ ℤ ) )
9 2 8 imbitrid ⊢ ( - 𝑤 ∈ ℤ → ( 𝑤 ∈ ℝ → 𝑤 ∈ ℤ ) )
10 1 9 syl6 ⊢ ( 𝐴 ⊆ ℤ → ( - 𝑤 ∈ 𝐴 → ( 𝑤 ∈ ℝ → 𝑤 ∈ ℤ ) ) )
11 10 impcomd ⊢ ( 𝐴 ⊆ ℤ → ( ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ 𝐴 ) → 𝑤 ∈ ℤ ) )
12 simpr ⊢ ( ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ 𝐴 ) → - 𝑤 ∈ 𝐴 )
13 11 12 jca2 ⊢ ( 𝐴 ⊆ ℤ → ( ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ 𝐴 ) → ( 𝑤 ∈ ℤ ∧ - 𝑤 ∈ 𝐴 ) ) )
14 zre ⊢ ( 𝑤 ∈ ℤ → 𝑤 ∈ ℝ )
15 14 anim1i ⊢ ( ( 𝑤 ∈ ℤ ∧ - 𝑤 ∈ 𝐴 ) → ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ 𝐴 ) )
16 13 15 impbid1 ⊢ ( 𝐴 ⊆ ℤ → ( ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ 𝐴 ) ↔ ( 𝑤 ∈ ℤ ∧ - 𝑤 ∈ 𝐴 ) ) )
17 negeq ⊢ ( 𝑧 = 𝑤 → - 𝑧 = - 𝑤 )
18 17 eleq1d ⊢ ( 𝑧 = 𝑤 → ( - 𝑧 ∈ 𝐴 ↔ - 𝑤 ∈ 𝐴 ) )
19 18 elrab ⊢ ( 𝑤 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ↔ ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ 𝐴 ) )
20 18 elrab ⊢ ( 𝑤 ∈ { 𝑧 ∈ ℤ ∣ - 𝑧 ∈ 𝐴 } ↔ ( 𝑤 ∈ ℤ ∧ - 𝑤 ∈ 𝐴 ) )
21 16 19 20 3bitr4g ⊢ ( 𝐴 ⊆ ℤ → ( 𝑤 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ↔ 𝑤 ∈ { 𝑧 ∈ ℤ ∣ - 𝑧 ∈ 𝐴 } ) )
22 21 eqrdv ⊢ ( 𝐴 ⊆ ℤ → { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } = { 𝑧 ∈ ℤ ∣ - 𝑧 ∈ 𝐴 } )