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

Theorem zcn 11259
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 11258 . 2 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
21recnd 9947 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  cc 9813  cz 11254
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-resscn 9872
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-neg 10148  df-z 11255
This theorem is referenced by:  zsscn  11262  zsubcl  11296  zrevaddcl  11299  nzadd  11302  zlem1lt  11306  zltlem1  11307  zdiv  11323  zdivadd  11324  zdivmul  11325  zextlt  11327  zneo  11336  zeo2  11340  peano5uzi  11342  zindd  11354  znnn0nn  11365  zriotaneg  11367  zmax  11661  rebtwnz  11663  qmulz  11667  zq  11670  qaddcl  11680  qnegcl  11681  qmulcl  11682  qreccl  11684  fzen  12229  uzsubsubfz  12234  fz01en  12240  fzmmmeqm  12245  fzsubel  12248  fztp  12267  fzsuc2  12268  fzrev2  12274  fzrev3  12276  elfzp1b  12286  fzrevral  12294  fzrevral2  12295  fzrevral3  12296  fzshftral  12297  fzo0addel  12389  fzo0addelr  12390  fzoaddel2  12391  elfzoext  12392  fzosubel2  12395  eluzgtdifelfzo  12397  fzocatel  12399  elfzom1elp1fzo  12402  fzval3  12404  zpnn0elfzo1  12408  fzosplitprm1  12443  fzoshftral  12447  flzadd  12489  2tnp1ge0ge0  12492  ceilid  12512  quoremz  12516  intfracq  12520  mulmod0  12538  zmod10  12548  modcyc  12567  modcyc2  12568  muladdmodid  12572  mulp1mod1  12573  modmuladdnn0  12576  modmul1  12585  modmulmodr  12598  modaddmulmod  12599  uzrdgxfr  12628  fzen2  12630  seqshft2  12689  sermono  12695  m1expeven  12769  expsub  12770  zesq  12849  modexp  12861  sqoddm1div8  12890  bccmpl  12958  swrd00  13270  addlenrevswrd  13289  swrdswrd  13312  swrdswrd0  13314  swrdccatin12lem1  13335  swrdccatin12lem2b  13337  swrdccatin2  13338  swrdccatin12lem2  13340  swrdccatin12  13342  repswrevw  13384  cshwsublen  13393  cshwidxmodr  13401  cshwidx0mod  13402  2cshw  13410  2cshwid  13411  2cshwcom  13413  cshweqdif2  13416  cshweqrep  13418  cshw1  13419  2cshwcshw  13422  shftuz  13657  seqshft  13673  nn0abscl  13900  nnabscl  13913  climshftlem  14153  climshft  14155  isershft  14242  mptfzshft  14352  fsumrev  14353  fsum0diag2  14357  efexp  14670  efzval  14671  demoivre  14769  znnenlem  14779  sqrt2irr  14817  dvdsval2  14824  iddvds  14833  1dvds  14834  dvds0  14835  negdvdsb  14836  dvdsnegb  14837  0dvds  14840  dvdsmul1  14841  iddvdsexp  14843  muldvds1  14844  muldvds2  14845  dvdscmul  14846  dvdsmulc  14847  dvdscmulr  14848  dvdsmulcr  14849  summodnegmod  14850  modmulconst  14851  dvds2ln  14852  dvds2add  14853  dvds2sub  14854  dvdstr  14856  dvdssub2  14861  dvdsadd  14862  dvdsaddr  14863  dvdssub  14864  dvdssubr  14865  dvdsadd2b  14866  dvdsaddre2b  14867  dvdsabseq  14873  divconjdvds  14875  alzdvds  14880  addmodlteqALT  14885  mulmoddvds  14889  odd2np1lem  14902  odd2np1  14903  even2n  14904  oddp1even  14906  mod2eq1n2dvds  14909  mulsucdiv2z  14915  zob  14921  ltoddhalfle  14923  halfleoddlt  14924  opoe  14925  omoe  14926  opeo  14927  omeo  14928  m1exp1  14931  divalglem0  14954  divalglem2  14956  divalglem4  14957  divalglem5  14958  divalglem9  14962  divalgb  14965  divalgmod  14967  divalgmodOLD  14968  modremain  14970  ndvdssub  14971  ndvdsadd  14972  flodddiv4  14975  flodddiv4t2lthalf  14978  bits0  14988  bitsp1e  14992  bitsp1o  14993  gcdneg  15081  gcdaddmlem  15083  gcdaddm  15084  gcdadd  15085  gcdid  15086  modgcd  15091  bezoutlem1  15094  bezoutlem2  15095  bezoutlem4  15097  dvdsgcd  15099  mulgcd  15103  absmulgcd  15104  mulgcdr  15105  gcddiv  15106  gcdmultiplez  15108  dvdssqim  15111  dvdssq  15118  bezoutr1  15120  lcmcllem  15147  lcmneg  15154  lcmgcdlem  15157  lcmgcd  15158  lcmid  15160  lcm1  15161  coprmdvds  15204  coprmdvdsOLD  15205  coprmdvds2  15206  qredeq  15209  qredeu  15210  divgcdcoprmex  15218  cncongr1  15219  cncongr2  15220  prmdvdsexp  15265  rpexp1i  15271  divnumden  15294  zsqrtelqelz  15304  phiprmpw  15319  vfermltlALT  15345  nnnn0modprm0  15349  modprmn0modprm0  15350  coprimeprodsq2  15352  iserodd  15378  pclem  15381  pcprendvds2  15384  pcpremul  15386  pcmul  15394  pcneg  15416  fldivp1  15439  prmpwdvds  15446  zgz  15475  modxai  15610  mod2xnegi  15613  mulgz  17391  mulgassr  17403  mulgmodid  17404  odmod  17788  odf1  17802  odf1o1  17810  gexdvds  17822  zaddablx  18098  cygabl  18115  ablfacrp  18288  pgpfac1lem3  18299  zsubrg  19618  zsssubrg  19623  zringmulg  19645  zringinvg  19654  zringunit  19655  zringcyg  19658  prmirred  19662  mulgrhm2  19666  znunit  19731  degltp1le  23637  ef2kpi  24034  efper  24035  sinperlem  24036  sin2kpi  24039  cos2kpi  24040  abssinper  24074  sinkpi  24075  coskpi  24076  eflogeq  24152  cxpexpz  24213  root1eq1  24296  cxpeq  24298  relogbexp  24318  leibpilem1  24467  sgmval2  24669  ppiprm  24677  ppinprm  24678  chtprm  24679  chtnprm  24680  lgslem3  24824  lgsneg  24846  lgsdir2lem2  24851  lgsdir2lem4  24853  lgsdir2  24855  lgssq  24862  lgsmulsqcoprm  24868  lgsdirnn0  24869  gausslemma2dlem3  24893  lgsquadlem1  24905  lgsquadlem2  24906  lgsquad2  24911  2lgslem1a2  24915  2lgsoddprmlem1  24933  2lgsoddprmlem2  24934  2sqlem2  24943  2sqlem7  24949  rplogsumlem2  24974  axlowdimlem13  25634  wlkdvspthlem  26137  clwwisshclwwlem1  26333  ipasslem5  27074  rearchi  29173  pdivsq  30888  dvdspw  30889  knoppndvlem9  31681  poimirlem19  32598  itg2addnclem2  32632  lzenom  36351  rexzrexnn0  36386  pell1234qrne0  36435  pell1234qrreccl  36436  pell1234qrmulcl  36437  pell1234qrdich  36443  pell14qrdich  36451  reglogexp  36476  reglogexpbas  36479  rmxm1  36517  rmym1  36518  rmxdbl  36522  rmydbl  36523  jm2.24  36548  congtr  36550  congadd  36551  congmul  36552  congsym  36553  congneg  36554  congid  36556  congabseq  36559  acongsym  36561  acongneg2  36562  acongtr  36563  acongrep  36565  jm2.19lem3  36576  jm2.19lem4  36577  jm2.19  36578  jm2.25  36584  jm2.26a  36585  oddfl  38430  coskpi2  38749  cosknegpi  38752  dvdsn1add  38829  itgsinexp  38846  fourierdlem42  39042  fourierdlem97  39096  fourierswlem  39123  sfprmdvdsmersenne  40058  proththd  40069  dfodd6  40088  dfeven4  40089  evenm1odd  40090  evenp1odd  40091  enege  40096  onego  40097  dfeven2  40100  bits0ALTV  40128  opoeALTV  40132  opeoALTV  40133  evensumeven  40154  bgoldbwt  40199  nnsum3primesgbe  40208  addlenrevpfx  40260  pfxccatin12lem1  40286  pfxccatin12lem2  40287  pfxccatin12  40288  2elfz2melfz  40355  1wlk1walk  40843  clwwisshclwwslemlem  41233  0nodd  41600  2nodd  41602  1neven  41722  2zlidl  41724  2zrngamgm  41729  2zrngasgrp  41730  2zrngagrp  41733  2zrngmmgm  41736  2zrngmsgrp  41737  2zrngnmrid  41740  zlmodzxzsub  41931  flsubz  42106  mod0mul  42108  m1modmmod  42110  zofldiv2  42119  dignn0flhalflem1  42207  dignn0flhalflem2  42208
  Copyright terms: Public domain W3C validator