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

Theorem gzcn 13993
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 13992 . 2  |-  ( A  e.  ZZ[_i]  <->  ( A  e.  CC  /\  ( Re
`  A )  e.  ZZ  /\  ( Im
`  A )  e.  ZZ ) )
21simp1bi 1003 1  |-  ( A  e.  ZZ[_i]  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   ` cfv 5418   CCcc 9280   ZZcz 10646   Recre 12586   Imcim 12587   ZZ[_i]cgz 13990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-iota 5381  df-fv 5426  df-gz 13991
This theorem is referenced by:  gznegcl  13996  gzcjcl  13997  gzaddcl  13998  gzmulcl  13999  gzsubcl  14001  gzabssqcl  14002  4sqlem4a  14012  4sqlem4  14013  mul4sqlem  14014  mul4sq  14015  4sqlem12  14017  4sqlem17  14022  gzsubrg  17867  gzrngunitlem  17877  gzrngunit  17878  2sqlem2  22703  mul2sq  22704  2sqlem3  22705  cntotbnd  28695
  Copyright terms: Public domain W3C validator