MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gzcn Unicode version

Theorem gzcn 13229
Description: A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.)
Assertion
Ref Expression
gzcn  |-  ( A  e.  ZZ [ _i ]  ->  A  e.  CC )

Proof of Theorem gzcn
StepHypRef Expression
1 elgz 13228 . 2  |-  ( A  e.  ZZ [ _i ] 
<->  ( A  e.  CC  /\  ( Re `  A
)  e.  ZZ  /\  ( Im `  A )  e.  ZZ ) )
21simp1bi 972 1  |-  ( A  e.  ZZ [ _i ]  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   ` cfv 5396   CCcc 8923   ZZcz 10216   Recre 11831   Imcim 11832   ZZ [ _i ]cgz 13226
This theorem is referenced by:  gznegcl  13232  gzcjcl  13233  gzaddcl  13234  gzmulcl  13235  gzsubcl  13237  gzabssqcl  13238  4sqlem4a  13248  4sqlem4  13249  mul4sqlem  13250  mul4sq  13251  4sqlem12  13253  4sqlem17  13258  gzsubrg  16678  gzrngunitlem  16688  gzrngunit  16689  2sqlem2  21017  mul2sq  21018  2sqlem3  21019  cntotbnd  26198
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-rex 2657  df-rab 2660  df-v 2903  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-br 4156  df-iota 5360  df-fv 5404  df-gz 13227
  Copyright terms: Public domain W3C validator