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