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

Theorem zcn 10325
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 10324 . 2 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
21recnd 9152 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1728  cc 9026  cz 10320
This theorem is referenced by:  zsscn  10328  zsubcl  10357  zrevaddcl  10359  zlem1lt  10365  zltlem1  10366  zdiv  10378  zdivadd  10379  zdivmul  10380  zextlt  10382  zneo  10390  zeo2  10394  peano5uzi  10396  uzindOLD  10402  zindd  10409  zmax  10609  rebtwnz  10611  qmulz  10615  zq  10618  qaddcl  10628  qnegcl  10629  qmulcl  10630  qreccl  10632  fzen  11110  fz01en  11117  fzsubel  11126  fztp  11140  fzsuc2  11142  fzrev2  11147  fzrev3  11149  fzrevral  11169  fzrevral2  11170  fzrevral3  11171  fzshftral  11172  fzoaddel2  11214  fzosubel2  11216  fzval3  11218  flzadd  11266  quoremz  11274  intfracq  11278  zmod10  11302  modcyc  11314  modcyc2  11315  modmul1  11317  uzrdgxfr  11344  fzen2  11346  seqshft2  11387  sermono  11393  expsub  11465  zesq  11540  modexp  11552  bccmpl  11638  swrd00  11803  shftuz  11922  seqshft  11938  nn0abscl  12155  nnabscl  12167  climshftlem  12406  climshft  12408  isershft  12495  fsumrev  12600  fsumshft  12601  fsum0diag2  12604  efexp  12740  efzval  12741  demoivre  12839  znnenlem  12849  sqr2irr  12886  dvdsval2  12893  iddvds  12901  1dvds  12902  dvds0  12903  negdvdsb  12904  dvdsnegb  12905  0dvds  12908  dvdsmul1  12909  iddvdsexp  12911  muldvds1  12912  muldvds2  12913  dvdscmul  12914  dvdsmulc  12915  dvdscmulr  12916  dvdsmulcr  12917  dvds2ln  12918  dvds2add  12919  dvds2sub  12920  dvdstr  12921  dvdssub2  12925  dvdsadd  12926  dvdsaddr  12927  dvdssub  12928  dvdssubr  12929  dvdsadd2b  12930  alzdvds  12937  odd2np1lem  12945  odd2np1  12946  oddp1even  12948  divalglem0  12951  divalglem2  12953  divalglem4  12954  divalglem5  12955  divalglem9  12959  divalgb  12962  divalgmod  12964  ndvdssub  12965  ndvdsadd  12966  bits0  12978  bitsp1e  12982  bitsp1o  12983  gcdneg  13064  gcdaddmlem  13066  gcdaddm  13067  gcdadd  13068  gcdid  13069  modgcd  13074  bezoutlem1  13076  bezoutlem2  13077  bezoutlem4  13079  dvdsgcd  13081  mulgcd  13084  absmulgcd  13085  mulgcdr  13086  gcddiv  13087  gcdmultiplez  13089  dvdssqim  13091  dvdssq  13098  coprmdvds  13140  coprmdvds2  13141  qredeq  13144  qredeu  13145  prmdvdsexp  13152  rpexp1i  13159  divnumden  13178  zsqrelqelz  13188  phiprmpw  13203  coprimeprodsq2  13222  opoe  13223  omoe  13224  opeo  13225  omeo  13226  iserodd  13247  pclem  13250  pcprendvds2  13253  pcpremul  13255  pcmul  13263  pcneg  13285  fldivp1  13304  prmpwdvds  13310  zgz  13339  modxai  13442  mod2xnegi  13445  mulgz  14949  odmod  15222  odf1  15236  odf1o1  15244  gexdvds  15256  zaddablx  15521  cygabl  15538  ablfacrp  15662  pgpfac1lem3  15673  zsubrg  16790  zsssubrg  16795  zrngunit  16803  zcyg  16810  prmirred  16813  mulgrhm2  16826  znunit  16882  degltp1le  20034  ef2kpi  20424  efper  20425  sinperlem  20426  sin2kpi  20429  cos2kpi  20430  abssinper  20464  sinkpi  20465  coskpi  20466  eflogeq  20534  cxpexpz  20596  root1eq1  20677  cxpeq  20679  leibpilem1  20818  sgmval2  20964  ppiprm  20972  ppinprm  20973  chtprm  20974  chtnprm  20975  lgslem3  21120  lgsneg  21141  lgsdir2lem2  21146  lgsdir2lem4  21148  lgsdir2  21150  lgsdirnn0  21161  lgsquadlem1  21176  lgsquadlem2  21177  lgsquad2  21182  2sqlem2  21186  2sqlem7  21192  rplogsumlem2  21217  wlkdvspthlem  21645  gxneg  21892  gxsuc  21898  gxnn0add  21900  gxadd  21901  gxsub  21902  gxnn0mul  21903  gxmul  21904  zaddsubgo  21980  ipasslem5  22374  zzsmulg  24300  m1expevenALT  24940  elfzp1b  25151  pdivsq  25403  dvdspw  25404  axlowdimlem13  25928  itg2addnclem2  26299  lzenom  26940  rexzrexnn0  26976  pell1234qrne0  27028  pell1234qrreccl  27029  pell1234qrmulcl  27030  pell1234qrdich  27036  pell14qrdich  27044  reglogexp  27069  reglogexpbas  27072  rmxm1  27109  rmym1  27110  rmxdbl  27114  rmydbl  27115  jm2.24  27140  congtr  27142  congadd  27143  congmul  27144  congsym  27145  congneg  27146  congid  27148  congabseq  27151  acongsym  27153  acongneg2  27154  acongtr  27155  acongrep  27157  bezoutr1  27163  dvdsabsmod0  27169  jm2.19lem3  27174  jm2.19lem4  27175  jm2.19  27176  jm2.25  27182  jm2.26a  27183  itgsinexp  27837  fzmmmeqm  28236  2elfz2melfz  28238  ubmelfzo  28247  ubmelm1fzo  28248  modaddmulmod  28279  addlenrevswrd  28317  swrd0swrd  28329  swrdswrd  28331  swrd0swrdid  28332  swrdswrd0  28333  swrdccatin12lem2  28339  swrdccatin12lem3b  28341  swrdccatin2  28342  swrdccatin12lem3  28344  swrdccatin12  28346  2cshw1lem1  28380  2cshw2lem1  28384  cshweqdif2  28402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-resscn 9085
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rex 2718  df-rab 2721  df-v 2967  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3768  df-sn 3849  df-pr 3850  df-op 3852  df-uni 4045  df-br 4244  df-iota 5453  df-fv 5497  df-ov 6120  df-neg 9332  df-z 10321
  Copyright terms: Public domain W3C validator