Metamath Proof Explorer

Theorem gzcjcl

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

Ref Expression
Assertion gzcjcl 
|- ( A e. Z[i] -> ( * ` A ) e. Z[i] )

Proof

Step Hyp Ref Expression
1 gzcn 
 |-  ( A e. Z[i] -> A e. CC )
2 1 cjcld 
 |-  ( A e. Z[i] -> ( * ` A ) e. CC )
3 1 recjd 
 |-  ( A e. Z[i] -> ( Re ` ( * ` A ) ) = ( 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 3 5 eqeltrd 
 |-  ( A e. Z[i] -> ( Re ` ( * ` A ) ) e. ZZ )
7 1 imcjd 
 |-  ( A e. Z[i] -> ( Im ` ( * ` A ) ) = -u ( Im ` A ) )
8 4 simp3bi 
 |-  ( A e. Z[i] -> ( Im ` A ) e. ZZ )
9 8 znegcld 
 |-  ( A e. Z[i] -> -u ( Im ` A ) e. ZZ )
10 7 9 eqeltrd 
 |-  ( A e. Z[i] -> ( Im ` ( * ` A ) ) e. ZZ )
11 elgz 
 |-  ( ( * ` A ) e. Z[i] <-> ( ( * ` A ) e. CC /\ ( Re ` ( * ` A ) ) e. ZZ /\ ( Im ` ( * ` A ) ) e. ZZ ) )
12 2 6 10 11 syl3anbrc 
 |-  ( A e. Z[i] -> ( * ` A ) e. Z[i] )