Metamath Proof Explorer

Theorem gznegcl

Description: The gaussian integers are closed under negation. (Contributed by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion gznegcl 
|- ( A e. Z[i] -> -u A e. Z[i] )

Proof

Step Hyp Ref Expression
1 gzcn 
 |-  ( A e. Z[i] -> A e. CC )
2 1 negcld 
 |-  ( A e. Z[i] -> -u A e. CC )
3 1 renegd 
 |-  ( A e. Z[i] -> ( Re ` -u A ) = -u ( Re ` A ) )
4 elgz 
 |-  ( A e. Z[i] <-> ( A e. CC /\ ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) )
5 4 simp2bi 
 |-  ( A e. Z[i] -> ( Re ` A ) e. ZZ )
6 5 znegcld 
 |-  ( A e. Z[i] -> -u ( Re ` A ) e. ZZ )
7 3 6 eqeltrd 
 |-  ( A e. Z[i] -> ( Re ` -u A ) e. ZZ )
8 1 imnegd 
 |-  ( A e. Z[i] -> ( Im ` -u A ) = -u ( Im ` A ) )
9 4 simp3bi 
 |-  ( A e. Z[i] -> ( Im ` A ) e. ZZ )
10 9 znegcld 
 |-  ( A e. Z[i] -> -u ( Im ` A ) e. ZZ )
11 8 10 eqeltrd 
 |-  ( A e. Z[i] -> ( Im ` -u A ) e. ZZ )
12 elgz 
 |-  ( -u A e. Z[i] <-> ( -u A e. CC /\ ( Re ` -u A ) e. ZZ /\ ( Im ` -u A ) e. ZZ ) )
13 2 7 11 12 syl3anbrc 
 |-  ( A e. Z[i] -> -u A e. Z[i] )