Metamath Proof Explorer

Theorem zgz

Description: An integer is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion zgz 
|- ( A e. ZZ -> A e. Z[i] )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( A e. ZZ -> A e. CC )
2 zre 
 |-  ( A e. ZZ -> A e. RR )
3 2 rered 
 |-  ( A e. ZZ -> ( Re ` A ) = A )
4 id 
 |-  ( A e. ZZ -> A e. ZZ )
5 3 4 eqeltrd 
 |-  ( A e. ZZ -> ( Re ` A ) e. ZZ )
6 2 reim0d 
 |-  ( A e. ZZ -> ( Im ` A ) = 0 )
7 0z 
 |-  0 e. ZZ
8 6 7 eqeltrdi 
 |-  ( A e. ZZ -> ( Im ` A ) e. ZZ )
9 elgz 
 |-  ( A e. Z[i] <-> ( A e. CC /\ ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) )
10 1 5 8 9 syl3anbrc 
 |-  ( A e. ZZ -> A e. Z[i] )