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

Theorem zcn 11211
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 11210 . 2 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
21recnd 9920 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1975  cc 9786  cz 11206
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-resscn 9845
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-rex 2897  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-iota 5750  df-fv 5794  df-ov 6526  df-neg 10116  df-z 11207
This theorem is referenced by:  zsscn  11214  zsubcl  11248  zrevaddcl  11251  nzadd  11254  zlem1lt  11258  zltlem1  11259  zdiv  11275  zdivadd  11276  zdivmul  11277  zextlt  11279  zneo  11288  zeo2  11292  peano5uzi  11294  zindd  11306  znnn0nn  11317  zriotaneg  11319  zmax  11613  rebtwnz  11615  qmulz  11619  zq  11622  qaddcl  11632  qnegcl  11633  qmulcl  11634  qreccl  11636  fzen  12180  uzsubsubfz  12185  fz01en  12191  fzmmmeqm  12196  fzsubel  12199  fztp  12218  fzsuc2  12219  fzrev2  12225  fzrev3  12227  elfzp1b  12237  fzrevral  12245  fzrevral2  12246  fzrevral3  12247  fzshftral  12248  fzo0addel  12340  fzo0addelr  12341  fzoaddel2  12342  elfzoext  12343  fzosubel2  12346  eluzgtdifelfzo  12348  fzocatel  12350  elfzom1elp1fzo  12353  fzval3  12355  zpnn0elfzo1  12359  fzosplitprm1  12394  fzoshftral  12398  flzadd  12440  2tnp1ge0ge0  12443  ceilid  12463  quoremz  12467  intfracq  12471  mulmod0  12489  zmod10  12499  modcyc  12518  modcyc2  12519  muladdmodid  12523  mulp1mod1  12524  modmuladdnn0  12527  modmul1  12536  modmulmodr  12549  modaddmulmod  12550  uzrdgxfr  12579  fzen2  12581  seqshft2  12640  sermono  12646  m1expeven  12720  expsub  12721  zesq  12800  modexp  12812  sqoddm1div8  12841  bccmpl  12909  swrd00  13212  addlenrevswrd  13231  swrdswrd  13254  swrdswrd0  13256  swrdccatin12lem1  13277  swrdccatin12lem2b  13279  swrdccatin2  13280  swrdccatin12lem2  13282  swrdccatin12  13284  repswrevw  13326  cshwsublen  13335  cshwidxmodr  13343  cshwidx0mod  13344  2cshw  13352  2cshwid  13353  2cshwcom  13355  cshweqdif2  13358  cshweqrep  13360  cshw1  13361  2cshwcshw  13364  shftuz  13599  seqshft  13615  nn0abscl  13842  nnabscl  13855  climshftlem  14095  climshft  14097  isershft  14184  mptfzshft  14294  fsumrev  14295  fsum0diag2  14299  efexp  14612  efzval  14613  demoivre  14711  znnenlem  14721  sqrt2irr  14759  dvdsval2  14766  iddvds  14775  1dvds  14776  dvds0  14777  negdvdsb  14778  dvdsnegb  14779  0dvds  14782  dvdsmul1  14783  iddvdsexp  14785  muldvds1  14786  muldvds2  14787  dvdscmul  14788  dvdsmulc  14789  dvdscmulr  14790  dvdsmulcr  14791  summodnegmod  14792  modmulconst  14793  dvds2ln  14794  dvds2add  14795  dvds2sub  14796  dvdstr  14798  dvdssub2  14803  dvdsadd  14804  dvdsaddr  14805  dvdssub  14806  dvdssubr  14807  dvdsadd2b  14808  dvdsaddre2b  14809  dvdsabseq  14815  divconjdvds  14817  alzdvds  14822  addmodlteqALT  14827  mulmoddvds  14831  odd2np1lem  14844  odd2np1  14845  even2n  14846  oddp1even  14848  mod2eq1n2dvds  14851  mulsucdiv2z  14857  zob  14863  ltoddhalfle  14865  halfleoddlt  14866  opoe  14867  omoe  14868  opeo  14869  omeo  14870  m1exp1  14873  divalglem0  14896  divalglem2  14898  divalglem4  14899  divalglem5  14900  divalglem9  14904  divalgb  14907  divalgmod  14909  divalgmodOLD  14910  modremain  14912  ndvdssub  14913  ndvdsadd  14914  flodddiv4  14917  flodddiv4t2lthalf  14920  bits0  14930  bitsp1e  14934  bitsp1o  14935  gcdneg  15023  gcdaddmlem  15025  gcdaddm  15026  gcdadd  15027  gcdid  15028  modgcd  15033  bezoutlem1  15036  bezoutlem2  15037  bezoutlem4  15039  dvdsgcd  15041  mulgcd  15045  absmulgcd  15046  mulgcdr  15047  gcddiv  15048  gcdmultiplez  15050  dvdssqim  15053  dvdssq  15060  bezoutr1  15062  lcmcllem  15089  lcmneg  15096  lcmgcdlem  15099  lcmgcd  15100  lcmid  15102  lcm1  15103  coprmdvds  15146  coprmdvdsOLD  15147  coprmdvds2  15148  qredeq  15151  qredeu  15152  divgcdcoprmex  15160  cncongr1  15161  cncongr2  15162  prmdvdsexp  15207  rpexp1i  15213  divnumden  15236  zsqrtelqelz  15246  phiprmpw  15261  vfermltlALT  15287  nnnn0modprm0  15291  modprmn0modprm0  15292  coprimeprodsq2  15294  iserodd  15320  pclem  15323  pcprendvds2  15326  pcpremul  15328  pcmul  15336  pcneg  15358  fldivp1  15381  prmpwdvds  15388  zgz  15417  modxai  15552  mod2xnegi  15555  mulgz  17333  mulgassr  17345  mulgmodid  17346  odmod  17730  odf1  17744  odf1o1  17752  gexdvds  17764  zaddablx  18040  cygabl  18057  ablfacrp  18230  pgpfac1lem3  18241  zsubrg  19560  zsssubrg  19565  zringmulg  19587  zringcyg  19597  zringinvg  19598  zringunit  19599  prmirred  19603  mulgrhm2  19607  znunit  19672  degltp1le  23550  ef2kpi  23947  efper  23948  sinperlem  23949  sin2kpi  23952  cos2kpi  23953  abssinper  23987  sinkpi  23988  coskpi  23989  eflogeq  24065  cxpexpz  24126  root1eq1  24209  cxpeq  24211  relogbexp  24231  leibpilem1  24380  sgmval2  24582  ppiprm  24590  ppinprm  24591  chtprm  24592  chtnprm  24593  lgslem3  24737  lgsneg  24759  lgsdir2lem2  24764  lgsdir2lem4  24766  lgsdir2  24768  lgssq  24775  lgsmulsqcoprm  24781  lgsdirnn0  24782  gausslemma2dlem3  24806  lgsquadlem1  24818  lgsquadlem2  24819  lgsquad2  24824  2lgslem1a2  24828  2lgsoddprmlem1  24846  2lgsoddprmlem2  24847  2sqlem2  24856  2sqlem7  24862  rplogsumlem2  24887  axlowdimlem13  25548  wlkdvspthlem  25899  clwwisshclwwlem1  26095  ipasslem5  26876  rearchi  28975  pdivsq  30690  dvdspw  30691  knoppndvlem9  31483  poimirlem19  32397  itg2addnclem2  32431  lzenom  36150  rexzrexnn0  36185  pell1234qrne0  36234  pell1234qrreccl  36235  pell1234qrmulcl  36236  pell1234qrdich  36242  pell14qrdich  36250  reglogexp  36275  reglogexpbas  36278  rmxm1  36316  rmym1  36317  rmxdbl  36321  rmydbl  36322  jm2.24  36347  congtr  36349  congadd  36350  congmul  36351  congsym  36352  congneg  36353  congid  36355  congabseq  36358  acongsym  36360  acongneg2  36361  acongtr  36362  acongrep  36364  jm2.19lem3  36375  jm2.19lem4  36376  jm2.19  36377  jm2.25  36383  jm2.26a  36384  oddfl  38229  coskpi2  38549  cosknegpi  38552  dvdsn1add  38629  itgsinexp  38646  fourierdlem42  38842  fourierdlem97  38896  fourierswlem  38923  sfprmdvdsmersenne  39859  proththd  39870  dfodd6  39889  dfeven4  39890  evenm1odd  39891  evenp1odd  39892  enege  39897  onego  39898  dfeven2  39901  bits0ALTV  39929  opoeALTV  39933  opeoALTV  39934  evensumeven  39955  bgoldbwt  40000  nnsum3primesgbe  40009  addlenrevpfx  40061  pfxccatin12lem1  40087  pfxccatin12lem2  40088  pfxccatin12  40089  2elfz2melfz  40178  1wlk1walk  40841  clwwisshclwwslemlem  41231  0nodd  41598  2nodd  41600  1neven  41720  2zlidl  41722  2zrngamgm  41727  2zrngasgrp  41728  2zrngagrp  41731  2zrngmmgm  41734  2zrngmsgrp  41735  2zrngnmrid  41738  zlmodzxzsub  41929  flsubz  42104  mod0mul  42106  m1modmmod  42108  zofldiv2  42117  dignn0flhalflem1  42205  dignn0flhalflem2  42206
  Copyright terms: Public domain W3C validator