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	⊢ ( 𝐴 ⊆ ℤ → { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } = { 𝑧 ∈ ℤ ∣ - 𝑧 ∈ 𝐴 } )