Metamath Proof Explorer

Theorem gzcn

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

Ref Expression
Assertion gzcn 
|- ( A e. Z[i] -> A e. CC )

Proof

Step Hyp Ref Expression
1 elgz 
 |-  ( A e. Z[i] <-> ( A e. CC /\ ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) )
2 1 simp1bi 
 |-  ( A e. Z[i] -> A e. CC )