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

Theorem zcn 10385
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 10384 . 2 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
21recnd 9211 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1734  cc 9085  cz 10380
This theorem is referenced by:  zsscn  10388  zsubcl  10417  zrevaddcl  10419  zlem1lt  10425  zltlem1  10426  zdiv  10438  zdivadd  10439  zdivmul  10440  zextlt  10442  zneo  10450  zeo2  10454  peano5uzi  10456  uzindOLD  10462  zindd  10469  zmax  10671  rebtwnz  10673  qmulz  10677  zq  10680  qaddcl  10690  qnegcl  10691  qmulcl  10692  qreccl  10694  fzen  11172  fz01en  11179  fzsubel  11188  fztp  11202  fzsuc2  11204  fzrev2  11209  fzrev3  11211  elfzp1b  11225  fzrevral  11232  fzrevral2  11233  fzrevral3  11234  fzshftral  11235  fzoaddel2  11277  fzosubel2  11279  fzval3  11281  flzadd  11330  quoremz  11338  intfracq  11342  zmod10  11366  modcyc  11379  modcyc2  11380  modmul1  11383  uzrdgxfr  11410  fzen2  11412  seqshft2  11453  sermono  11459  expsub  11531  zesq  11606  modexp  11618  bccmpl  11704  swrd00  11875  shftuz  11994  seqshft  12010  nn0abscl  12237  nnabscl  12249  climshftlem  12488  climshft  12490  isershft  12577  fsumrev  12682  fsumshft  12683  fsum0diag2  12686  efexp  12822  efzval  12823  demoivre  12921  znnenlem  12931  sqr2irr  12968  dvdsval2  12975  iddvds  12983  1dvds  12984  dvds0  12985  negdvdsb  12986  dvdsnegb  12987  0dvds  12990  dvdsmul1  12991  iddvdsexp  12993  muldvds1  12994  muldvds2  12995  dvdscmul  12996  dvdsmulc  12997  dvdscmulr  12998  dvdsmulcr  12999  dvds2ln  13000  dvds2add  13001  dvds2sub  13002  dvdstr  13003  dvdssub2  13007  dvdsadd  13008  dvdsaddr  13009  dvdssub  13010  dvdssubr  13011  dvdsadd2b  13012  alzdvds  13019  odd2np1lem  13027  odd2np1  13028  oddp1even  13030  divalglem0  13033  divalglem2  13035  divalglem4  13036  divalglem5  13037  divalglem9  13041  divalgb  13044  divalgmod  13046  ndvdssub  13047  ndvdsadd  13048  bits0  13060  bitsp1e  13064  bitsp1o  13065  gcdneg  13146  gcdaddmlem  13148  gcdaddm  13149  gcdadd  13150  gcdid  13151  modgcd  13156  bezoutlem1  13158  bezoutlem2  13159  bezoutlem4  13161  dvdsgcd  13163  mulgcd  13166  absmulgcd  13167  mulgcdr  13168  gcddiv  13169  gcdmultiplez  13171  dvdssqim  13173  dvdssq  13180  coprmdvds  13222  coprmdvds2  13223  qredeq  13226  qredeu  13227  prmdvdsexp  13234  rpexp1i  13241  divnumden  13260  zsqrelqelz  13270  phiprmpw  13285  coprimeprodsq2  13304  opoe  13305  omoe  13306  opeo  13307  omeo  13308  iserodd  13329  pclem  13332  pcprendvds2  13335  pcpremul  13337  pcmul  13345  pcneg  13367  fldivp1  13386  prmpwdvds  13392  zgz  13421  modxai  13524  mod2xnegi  13527  mulgz  15043  odmod  15316  odf1  15330  odf1o1  15338  gexdvds  15350  zaddablx  15615  cygabl  15632  ablfacrp  15756  pgpfac1lem3  15767  zsubrg  16884  zsssubrg  16889  zrngunit  16897  zcyg  16904  prmirred  16907  mulgrhm2  16920  znunit  16976  degltp1le  20128  ef2kpi  20518  efper  20519  sinperlem  20520  sin2kpi  20523  cos2kpi  20524  abssinper  20558  sinkpi  20559  coskpi  20560  eflogeq  20628  cxpexpz  20690  root1eq1  20771  cxpeq  20773  leibpilem1  20912  sgmval2  21058  ppiprm  21066  ppinprm  21067  chtprm  21068  chtnprm  21069  lgslem3  21214  lgsneg  21235  lgsdir2lem2  21240  lgsdir2lem4  21242  lgsdir2  21244  lgsdirnn0  21255  lgsquadlem1  21270  lgsquadlem2  21271  lgsquad2  21276  2sqlem2  21280  2sqlem7  21286  rplogsumlem2  21311  wlkdvspthlem  21739  gxneg  21986  gxsuc  21992  gxnn0add  21994  gxadd  21995  gxsub  21996  gxnn0mul  21997  gxmul  21998  zaddsubgo  22074  ipasslem5  22468  fzocatel  24324  zzsmulg  24574  rearchi  24607  m1expevenALT  25371  pdivsq  25825  dvdspw  25826  axlowdimlem13  26350  itg2addnclem2  26713  lzenom  27352  rexzrexnn0  27386  pell1234qrne0  27438  pell1234qrreccl  27439  pell1234qrmulcl  27440  pell1234qrdich  27446  pell14qrdich  27454  reglogexp  27479  reglogexpbas  27482  rmxm1  27519  rmym1  27520  rmxdbl  27524  rmydbl  27525  jm2.24  27550  congtr  27552  congadd  27553  congmul  27554  congsym  27555  congneg  27556  congid  27558  congabseq  27561  acongsym  27563  acongneg2  27564  acongtr  27565  acongrep  27567  bezoutr1  27573  dvdsabsmod0  27579  jm2.19lem3  27584  jm2.19lem4  27585  jm2.19  27586  jm2.25  27592  jm2.26a  27593  itgsinexp  28243  fzmmmeqm  28677  2elfz2melfz  28679  uzsubsubfz  28685  ubmelfzo  28694  ubmelm1fzo  28695  fzoshftral  28713  eluzgtdifelfzo  28716  zpnn0elfzo1  28719  fzosplitprm1  28721  modaddmulmod  28740  mulmoddvds  28777  addlenrevswrd  28833  swrd0swrd  28847  swrdswrd  28849  swrdswrd0  28850  swrdccatin12lem2  28870  swrdccatin12lem3b  28872  swrdccatin2  28873  swrdccatin12lem3  28875  swrdccatin12  28877  2cshw1lem1  28920  2cshw2lem1  28924  cshweqdif2  28935  clwwisshclwwlem2  29163  cshwlemma1  29184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-5 1573  ax-17 1636  ax-9 1677  ax-8 1698  ax-6 1753  ax-7 1758  ax-11 1770  ax-12 1963  ax-ext 2460  ax-resscn 9144
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 939  df-3an 940  df-tru 1334  df-ex 1558  df-nf 1561  df-sb 1669  df-clab 2466  df-cleq 2472  df-clel 2475  df-nfc 2604  df-rex 2754  df-rab 2757  df-v 3005  df-dif 3353  df-un 3355  df-in 3357  df-ss 3364  df-nul 3658  df-if 3810  df-sn 3894  df-pr 3895  df-op 3897  df-uni 4094  df-br 4294  df-iota 5516  df-fv 5561  df-ov 6184  df-neg 9392  df-z 10381
  Copyright terms: Public domain W3C validator