Metamath Proof Explorer

Theorem elgz

Description: Elementhood in the gaussian integers. (Contributed by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion elgz 
|- ( A e. Z[i] <-> ( A e. CC /\ ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( x = A -> ( Re ` x ) = ( Re ` A ) )
2 1 eleq1d 
 |-  ( x = A -> ( ( Re ` x ) e. ZZ <-> ( Re ` A ) e. ZZ ) )
3 fveq2 
 |-  ( x = A -> ( Im ` x ) = ( Im ` A ) )
4 3 eleq1d 
 |-  ( x = A -> ( ( Im ` x ) e. ZZ <-> ( Im ` A ) e. ZZ ) )
5 2 4 anbi12d 
 |-  ( x = A -> ( ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) <-> ( ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) ) )
6 df-gz 
 |-  Z[i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
7 5 6 elrab2 
 |-  ( A e. Z[i] <-> ( A e. CC /\ ( ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) ) )
8 3anass 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) <-> ( A e. CC /\ ( ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) ) )
9 7 8 bitr4i 
 |-  ( A e. Z[i] <-> ( A e. CC /\ ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) )