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 ⊢ A ⊆ ℤ → z ∈ ℝ | − z ∈ A = z ∈ ℤ | − z ∈ A

Proof

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