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 C_ ZZ -> { z e. RR | -u z e. A } = { z e. ZZ | -u z e. A } )

Proof

Step	Hyp	Ref	Expression
1		ssel	|- ( A C_ ZZ -> ( -u w e. A -> -u w e. ZZ ) )
2		recn	|- ( w e. RR -> w e. CC )
3		negid	|- ( w e. CC -> ( w + -u w ) = 0 )
4		0z	|- 0 e. ZZ
5	3 4	eqeltrdi	|- ( w e. CC -> ( w + -u w ) e. ZZ )
6	5	pm4.71i	|- ( w e. CC <-> ( w e. CC /\ ( w + -u w ) e. ZZ ) )
7		zrevaddcl	|- ( -u w e. ZZ -> ( ( w e. CC /\ ( w + -u w ) e. ZZ ) <-> w e. ZZ ) )
8	6 7	bitrid	|- ( -u w e. ZZ -> ( w e. CC <-> w e. ZZ ) )
9	2 8	imbitrid	|- ( -u w e. ZZ -> ( w e. RR -> w e. ZZ ) )
10	1 9	syl6	|- ( A C_ ZZ -> ( -u w e. A -> ( w e. RR -> w e. ZZ ) ) )
11	10	impcomd	|- ( A C_ ZZ -> ( ( w e. RR /\ -u w e. A ) -> w e. ZZ ) )
12		simpr	|- ( ( w e. RR /\ -u w e. A ) -> -u w e. A )
13	11 12	jca2	|- ( A C_ ZZ -> ( ( w e. RR /\ -u w e. A ) -> ( w e. ZZ /\ -u w e. A ) ) )
14		zre	|- ( w e. ZZ -> w e. RR )
15	14	anim1i	|- ( ( w e. ZZ /\ -u w e. A ) -> ( w e. RR /\ -u w e. A ) )
16	13 15	impbid1	|- ( A C_ ZZ -> ( ( w e. RR /\ -u w e. A ) <-> ( w e. ZZ /\ -u w e. A ) ) )
17		negeq	|- ( z = w -> -u z = -u w )
18	17	eleq1d	|- ( z = w -> ( -u z e. A <-> -u w e. A ) )
19	18	elrab	|- ( w e. { z e. RR | -u z e. A } <-> ( w e. RR /\ -u w e. A ) )
20	18	elrab	|- ( w e. { z e. ZZ | -u z e. A } <-> ( w e. ZZ /\ -u w e. A ) )
21	16 19 20	3bitr4g	|- ( A C_ ZZ -> ( w e. { z e. RR | -u z e. A } <-> w e. { z e. ZZ | -u z e. A } ) )
22	21	eqrdv	|- ( A C_ ZZ -> { z e. RR | -u z e. A } = { z e. ZZ | -u z e. A } )