Theorem zcn 12738

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 12737	. 2 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
2	1	recnd 11376	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℂcc 11237  ℤcz 12733

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-resscn 11296

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-neg 11583  df-z 12734

This theorem is used by:  zsscn  12741  zsubcl  12778  zrevaddcl  12781  nzadd  12784  zlem1lt  12788  zltlem1  12789  zdiv  12809  zdivadd  12810  zdivmul  12811  zextlt  12813  zneo  12822  zeo2  12826  peano5uzi  12828  zindd  12840  znnn0nn  12850  zriotaneg  12852  zmax  13112  rebtwnz  13114  qmulz  13118  zq  13121  qaddcl  13133  qnegcl  13134  qmulcl  13135  qreccl  13137  fzen  13714  uzsubsubfz  13720  fz01en  13726  fzmmmeqm  13731  fzsubel  13734  fztp  13754  fzsuc2  13756  fzrev2  13762  fzrev3  13764  elfzp1b  13775  fzrevral  13786  fzrevral2  13787  fzrevral3  13788  fzshftral  13789  fzo0addel  13893  fzo0addelr  13894  fzoaddel2  13895  fzosubel2  13900  eluzgtdifelfzo  13902  fzocatel  13904  elfzom1elp1fzo  13907  fzval3  13909  zpnn0elfzo1  13914  fzosplitprm1  13953  fzoshftral  13962  flzadd  14006  2tnp1ge0ge0  14009  ceilid  14031  quoremz  14035  intfracq  14039  mulmod0  14057  zmod10  14067  modcyc  14086  modcyc2  14087  muladdmodid  14093  mulp1mod1  14094  modmuladdnn0  14098  modmul1  14107  modmulmodr  14120  modaddmulmod  14121  uzrdgxfr  14150  fzen2  14152  seqshft2  14211  sermono  14217  m1expeven  14292  expsub  14293  zesq  14411  modexp  14423  sqoddm1div8  14428  bccmpl  14494  swrd00  14834  swrdswrd  14896  swrdpfx  14898  pfxccatin12lem4  14917  pfxccatin12lem1  14919  swrdccatin2  14920  pfxccatin12lem2  14922  pfxccatin12  14924  repswrevw  14980  cshwsublen  14989  cshwidxmodr  14997  cshwidx0mod  14998  2cshw  15006  2cshwid  15007  2cshwcom  15009  cshweqdif2  15012  cshweqrep  15014  cshw1  15015  2cshwcshw  15018  shftuz  15265  seqshft  15281  nn0abscl  15522  zabs0b  15524  nnabscl  15536  climshftlem  15785  climshft  15787  isershft  15875  mptfzshft  15988  fsumrev  15989  fsum0diag2  15993  efexp  16313  efzval  16314  demoivre  16412  sqrt2irr  16461  dvdsval2  16469  iddvds  16483  1dvds  16484  dvds0  16485  negdvdsb  16486  dvdsnegb  16487  0dvds  16490  dvdsmul1  16491  iddvdsexp  16493  muldvds1  16494  muldvds2  16495  dvdscmul  16496  dvdsmulc  16497  dvdscmulr  16498  dvdsmulcr  16499  summodnegmod  16500  difmod0  16501  modmulconst  16502  dvds2ln  16503  dvds2add  16504  dvds2sub  16505  dvdstr  16508  dvdssub2  16515  dvdsadd  16516  dvdsaddr  16517  dvdssub  16518  dvdssubr  16519  dvdsadd2b  16520  dvdsaddre2b  16521  dvdsabseq  16527  divconjdvds  16529  alzdvds  16534  addmodlteqALT  16539  dvdsexp2im  16541  odd2np1lem  16554  odd2np1  16555  even2n  16556  oddp1even  16558  mod2eq1n2dvds  16561  mulsucdiv2z  16567  zob  16573  ltoddhalfle  16575  halfleoddlt  16576  opoe  16577  omoe  16578  opeo  16579  omeo  16580  m1exp1  16590  divalglem0  16607  divalglem2  16609  divalglem4  16610  divalglem5  16611  divalglem9  16615  divalgb  16618  divalgmod  16620  modremain  16622  ndvdssub  16623  ndvdsadd  16624  flodddiv4  16629  flodddiv4t2lthalf  16632  bits0  16642  bitsp1e  16646  bitsp1o  16647  gcdneg  16738  gcdaddmlem  16740  gcdaddm  16741  gcdadd  16742  gcdid  16743  modgcd  16749  gcdmultiplez  16752  bezoutlem1  16756  bezoutlem2  16757  bezoutlem4  16759  dvdsgcd  16761  mulgcd  16765  absmulgcd  16766  mulgcdr  16767  gcddiv  16768  dvdssqim  16771  dvdsexpim  16772  zexpgcd  16783  dvdssq  16786  bezoutr1  16788  lcmcllem  16815  lcmneg  16822  lcmgcdlem  16825  lcmgcd  16826  lcmid  16828  lcm1  16829  coprmdvds  16872  coprmdvds2  16873  qredeq  16876  qredeu  16877  divgcdcoprmex  16885  cncongr1  16886  cncongr2  16887  prmdvdsexp  16935  rpexp1i  16943  divnumden  16968  zsqrtelqelz  16978  phiprmpw  16997  vfermltlALT  17024  nnnn0modprm0  17028  modprmn0modprm0  17029  coprimeprodsq2  17031  iserodd  17057  pclem  17060  pcprendvds2  17063  pcpremul  17065  pcmul  17073  pcneg  17096  fldivp1  17119  prmpwdvds  17126  zgz  17155  modxai  17290  mod2xnegi  17293  chnccat  18850  chnrev  18851  mulgfval  19329  mulgz  19362  mulgassr  19372  mulgmodid  19373  odmod  19811  odf1  19827  odf1o1  19837  gexdvds  19849  zaddablx  20137  ablfacrp  20333  pgpfac1lem3  20344  ablsimpgfindlem1  20374  zsubrg  21780  zsssubrg  21785  zringsub  21816  zringmulg  21817  zringinvg  21826  zringunit  21827  zringcyg  21830  prmirred  21835  mulgrhm2  21839  pzriprnglem6  21847  pzriprnglem8  21849  pzriprnglem10  21851  pzriprnglem12  21853  fermltlchr  21890  znunit  21924  degltp1le  26446  ef2kpi  26864  efper  26865  sinperlem  26866  sin2kpi  26869  cos2kpi  26870  abssinper  26906  sinkpi  26907  coskpi  26908  eflogeq  26987  cxpexpz  27052  root1eq1  27140  cxpeq  27142  zrtelqelz  27143  zrtdvds  27144  relogbexp  27165  sgmval2  27527  ppiprm  27535  ppinprm  27536  chtprm  27537  chtnprm  27538  lgslem3  27683  lgsneg  27705  lgsdir2lem2  27710  lgsdir2lem4  27712  lgsdir2  27714  lgssq  27721  lgsmulsqcoprm  27727  lgsdirnn0  27728  gausslemma2dlem3  27752  lgsquadlem1  27764  lgsquadlem2  27765  lgsquad2  27770  2lgslem1a2  27774  2lgsoddprmlem1  27792  2lgsoddprmlem2  27793  2sqlem2  27802  2sqlem7  27808  rplogsumlem2  27869  axlowdimlem13  29589  wlk1walk  30276  clwwisshclwwslemlem  30661  ipasslem5  31494  rearchi  34011  znfermltl  34026  knoppndvlem9  37601  poimirlem19  38825  itg2addnclem2  38858  gcdaddmzz2nncomi  43311  zdivgd  43654  ef11d  43656  cxp112d  43658  cxp111d  43659  cxpi11d  43660  dffltz  43936  lzenom  44047  rexzrexnn0  44077  pell1234qrne0  44126  pell1234qrreccl  44127  pell1234qrmulcl  44128  pell1234qrdich  44134  pell14qrdich  44142  reglogexp  44167  reglogexpbas  44170  rmxm1  44207  rmym1  44208  rmxdbl  44212  rmydbl  44213  jm2.24  44236  congtr  44238  congadd  44239  congmul  44240  congsym  44241  congneg  44242  congid  44244  congabseq  44247  acongsym  44249  acongneg2  44250  acongtr  44251  acongrep  44253  jm2.19lem3  44264  jm2.19lem4  44265  jm2.19  44266  jm2.25  44272  jm2.26a  44273  oddfl  46567  coskpi2  47149  cosknegpi  47152  dvdsn1add  47222  itgsinexp  47238  fourierdlem42  47432  fourierdlem97  47486  fourierswlem  47513  sinnpoly  48214  2elfz2melfz  48661  ceilbi  48680  flmrecm1  48686  submodaddmod  48690  submodneaddmod  48700  mod0mul  48705  m1modmmod  48707  modmkpkne  48710  modlt0b  48712  sfprmdvdsmersenne  48961  proththd  48972  ppivalnnprm  48983  ppivalnnnprmge6  48984  dfodd6  49008  dfeven4  49009  evenm1odd  49010  evenp1odd  49011  enege  49016  onego  49017  dfeven2  49020  bits0ALTV  49050  opoeALTV  49054  opeoALTV  49055  evensumeven  49078  fppr2odd  49102  sbgoldbwt  49148  nnsum3primesgbe  49163  gpgedgvtx0  49432  gpg5nbgrvtx03starlem2  49440  gpg5nbgrvtx13starlem2  49443  0nodd  49540  2nodd  49542  1neven  49608  2zlidl  49610  2zrngamgm  49615  2zrngasgrp  49616  2zrngagrp  49619  2zrngmmgm  49622  2zrngmsgrp  49623  2zrngnmrid  49626  zellaz  49729  adcnmulzlaz  49731  lazlinz  49733  adcnlaz  49734  gzilaz  49735  laznegcl  49736  lazmulzcl  49737  lazaddcl  49738  lazmulcl  49740  lazcjcl  49741  zlmodzxzsub  49803  flsubz  49965  zofldiv2  49974  dignn0flhalflem1  50058  dignn0flhalflem2  50059