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

Theorem zcn 11978
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 11977 . 2 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
21recnd 10662 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  cc 10528  cz 11973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-resscn 10587
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-rab 3118  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-ov 7142  df-neg 10866  df-z 11974
This theorem is referenced by:  zsscn  11981  zsubcl  12016  zrevaddcl  12019  nzadd  12022  zlem1lt  12026  zltlem1  12027  zdiv  12044  zdivadd  12045  zdivmul  12046  zextlt  12048  zneo  12057  zeo2  12061  peano5uzi  12063  zindd  12075  znnn0nn  12086  zriotaneg  12088  zmax  12337  rebtwnz  12339  qmulz  12343  zq  12346  qaddcl  12356  qnegcl  12357  qmulcl  12358  qreccl  12360  fzen  12923  uzsubsubfz  12928  fz01en  12934  fzmmmeqm  12939  fzsubel  12942  fztp  12962  fzsuc2  12964  fzrev2  12970  fzrev3  12972  elfzp1b  12983  fzrevral  12991  fzrevral2  12992  fzrevral3  12993  fzshftral  12994  fzo0addel  13090  fzo0addelr  13091  fzoaddel2  13092  elfzoext  13093  fzosubel2  13096  eluzgtdifelfzo  13098  fzocatel  13100  elfzom1elp1fzo  13103  fzval3  13105  zpnn0elfzo1  13110  fzosplitprm1  13146  fzoshftral  13153  flzadd  13195  2tnp1ge0ge0  13198  ceilid  13218  quoremz  13222  intfracq  13226  mulmod0  13244  zmod10  13254  modcyc  13273  modcyc2  13274  muladdmodid  13278  mulp1mod1  13279  modmuladdnn0  13282  modmul1  13291  modmulmodr  13304  modaddmulmod  13305  uzrdgxfr  13334  fzen2  13336  seqshft2  13396  sermono  13402  m1expeven  13476  expsub  13477  zesq  13587  modexp  13599  sqoddm1div8  13604  bccmpl  13669  swrd00  14001  addlenrevpfx  14047  swrdswrd  14062  swrdpfx  14064  pfxccatin12lem4  14083  pfxccatin12lem1  14085  swrdccatin2  14086  pfxccatin12lem2  14088  pfxccatin12  14090  repswrevw  14144  cshwsublen  14153  cshwidxmodr  14161  cshwidx0mod  14162  2cshw  14170  2cshwid  14171  2cshwcom  14173  cshweqdif2  14176  cshweqrep  14178  cshw1  14179  2cshwcshw  14182  shftuz  14424  seqshft  14440  nn0abscl  14668  nnabscl  14681  climshftlem  14927  climshft  14929  isershft  15016  mptfzshft  15129  fsumrev  15130  fsum0diag2  15134  efexp  15450  efzval  15451  demoivre  15549  sqrt2irr  15598  dvdsval2  15606  iddvds  15619  1dvds  15620  dvds0  15621  negdvdsb  15622  dvdsnegb  15623  0dvds  15626  dvdsmul1  15627  iddvdsexp  15629  muldvds1  15630  muldvds2  15631  dvdscmul  15632  dvdsmulc  15633  dvdscmulr  15634  dvdsmulcr  15635  summodnegmod  15636  modmulconst  15637  dvds2ln  15638  dvds2add  15639  dvds2sub  15640  dvdstr  15642  dvdssub2  15647  dvdsadd  15648  dvdsaddr  15649  dvdssub  15650  dvdssubr  15651  dvdsadd2b  15652  dvdsaddre2b  15653  dvdsabseq  15659  divconjdvds  15661  alzdvds  15666  addmodlteqALT  15671  odd2np1lem  15685  odd2np1  15686  even2n  15687  oddp1even  15689  mod2eq1n2dvds  15692  mulsucdiv2z  15698  zob  15704  ltoddhalfle  15706  halfleoddlt  15707  opoe  15708  omoe  15709  opeo  15710  omeo  15711  m1exp1  15721  divalglem0  15738  divalglem2  15740  divalglem4  15741  divalglem5  15742  divalglem9  15746  divalgb  15749  divalgmod  15751  modremain  15753  ndvdssub  15754  ndvdsadd  15755  flodddiv4  15758  flodddiv4t2lthalf  15761  bits0  15771  bitsp1e  15775  bitsp1o  15776  gcdneg  15864  gcdaddmlem  15866  gcdaddm  15867  gcdadd  15868  gcdid  15869  modgcd  15874  gcdmultiplez  15877  bezoutlem1  15881  bezoutlem2  15882  bezoutlem4  15884  dvdsgcd  15886  mulgcd  15890  absmulgcd  15891  mulgcdr  15892  gcddiv  15893  gcdmultiplezOLD  15895  dvdssqim  15898  dvdssq  15905  bezoutr1  15907  lcmcllem  15934  lcmneg  15941  lcmgcdlem  15944  lcmgcd  15945  lcmid  15947  lcm1  15948  coprmdvds  15991  coprmdvds2  15992  qredeq  15995  qredeu  15996  divgcdcoprmex  16004  cncongr1  16005  cncongr2  16006  prmdvdsexp  16053  rpexp1i  16059  divnumden  16082  zsqrtelqelz  16092  phiprmpw  16107  vfermltlALT  16133  nnnn0modprm0  16137  modprmn0modprm0  16138  coprimeprodsq2  16140  iserodd  16166  pclem  16169  pcprendvds2  16172  pcpremul  16174  pcmul  16182  pcneg  16204  fldivp1  16227  prmpwdvds  16234  zgz  16263  modxai  16398  mod2xnegi  16401  mulgfval  18222  mulgz  18251  mulgassr  18261  mulgmodid  18262  odmod  18670  odf1  18685  odf1o1  18693  gexdvds  18705  zaddablx  18989  cygablOLD  19008  ablfacrp  19185  pgpfac1lem3  19196  ablsimpgfindlem1  19226  zsubrg  20148  zsssubrg  20153  zringmulg  20175  zringinvg  20184  zringunit  20185  zringcyg  20188  prmirred  20192  mulgrhm2  20196  znunit  20259  degltp1le  24678  ef2kpi  25075  efper  25076  sinperlem  25077  sin2kpi  25080  cos2kpi  25081  abssinper  25117  sinkpi  25118  coskpi  25119  eflogeq  25197  cxpexpz  25262  root1eq1  25348  cxpeq  25350  relogbexp  25370  sgmval2  25732  ppiprm  25740  ppinprm  25741  chtprm  25742  chtnprm  25743  lgslem3  25887  lgsneg  25909  lgsdir2lem2  25914  lgsdir2lem4  25916  lgsdir2  25918  lgssq  25925  lgsmulsqcoprm  25931  lgsdirnn0  25932  gausslemma2dlem3  25956  lgsquadlem1  25968  lgsquadlem2  25969  lgsquad2  25974  2lgslem1a2  25978  2lgsoddprmlem1  25996  2lgsoddprmlem2  25997  2sqlem2  26006  2sqlem7  26012  rplogsumlem2  26073  axlowdimlem13  26752  wlk1walk  27432  clwwisshclwwslemlem  27802  ipasslem5  28622  rearchi  30970  pdivsq  33095  dvdspw  33096  knoppndvlem9  33973  poimirlem19  35075  itg2addnclem2  35108  gcdaddmzz2nncomi  39282  metakunt16  39362  dvdsexpim  39486  zexpgcd  39490  zrtelqelz  39497  zrtdvds  39498  dffltz  39612  lzenom  39708  rexzrexnn0  39742  pell1234qrne0  39791  pell1234qrreccl  39792  pell1234qrmulcl  39793  pell1234qrdich  39799  pell14qrdich  39807  reglogexp  39832  reglogexpbas  39835  rmxm1  39872  rmym1  39873  rmxdbl  39877  rmydbl  39878  jm2.24  39901  congtr  39903  congadd  39904  congmul  39905  congsym  39906  congneg  39907  congid  39909  congabseq  39912  acongsym  39914  acongneg2  39915  acongtr  39916  acongrep  39918  jm2.19lem3  39929  jm2.19lem4  39930  jm2.19  39931  jm2.25  39937  jm2.26a  39938  oddfl  41905  coskpi2  42505  cosknegpi  42508  dvdsn1add  42578  itgsinexp  42594  fourierdlem42  42788  fourierdlem97  42842  fourierswlem  42869  2elfz2melfz  43872  sfprmdvdsmersenne  44118  proththd  44129  dfodd6  44152  dfeven4  44153  evenm1odd  44154  evenp1odd  44155  enege  44160  onego  44161  dfeven2  44164  bits0ALTV  44194  opoeALTV  44198  opeoALTV  44199  evensumeven  44222  fppr2odd  44246  sbgoldbwt  44292  nnsum3primesgbe  44307  0nodd  44427  2nodd  44429  1neven  44553  2zlidl  44555  2zrngamgm  44560  2zrngasgrp  44561  2zrngagrp  44564  2zrngmmgm  44567  2zrngmsgrp  44568  2zrngnmrid  44571  zlmodzxzsub  44759  flsubz  44928  mod0mul  44930  m1modmmod  44932  zofldiv2  44942  dignn0flhalflem1  45026  dignn0flhalflem2  45027
  Copyright terms: Public domain W3C validator