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

Theorem zcn 10894
Description: An integer is a complex number. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
zcn

Proof of Theorem zcn
StepHypRef Expression
1 zre 10893 . 2
21recnd 9643 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cc 9511   cz 10889
This theorem is referenced by:  zsscn  10897  zsubcl  10931  zrevaddcl  10934  zlem1lt  10940  zltlem1  10941  zdiv  10958  zdivadd  10959  zdivmul  10960  zextlt  10962  zneo  10970  zeo2  10974  peano5uzi  10976  uzindOLD  10982  zindd  10990  zriotaneg  11002  zmax  11208  rebtwnz  11210  qmulz  11214  zq  11217  qaddcl  11227  qnegcl  11228  qmulcl  11229  qreccl  11231  fzen  11732  uzsubsubfz  11736  fz01en  11742  fzmmmeqm  11746  fzsubel  11748  fztp  11765  fzsuc2  11766  fzrev2  11772  fzrev3  11774  elfzp1b  11784  fzrevral  11792  fzrevral2  11793  fzrevral3  11794  fzshftral  11795  fzoaddel2  11874  fzosubel2  11876  eluzgtdifelfzo  11878  fzocatel  11880  elfzom1elp1fzo  11883  fzval3  11885  zpnn0elfzo1  11889  fzosplitprm1  11919  fzoshftral  11923  flzadd  11959  ceilid  11978  quoremz  11982  intfracq  11986  zmod10  12012  modcyc  12031  modcyc2  12032  modmul1  12040  modaddmulmod  12053  uzrdgxfr  12077  fzen2  12079  seqshft2  12133  sermono  12139  expsub  12213  zesq  12289  modexp  12301  bccmpl  12387  swrd00  12645  addlenrevswrd  12661  swrdswrd  12685  swrdswrd0  12687  swrdccatin12lem1  12709  swrdccatin12lem2b  12711  swrdccatin2  12712  swrdccatin12lem2  12714  swrdccatin12  12716  repswrevw  12758  cshwsublen  12767  cshwidx0mod  12775  2cshw  12781  2cshwid  12782  2cshwcom  12784  cshweqdif2  12787  cshweqrep  12789  cshw1  12790  2cshwcshw  12793  shftuz  12902  seqshft  12918  nn0abscl  13145  nnabscl  13158  climshftlem  13397  climshft  13399  isershft  13486  mptfzshft  13593  fsumrev  13594  fsum0diag2  13598  efexp  13836  efzval  13837  demoivre  13935  znnenlem  13945  sqrt2irr  13982  dvdsval2  13989  iddvds  13997  1dvds  13998  dvds0  13999  negdvdsb  14000  dvdsnegb  14001  0dvds  14004  dvdsmul1  14005  iddvdsexp  14007  muldvds1  14008  muldvds2  14009  dvdscmul  14010  dvdsmulc  14011  dvdscmulr  14012  dvdsmulcr  14013  dvds2ln  14014  dvds2add  14015  dvds2sub  14016  dvdstr  14018  dvdssub2  14023  dvdsadd  14024  dvdsaddr  14025  dvdssub  14026  dvdssubr  14027  dvdsadd2b  14028  alzdvds  14036  mulmoddvds  14044  odd2np1lem  14045  odd2np1  14046  oddp1even  14048  divalglem0  14051  divalglem2  14053  divalglem4  14054  divalglem5  14055  divalglem9  14059  divalgb  14062  divalgmod  14064  ndvdssub  14065  ndvdsadd  14066  bits0  14078  bitsp1e  14082  bitsp1o  14083  gcdneg  14164  gcdaddmlem  14166  gcdaddm  14167  gcdadd  14168  gcdid  14169  modgcd  14174  bezoutlem1  14176  bezoutlem2  14177  bezoutlem4  14179  dvdsgcd  14181  mulgcd  14184  absmulgcd  14185  mulgcdr  14186  gcddiv  14187  gcdmultiplez  14189  dvdssqim  14191  dvdssq  14198  coprmdvds  14243  coprmdvds2  14244  qredeq  14247  qredeu  14248  prmdvdsexp  14255  rpexp1i  14262  divnumden  14281  zsqrtelqelz  14291  phiprmpw  14306  nnnn0modprm0  14331  modprmn0modprm0  14332  coprimeprodsq2  14334  opoe  14335  omoe  14336  opeo  14337  omeo  14338  iserodd  14359  pclem  14362  pcprendvds2  14365  pcpremul  14367  pcmul  14375  pcneg  14397  fldivp1  14416  prmpwdvds  14422  zgz  14451  modxai  14554  mod2xnegi  14557  mulgz  16163  odmod  16570  odf1  16584  odf1o1  16592  gexdvds  16604  zaddablx  16876  cygabl  16893  ablfacrp  17117  pgpfac1lem3  17128  zsubrg  18471  zsssubrg  18476  zringmulg  18496  zrngmulg  18503  zringcyg  18513  zcyg  18518  zringinvg  18519  zringunit  18520  zrngunit  18521  prmirred  18525  prmirredOLD  18528  mulgrhm2  18533  mulgrhm2OLD  18536  znunit  18602  degltp1le  22473  ef2kpi  22871  efper  22872  sinperlem  22873  sin2kpi  22876  cos2kpi  22877  abssinper  22911  sinkpi  22912  coskpi  22913  eflogeq  22986  cxpexpz  23048  root1eq1  23129  cxpeq  23131  leibpilem1  23271  sgmval2  23417  ppiprm  23425  ppinprm  23426  chtprm  23427  chtnprm  23428  lgslem3  23573  lgsneg  23594  lgsdir2lem2  23599  lgsdir2lem4  23601  lgsdir2  23603  lgsdirnn0  23614  lgsquadlem1  23629  lgsquadlem2  23630  lgsquad2  23635  2sqlem2  23639  2sqlem7  23645  rplogsumlem2  23670  axlowdimlem13  24257  wlkdvspthlem  24609  clwwisshclwwlem1  24805  gxneg  25268  gxsuc  25274  gxnn0add  25276  gxadd  25277  gxsub  25278  gxnn0mul  25279  gxmul  25280  zaddsubgo  25356  ipasslem5  25750  rearchi  27832  m1expevenALT  28663  pdivsq  29174  dvdspw  29175  itg2addnclem2  30067  lzenom  30703  rexzrexnn0  30737  pell1234qrne0  30789  pell1234qrreccl  30790  pell1234qrmulcl  30791  pell1234qrdich  30797  pell14qrdich  30805  reglogexp  30830  reglogexpbas  30833  rmxm1  30870  rmym1  30871  rmxdbl  30875  rmydbl  30876  jm2.24  30901  congtr  30903  congadd  30904  congmul  30905  congsym  30906  congneg  30907  congid  30909  congabseq  30912  acongsym  30914  acongneg2  30915  acongtr  30916  acongrep  30918  bezoutr1  30924  dvdsabsmod0  30928  jm2.19lem3  30933  jm2.19lem4  30934  jm2.19  30935  jm2.25  30941  jm2.26a  30942  lcmcllem  31202  lcmneg  31209  lcmgcdlem  31212  lcmgcd  31213  lcmid  31215  oddfl  31459  znnn0nn  31489  coskpi2  31666  cosknegpi  31669  dvdsn1add  31736  itgsinexp  31753  fourierdlem42  31931  fourierdlem97  31986  fourierswlem  32013  2elfz2melfz  32334  0nodd  32498  2nodd  32500  1neven  32738  2zlidl  32740  2zrngamgm  32745  2zrngasgrp  32746  2zrngagrp  32749  2zrngmmgm  32752  2zrngmsgrp  32753  2zrngnmrid  32756  zlmodzxzsub  32949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-resscn 9570
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-neg 9831  df-z 10890
  Copyright terms: Public domain W3C validator