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

Theorem zcn 11668
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 11667 . 2 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
21recnd 10363 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  cc 10229  cz 11663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-resscn 10288
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-iota 6074  df-fv 6119  df-ov 6887  df-neg 10564  df-z 11664
This theorem is referenced by:  zsscn  11671  zsubcl  11705  zrevaddcl  11708  nzadd  11711  zlem1lt  11715  zltlem1  11716  zdiv  11733  zdivadd  11734  zdivmul  11735  zextlt  11737  zneo  11746  zeo2  11750  peano5uzi  11752  zindd  11764  znnn0nn  11775  zriotaneg  11777  zmax  12024  rebtwnz  12026  qmulz  12030  zq  12033  qaddcl  12043  qnegcl  12044  qmulcl  12045  qreccl  12047  fzen  12601  uzsubsubfz  12606  fz01en  12612  fzmmmeqm  12617  fzsubel  12620  fztp  12640  fzsuc2  12641  fzrev2  12647  fzrev3  12649  elfzp1b  12660  fzrevral  12668  fzrevral2  12669  fzrevral3  12670  fzshftral  12671  fzo0addel  12766  fzo0addelr  12767  fzoaddel2  12768  elfzoext  12769  fzosubel2  12772  eluzgtdifelfzo  12774  fzocatel  12776  elfzom1elp1fzo  12779  fzval3  12781  zpnn0elfzo1  12786  fzosplitprm1  12822  fzoshftral  12829  flzadd  12871  2tnp1ge0ge0  12874  ceilid  12894  quoremz  12898  intfracq  12902  mulmod0  12920  zmod10  12930  modcyc  12949  modcyc2  12950  muladdmodid  12954  mulp1mod1  12955  modmuladdnn0  12958  modmul1  12967  modmulmodr  12980  modaddmulmod  12981  uzrdgxfr  13010  fzen2  13012  seqshft2  13070  sermono  13076  m1expeven  13150  expsub  13151  zesq  13230  modexp  13242  sqoddm1div8  13271  bccmpl  13336  swrd00  13661  addlenrevswrd  13681  swrdswrd  13704  swrdswrd0  13706  swrdccatin12lem1  13728  swrdccatin12lem2b  13730  swrdccatin2  13731  swrdccatin12lem2  13733  swrdccatin12  13735  repswrevw  13777  cshwsublen  13786  cshwidxmodr  13794  cshwidx0mod  13795  2cshw  13803  2cshwid  13804  2cshwcom  13806  cshweqdif2  13809  cshweqrep  13811  cshw1  13812  2cshwcshw  13815  shftuz  14052  seqshft  14068  nn0abscl  14295  nnabscl  14308  climshftlem  14548  climshft  14550  isershft  14637  mptfzshft  14752  fsumrev  14753  fsum0diag2  14757  efexp  15071  efzval  15072  demoivre  15170  znnenlemOLD  15180  sqrt2irr  15219  dvdsval2  15226  iddvds  15238  1dvds  15239  dvds0  15240  negdvdsb  15241  dvdsnegb  15242  0dvds  15245  dvdsmul1  15246  iddvdsexp  15248  muldvds1  15249  muldvds2  15250  dvdscmul  15251  dvdsmulc  15252  dvdscmulr  15253  dvdsmulcr  15254  summodnegmod  15255  modmulconst  15256  dvds2ln  15257  dvds2add  15258  dvds2sub  15259  dvdstr  15261  dvdssub2  15266  dvdsadd  15267  dvdsaddr  15268  dvdssub  15269  dvdssubr  15270  dvdsadd2b  15271  dvdsaddre2b  15272  dvdsabseq  15278  divconjdvds  15280  alzdvds  15285  addmodlteqALT  15290  odd2np1lem  15304  odd2np1  15305  even2n  15306  oddp1even  15308  mod2eq1n2dvds  15311  mulsucdiv2z  15317  zob  15323  ltoddhalfle  15325  halfleoddlt  15326  opoe  15327  omoe  15328  opeo  15329  omeo  15330  m1exp1  15333  divalglem0  15356  divalglem2  15358  divalglem4  15359  divalglem5  15360  divalglem9  15364  divalgb  15367  divalgmod  15369  modremain  15371  ndvdssub  15372  ndvdsadd  15373  flodddiv4  15376  flodddiv4t2lthalf  15379  bits0  15389  bitsp1e  15393  bitsp1o  15394  gcdneg  15482  gcdaddmlem  15484  gcdaddm  15485  gcdadd  15486  gcdid  15487  modgcd  15492  bezoutlem1  15495  bezoutlem2  15496  bezoutlem4  15498  dvdsgcd  15500  mulgcd  15504  absmulgcd  15505  mulgcdr  15506  gcddiv  15507  gcdmultiplez  15509  dvdssqim  15512  dvdssq  15519  bezoutr1  15521  lcmcllem  15548  lcmneg  15555  lcmgcdlem  15558  lcmgcd  15559  lcmid  15561  lcm1  15562  coprmdvds  15605  coprmdvds2  15606  qredeq  15609  qredeu  15610  divgcdcoprmex  15618  cncongr1  15619  cncongr2  15620  prmdvdsexp  15664  rpexp1i  15670  divnumden  15693  zsqrtelqelz  15703  phiprmpw  15718  vfermltlALT  15744  nnnn0modprm0  15748  modprmn0modprm0  15749  coprimeprodsq2  15751  iserodd  15777  pclem  15780  pcprendvds2  15783  pcpremul  15785  pcmul  15793  pcneg  15815  fldivp1  15838  prmpwdvds  15845  zgz  15874  modxai  16009  mod2xnegi  16012  mulgz  17792  mulgassr  17802  mulgmodid  17803  odmod  18186  odf1  18200  odf1o1  18208  gexdvds  18220  zaddablx  18496  cygabl  18513  ablfacrp  18687  pgpfac1lem3  18698  zsubrg  20027  zsssubrg  20032  zringmulg  20054  zringinvg  20063  zringunit  20064  zringcyg  20067  prmirred  20071  mulgrhm2  20075  znunit  20139  degltp1le  24070  ef2kpi  24468  efper  24469  sinperlem  24470  sin2kpi  24473  cos2kpi  24474  abssinper  24508  sinkpi  24509  coskpi  24510  eflogeq  24585  cxpexpz  24650  root1eq1  24733  cxpeq  24735  relogbexp  24755  leibpilem1  24904  sgmval2  25106  ppiprm  25114  ppinprm  25115  chtprm  25116  chtnprm  25117  lgslem3  25261  lgsneg  25283  lgsdir2lem2  25288  lgsdir2lem4  25290  lgsdir2  25292  lgssq  25299  lgsmulsqcoprm  25305  lgsdirnn0  25306  gausslemma2dlem3  25330  lgsquadlem1  25342  lgsquadlem2  25343  lgsquad2  25348  2lgslem1a2  25352  2lgsoddprmlem1  25370  2lgsoddprmlem2  25371  2sqlem2  25380  2sqlem7  25386  rplogsumlem2  25411  axlowdimlem13  26071  wlk1walk  26786  clwwisshclwwslemlem  27179  ipasslem5  28041  rearchi  30190  pdivsq  31979  dvdspw  31980  knoppndvlem9  32850  poimirlem19  33760  itg2addnclem2  33793  lzenom  37853  rexzrexnn0  37888  pell1234qrne0  37937  pell1234qrreccl  37938  pell1234qrmulcl  37939  pell1234qrdich  37945  pell14qrdich  37953  reglogexp  37978  reglogexpbas  37981  rmxm1  38018  rmym1  38019  rmxdbl  38023  rmydbl  38024  jm2.24  38049  congtr  38051  congadd  38052  congmul  38053  congsym  38054  congneg  38055  congid  38057  congabseq  38060  acongsym  38062  acongneg2  38063  acongtr  38064  acongrep  38066  jm2.19lem3  38077  jm2.19lem4  38078  jm2.19  38079  jm2.25  38085  jm2.26a  38086  oddfl  39989  coskpi2  40575  cosknegpi  40578  dvdsn1add  40652  itgsinexp  40668  fourierdlem42  40863  fourierdlem97  40917  fourierswlem  40944  2elfz2melfz  41921  addlenrevpfx  41990  pfxccatin12lem1  42016  pfxccatin12lem2  42017  pfxccatin12  42018  sfprmdvdsmersenne  42113  proththd  42124  dfodd6  42143  dfeven4  42144  evenm1odd  42145  evenp1odd  42146  enege  42151  onego  42152  dfeven2  42155  bits0ALTV  42183  opoeALTV  42187  opeoALTV  42188  evensumeven  42209  sbgoldbwt  42258  nnsum3primesgbe  42273  0nodd  42396  2nodd  42398  1neven  42518  2zlidl  42520  2zrngamgm  42525  2zrngasgrp  42526  2zrngagrp  42529  2zrngmmgm  42532  2zrngmsgrp  42533  2zrngnmrid  42536  zlmodzxzsub  42724  flsubz  42898  mod0mul  42900  m1modmmod  42902  zofldiv2  42911  dignn0flhalflem1  42995  dignn0flhalflem2  42996
  Copyright terms: Public domain W3C validator