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 
|- ( 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 } )