Theorem zcn 12620

Description: An integer is a complex number. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
zcn	⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

Proof of Theorem zcn

Step	Hyp	Ref	Expression
1		zre 12619	. 2 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
2	1	recnd 11290	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11154  ℤcz 12615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-resscn 11213

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-iota 6513  df-fv 6568  df-ov 7435  df-neg 11496  df-z 12616

This theorem is referenced by:  zsscn  12623  zsubcl  12661  zrevaddcl  12664  nzadd  12667  zlem1lt  12671  zltlem1  12672  zdiv  12690  zdivadd  12691  zdivmul  12692  zextlt  12694  zneo  12703  zeo2  12707  peano5uzi  12709  zindd  12721  znnn0nn  12731  zriotaneg  12733  zmax  12988  rebtwnz  12990  qmulz  12994  zq  12997  qaddcl  13008  qnegcl  13009  qmulcl  13010  qreccl  13012  fzen  13582  uzsubsubfz  13587  fz01en  13593  fzmmmeqm  13598  fzsubel  13601  fztp  13621  fzsuc2  13623  fzrev2  13629  fzrev3  13631  elfzp1b  13642  fzrevral  13653  fzrevral2  13654  fzrevral3  13655  fzshftral  13656  fzo0addel  13758  fzo0addelr  13759  fzoaddel2  13760  fzosubel2  13765  eluzgtdifelfzo  13767  fzocatel  13769  elfzom1elp1fzo  13772  fzval3  13774  zpnn0elfzo1  13779  fzosplitprm1  13817  fzoshftral  13824  flzadd  13867  2tnp1ge0ge0  13870  ceilid  13892  quoremz  13896  intfracq  13900  mulmod0  13918  zmod10  13928  modcyc  13947  modcyc2  13948  muladdmodid  13952  mulp1mod1  13953  modmuladdnn0  13957  modmul1  13966  modmulmodr  13979  modaddmulmod  13980  uzrdgxfr  14009  fzen2  14011  seqshft2  14070  sermono  14076  m1expeven  14151  expsub  14152  zesq  14266  modexp  14278  sqoddm1div8  14283  bccmpl  14349  swrd00  14683  addlenrevpfx  14729  swrdswrd  14744  swrdpfx  14746  pfxccatin12lem4  14765  pfxccatin12lem1  14767  swrdccatin2  14768  pfxccatin12lem2  14770  pfxccatin12  14772  repswrevw  14826  cshwsublen  14835  cshwidxmodr  14843  cshwidx0mod  14844  2cshw  14852  2cshwid  14853  2cshwcom  14855  cshweqdif2  14858  cshweqrep  14860  cshw1  14861  2cshwcshw  14865  shftuz  15109  seqshft  15125  nn0abscl  15352  nnabscl  15365  climshftlem  15611  climshft  15613  isershft  15701  mptfzshft  15815  fsumrev  15816  fsum0diag2  15820  efexp  16138  efzval  16139  demoivre  16237  sqrt2irr  16286  dvdsval2  16294  iddvds  16308  1dvds  16309  dvds0  16310  negdvdsb  16311  dvdsnegb  16312  0dvds  16315  dvdsmul1  16316  iddvdsexp  16318  muldvds1  16319  muldvds2  16320  dvdscmul  16321  dvdsmulc  16322  dvdscmulr  16323  dvdsmulcr  16324  summodnegmod  16325  modmulconst  16326  dvds2ln  16327  dvds2add  16328  dvds2sub  16329  dvdstr  16332  dvdssub2  16339  dvdsadd  16340  dvdsaddr  16341  dvdssub  16342  dvdssubr  16343  dvdsadd2b  16344  dvdsaddre2b  16345  dvdsabseq  16351  divconjdvds  16353  alzdvds  16358  addmodlteqALT  16363  dvdsexp2im  16365  odd2np1lem  16378  odd2np1  16379  even2n  16380  oddp1even  16382  mod2eq1n2dvds  16385  mulsucdiv2z  16391  zob  16397  ltoddhalfle  16399  halfleoddlt  16400  opoe  16401  omoe  16402  opeo  16403  omeo  16404  m1exp1  16414  divalglem0  16431  divalglem2  16433  divalglem4  16434  divalglem5  16435  divalglem9  16439  divalgb  16442  divalgmod  16444  modremain  16446  ndvdssub  16447  ndvdsadd  16448  flodddiv4  16453  flodddiv4t2lthalf  16456  bits0  16466  bitsp1e  16470  bitsp1o  16471  gcdneg  16560  gcdaddmlem  16562  gcdaddm  16563  gcdadd  16564  gcdid  16565  modgcd  16570  gcdmultiplez  16573  bezoutlem1  16577  bezoutlem2  16578  bezoutlem4  16580  dvdsgcd  16582  mulgcd  16586  absmulgcd  16587  mulgcdr  16588  gcddiv  16589  dvdssqim  16592  dvdsexpim  16593  zexpgcd  16603  dvdssq  16605  bezoutr1  16607  lcmcllem  16634  lcmneg  16641  lcmgcdlem  16644  lcmgcd  16645  lcmid  16647  lcm1  16648  coprmdvds  16691  coprmdvds2  16692  qredeq  16695  qredeu  16696  divgcdcoprmex  16704  cncongr1  16705  cncongr2  16706  prmdvdsexp  16753  rpexp1i  16761  divnumden  16786  zsqrtelqelz  16796  phiprmpw  16814  vfermltlALT  16841  nnnn0modprm0  16845  modprmn0modprm0  16846  coprimeprodsq2  16848  iserodd  16874  pclem  16877  pcprendvds2  16880  pcpremul  16882  pcmul  16890  pcneg  16913  fldivp1  16936  prmpwdvds  16943  zgz  16972  modxai  17107  mod2xnegi  17110  mulgfval  19088  mulgz  19121  mulgassr  19131  mulgmodid  19132  odmod  19565  odf1  19581  odf1o1  19591  gexdvds  19603  zaddablx  19891  ablfacrp  20087  pgpfac1lem3  20098  ablsimpgfindlem1  20128  zsubrg  21439  zsssubrg  21444  zringsub  21467  zringmulg  21468  zringinvg  21477  zringunit  21478  zringcyg  21481  prmirred  21486  mulgrhm2  21490  pzriprnglem6  21498  pzriprnglem8  21500  pzriprnglem10  21502  pzriprnglem12  21504  fermltlchr  21545  znunit  21583  degltp1le  26113  ef2kpi  26521  efper  26522  sinperlem  26523  sin2kpi  26526  cos2kpi  26527  abssinper  26564  sinkpi  26565  coskpi  26566  eflogeq  26645  cxpexpz  26710  root1eq1  26799  cxpeq  26801  zrtelqelz  26802  zrtdvds  26803  relogbexp  26824  sgmval2  27187  ppiprm  27195  ppinprm  27196  chtprm  27197  chtnprm  27198  lgslem3  27344  lgsneg  27366  lgsdir2lem2  27371  lgsdir2lem4  27373  lgsdir2  27375  lgssq  27382  lgsmulsqcoprm  27388  lgsdirnn0  27389  gausslemma2dlem3  27413  lgsquadlem1  27425  lgsquadlem2  27426  lgsquad2  27431  2lgslem1a2  27435  2lgsoddprmlem1  27453  2lgsoddprmlem2  27454  2sqlem2  27463  2sqlem7  27469  rplogsumlem2  27530  axlowdimlem13  28970  wlk1walk  29658  clwwisshclwwslemlem  30033  ipasslem5  30855  rearchi  33375  znfermltl  33395  knoppndvlem9  36522  poimirlem19  37647  itg2addnclem2  37680  gcdaddmzz2nncomi  41997  metakunt16  42222  zdivgd  42377  ef11d  42380  cxp112d  42382  cxp111d  42383  cxpi11d  42384  dffltz  42649  lzenom  42786  rexzrexnn0  42820  pell1234qrne0  42869  pell1234qrreccl  42870  pell1234qrmulcl  42871  pell1234qrdich  42877  pell14qrdich  42885  reglogexp  42910  reglogexpbas  42913  rmxm1  42951  rmym1  42952  rmxdbl  42956  rmydbl  42957  jm2.24  42980  congtr  42982  congadd  42983  congmul  42984  congsym  42985  congneg  42986  congid  42988  congabseq  42991  acongsym  42993  acongneg2  42994  acongtr  42995  acongrep  42997  jm2.19lem3  43008  jm2.19lem4  43009  jm2.19  43010  jm2.25  43016  jm2.26a  43017  oddfl  45294  coskpi2  45886  cosknegpi  45889  dvdsn1add  45959  itgsinexp  45975  fourierdlem42  46169  fourierdlem97  46223  fourierswlem  46250  2elfz2melfz  47335  submodaddmod  47348  submodneaddmod  47358  sfprmdvdsmersenne  47595  proththd  47606  dfodd6  47629  dfeven4  47630  evenm1odd  47631  evenp1odd  47632  enege  47637  onego  47638  dfeven2  47641  bits0ALTV  47671  opoeALTV  47675  opeoALTV  47676  evensumeven  47699  fppr2odd  47723  sbgoldbwt  47769  nnsum3primesgbe  47784  gpgedgvtx0  48024  gpg5nbgrvtx03starlem2  48030  gpg5nbgrvtx13starlem2  48033  0nodd  48091  2nodd  48093  1neven  48159  2zlidl  48161  2zrngamgm  48166  2zrngasgrp  48167  2zrngagrp  48170  2zrngmmgm  48173  2zrngmsgrp  48174  2zrngnmrid  48177  zlmodzxzsub  48281  flsubz  48444  mod0mul  48445  m1modmmod  48447  zofldiv2  48457  dignn0flhalflem1  48541  dignn0flhalflem2  48542