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

Theorem zcn 11574
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 11573 . 2 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
21recnd 10260 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  cc 10126  cz 11569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-resscn 10185
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6816  df-neg 10461  df-z 11570
This theorem is referenced by:  zsscn  11577  zsubcl  11611  zrevaddcl  11614  nzadd  11617  zlem1lt  11621  zltlem1  11622  zdiv  11639  zdivadd  11640  zdivmul  11641  zextlt  11643  zneo  11652  zeo2  11656  peano5uzi  11658  zindd  11670  znnn0nn  11681  zriotaneg  11683  zmax  11978  rebtwnz  11980  qmulz  11984  zq  11987  qaddcl  11997  qnegcl  11998  qmulcl  11999  qreccl  12001  fzen  12551  uzsubsubfz  12556  fz01en  12562  fzmmmeqm  12567  fzsubel  12570  fztp  12590  fzsuc2  12591  fzrev2  12597  fzrev3  12599  elfzp1b  12610  fzrevral  12618  fzrevral2  12619  fzrevral3  12620  fzshftral  12621  fzo0addel  12716  fzo0addelr  12717  fzoaddel2  12718  elfzoext  12719  fzosubel2  12722  eluzgtdifelfzo  12724  fzocatel  12726  elfzom1elp1fzo  12729  fzval3  12731  zpnn0elfzo1  12736  fzosplitprm1  12772  fzoshftral  12779  flzadd  12821  2tnp1ge0ge0  12824  ceilid  12844  quoremz  12848  intfracq  12852  mulmod0  12870  zmod10  12880  modcyc  12899  modcyc2  12900  muladdmodid  12904  mulp1mod1  12905  modmuladdnn0  12908  modmul1  12917  modmulmodr  12930  modaddmulmod  12931  uzrdgxfr  12960  fzen2  12962  seqshft2  13021  sermono  13027  m1expeven  13101  expsub  13102  zesq  13181  modexp  13193  sqoddm1div8  13222  bccmpl  13290  swrd00  13617  addlenrevswrd  13637  swrdswrd  13660  swrdswrd0  13662  swrdccatin12lem1  13684  swrdccatin12lem2b  13686  swrdccatin2  13687  swrdccatin12lem2  13689  swrdccatin12  13691  repswrevw  13733  cshwsublen  13742  cshwidxmodr  13750  cshwidx0mod  13751  2cshw  13759  2cshwid  13760  2cshwcom  13762  cshweqdif2  13765  cshweqrep  13767  cshw1  13768  2cshwcshw  13771  shftuz  14008  seqshft  14024  nn0abscl  14251  nnabscl  14264  climshftlem  14504  climshft  14506  isershft  14593  mptfzshft  14709  fsumrev  14710  fsum0diag2  14714  efexp  15030  efzval  15031  demoivre  15129  znnenlem  15139  sqrt2irr  15178  dvdsval2  15185  iddvds  15197  1dvds  15198  dvds0  15199  negdvdsb  15200  dvdsnegb  15201  0dvds  15204  dvdsmul1  15205  iddvdsexp  15207  muldvds1  15208  muldvds2  15209  dvdscmul  15210  dvdsmulc  15211  dvdscmulr  15212  dvdsmulcr  15213  summodnegmod  15214  modmulconst  15215  dvds2ln  15216  dvds2add  15217  dvds2sub  15218  dvdstr  15220  dvdssub2  15225  dvdsadd  15226  dvdsaddr  15227  dvdssub  15228  dvdssubr  15229  dvdsadd2b  15230  dvdsaddre2b  15231  dvdsabseq  15237  divconjdvds  15239  alzdvds  15244  addmodlteqALT  15249  odd2np1lem  15266  odd2np1  15267  even2n  15268  oddp1even  15270  mod2eq1n2dvds  15273  mulsucdiv2z  15279  zob  15285  ltoddhalfle  15287  halfleoddlt  15288  opoe  15289  omoe  15290  opeo  15291  omeo  15292  m1exp1  15295  divalglem0  15318  divalglem2  15320  divalglem4  15321  divalglem5  15322  divalglem9  15326  divalgb  15329  divalgmod  15331  divalgmodOLD  15332  modremain  15334  ndvdssub  15335  ndvdsadd  15336  flodddiv4  15339  flodddiv4t2lthalf  15342  bits0  15352  bitsp1e  15356  bitsp1o  15357  gcdneg  15445  gcdaddmlem  15447  gcdaddm  15448  gcdadd  15449  gcdid  15450  modgcd  15455  bezoutlem1  15458  bezoutlem2  15459  bezoutlem4  15461  dvdsgcd  15463  mulgcd  15467  absmulgcd  15468  mulgcdr  15469  gcddiv  15470  gcdmultiplez  15472  dvdssqim  15475  dvdssq  15482  bezoutr1  15484  lcmcllem  15511  lcmneg  15518  lcmgcdlem  15521  lcmgcd  15522  lcmid  15524  lcm1  15525  coprmdvds  15568  coprmdvdsOLD  15569  coprmdvds2  15570  qredeq  15573  qredeu  15574  divgcdcoprmex  15582  cncongr1  15583  cncongr2  15584  prmdvdsexp  15629  rpexp1i  15635  divnumden  15658  zsqrtelqelz  15668  phiprmpw  15683  vfermltlALT  15709  nnnn0modprm0  15713  modprmn0modprm0  15714  coprimeprodsq2  15716  iserodd  15742  pclem  15745  pcprendvds2  15748  pcpremul  15750  pcmul  15758  pcneg  15780  fldivp1  15803  prmpwdvds  15810  zgz  15839  modxai  15974  mod2xnegi  15977  mulgz  17769  mulgassr  17781  mulgmodid  17782  odmod  18165  odf1  18179  odf1o1  18187  gexdvds  18199  zaddablx  18475  cygabl  18492  ablfacrp  18665  pgpfac1lem3  18676  zsubrg  20001  zsssubrg  20006  zringmulg  20028  zringinvg  20037  zringunit  20038  zringcyg  20041  prmirred  20045  mulgrhm2  20049  znunit  20114  degltp1le  24032  ef2kpi  24429  efper  24430  sinperlem  24431  sin2kpi  24434  cos2kpi  24435  abssinper  24469  sinkpi  24470  coskpi  24471  eflogeq  24547  cxpexpz  24612  root1eq1  24695  cxpeq  24697  relogbexp  24717  leibpilem1  24866  sgmval2  25068  ppiprm  25076  ppinprm  25077  chtprm  25078  chtnprm  25079  lgslem3  25223  lgsneg  25245  lgsdir2lem2  25250  lgsdir2lem4  25252  lgsdir2  25254  lgssq  25261  lgsmulsqcoprm  25267  lgsdirnn0  25268  gausslemma2dlem3  25292  lgsquadlem1  25304  lgsquadlem2  25305  lgsquad2  25310  2lgslem1a2  25314  2lgsoddprmlem1  25332  2lgsoddprmlem2  25333  2sqlem2  25342  2sqlem7  25348  rplogsumlem2  25373  axlowdimlem13  26033  wlk1walk  26745  clwwisshclwwslemlem  27136  ipasslem5  27999  rearchi  30151  pdivsq  31942  dvdspw  31943  knoppndvlem9  32817  poimirlem19  33741  itg2addnclem2  33775  lzenom  37835  rexzrexnn0  37870  pell1234qrne0  37919  pell1234qrreccl  37920  pell1234qrmulcl  37921  pell1234qrdich  37927  pell14qrdich  37935  reglogexp  37960  reglogexpbas  37963  rmxm1  38001  rmym1  38002  rmxdbl  38006  rmydbl  38007  jm2.24  38032  congtr  38034  congadd  38035  congmul  38036  congsym  38037  congneg  38038  congid  38040  congabseq  38043  acongsym  38045  acongneg2  38046  acongtr  38047  acongrep  38049  jm2.19lem3  38060  jm2.19lem4  38061  jm2.19  38062  jm2.25  38068  jm2.26a  38069  oddfl  39988  coskpi2  40580  cosknegpi  40583  dvdsn1add  40657  itgsinexp  40673  fourierdlem42  40869  fourierdlem97  40923  fourierswlem  40950  2elfz2melfz  41838  addlenrevpfx  41907  pfxccatin12lem1  41933  pfxccatin12lem2  41934  pfxccatin12  41935  sfprmdvdsmersenne  42030  proththd  42041  dfodd6  42060  dfeven4  42061  evenm1odd  42062  evenp1odd  42063  enege  42068  onego  42069  dfeven2  42072  bits0ALTV  42100  opoeALTV  42104  opeoALTV  42105  evensumeven  42126  sbgoldbwt  42175  nnsum3primesgbe  42190  0nodd  42320  2nodd  42322  1neven  42442  2zlidl  42444  2zrngamgm  42449  2zrngasgrp  42450  2zrngagrp  42453  2zrngmmgm  42456  2zrngmsgrp  42457  2zrngnmrid  42460  zlmodzxzsub  42648  flsubz  42822  mod0mul  42824  m1modmmod  42826  zofldiv2  42835  dignn0flhalflem1  42919  dignn0flhalflem2  42920
  Copyright terms: Public domain W3C validator