Theorem zcn 11987

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 10535  ℤcz 11982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-resscn 10594

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159  df-neg 10873  df-z 11983

This theorem is referenced by:  zsscn  11990  zsubcl  12025  zrevaddcl  12028  nzadd  12031  zlem1lt  12035  zltlem1  12036  zdiv  12053  zdivadd  12054  zdivmul  12055  zextlt  12057  zneo  12066  zeo2  12070  peano5uzi  12072  zindd  12084  znnn0nn  12095  zriotaneg  12097  zmax  12346  rebtwnz  12348  qmulz  12352  zq  12355  qaddcl  12365  qnegcl  12366  qmulcl  12367  qreccl  12369  fzen  12925  uzsubsubfz  12930  fz01en  12936  fzmmmeqm  12941  fzsubel  12944  fztp  12964  fzsuc2  12966  fzrev2  12972  fzrev3  12974  elfzp1b  12985  fzrevral  12993  fzrevral2  12994  fzrevral3  12995  fzshftral  12996  fzo0addel  13092  fzo0addelr  13093  fzoaddel2  13094  elfzoext  13095  fzosubel2  13098  eluzgtdifelfzo  13100  fzocatel  13102  elfzom1elp1fzo  13105  fzval3  13107  zpnn0elfzo1  13112  fzosplitprm1  13148  fzoshftral  13155  flzadd  13197  2tnp1ge0ge0  13200  ceilid  13220  quoremz  13224  intfracq  13228  mulmod0  13246  zmod10  13256  modcyc  13275  modcyc2  13276  muladdmodid  13280  mulp1mod1  13281  modmuladdnn0  13284  modmul1  13293  modmulmodr  13306  modaddmulmod  13307  uzrdgxfr  13336  fzen2  13338  seqshft2  13397  sermono  13403  m1expeven  13477  expsub  13478  zesq  13588  modexp  13600  sqoddm1div8  13605  bccmpl  13670  swrd00  14006  addlenrevpfx  14052  swrdswrd  14067  swrdpfx  14069  pfxccatin12lem4  14088  pfxccatin12lem1  14090  swrdccatin2  14091  pfxccatin12lem2  14093  pfxccatin12  14095  repswrevw  14149  cshwsublen  14158  cshwidxmodr  14166  cshwidx0mod  14167  2cshw  14175  2cshwid  14176  2cshwcom  14178  cshweqdif2  14181  cshweqrep  14183  cshw1  14184  2cshwcshw  14187  shftuz  14428  seqshft  14444  nn0abscl  14672  nnabscl  14685  climshftlem  14931  climshft  14933  isershft  15020  mptfzshft  15133  fsumrev  15134  fsum0diag2  15138  efexp  15454  efzval  15455  demoivre  15553  sqrt2irr  15602  dvdsval2  15610  iddvds  15623  1dvds  15624  dvds0  15625  negdvdsb  15626  dvdsnegb  15627  0dvds  15630  dvdsmul1  15631  iddvdsexp  15633  muldvds1  15634  muldvds2  15635  dvdscmul  15636  dvdsmulc  15637  dvdscmulr  15638  dvdsmulcr  15639  summodnegmod  15640  modmulconst  15641  dvds2ln  15642  dvds2add  15643  dvds2sub  15644  dvdstr  15646  dvdssub2  15651  dvdsadd  15652  dvdsaddr  15653  dvdssub  15654  dvdssubr  15655  dvdsadd2b  15656  dvdsaddre2b  15657  dvdsabseq  15663  divconjdvds  15665  alzdvds  15670  addmodlteqALT  15675  odd2np1lem  15689  odd2np1  15690  even2n  15691  oddp1even  15693  mod2eq1n2dvds  15696  mulsucdiv2z  15702  zob  15708  ltoddhalfle  15710  halfleoddlt  15711  opoe  15712  omoe  15713  opeo  15714  omeo  15715  m1exp1  15727  divalglem0  15744  divalglem2  15746  divalglem4  15747  divalglem5  15748  divalglem9  15752  divalgb  15755  divalgmod  15757  modremain  15759  ndvdssub  15760  ndvdsadd  15761  flodddiv4  15764  flodddiv4t2lthalf  15767  bits0  15777  bitsp1e  15781  bitsp1o  15782  gcdneg  15870  gcdaddmlem  15872  gcdaddm  15873  gcdadd  15874  gcdid  15875  modgcd  15880  gcdmultiplez  15883  bezoutlem1  15887  bezoutlem2  15888  bezoutlem4  15890  dvdsgcd  15892  mulgcd  15896  absmulgcd  15897  mulgcdr  15898  gcddiv  15899  gcdmultiplezOLD  15901  dvdssqim  15904  dvdssq  15911  bezoutr1  15913  lcmcllem  15940  lcmneg  15947  lcmgcdlem  15950  lcmgcd  15951  lcmid  15953  lcm1  15954  coprmdvds  15997  coprmdvds2  15998  qredeq  16001  qredeu  16002  divgcdcoprmex  16010  cncongr1  16011  cncongr2  16012  prmdvdsexp  16059  rpexp1i  16065  divnumden  16088  zsqrtelqelz  16098  phiprmpw  16113  vfermltlALT  16139  nnnn0modprm0  16143  modprmn0modprm0  16144  coprimeprodsq2  16146  iserodd  16172  pclem  16175  pcprendvds2  16178  pcpremul  16180  pcmul  16188  pcneg  16210  fldivp1  16233  prmpwdvds  16240  zgz  16269  modxai  16404  mod2xnegi  16407  mulgfval  18226  mulgz  18255  mulgassr  18265  mulgmodid  18266  odmod  18674  odf1  18689  odf1o1  18697  gexdvds  18709  zaddablx  18992  cygablOLD  19011  ablfacrp  19188  pgpfac1lem3  19199  ablsimpgfindlem1  19229  zsubrg  20598  zsssubrg  20603  zringmulg  20625  zringinvg  20634  zringunit  20635  zringcyg  20638  prmirred  20642  mulgrhm2  20646  znunit  20710  degltp1le  24667  ef2kpi  25064  efper  25065  sinperlem  25066  sin2kpi  25069  cos2kpi  25070  abssinper  25106  sinkpi  25107  coskpi  25108  eflogeq  25185  cxpexpz  25250  root1eq1  25336  cxpeq  25338  relogbexp  25358  sgmval2  25720  ppiprm  25728  ppinprm  25729  chtprm  25730  chtnprm  25731  lgslem3  25875  lgsneg  25897  lgsdir2lem2  25902  lgsdir2lem4  25904  lgsdir2  25906  lgssq  25913  lgsmulsqcoprm  25919  lgsdirnn0  25920  gausslemma2dlem3  25944  lgsquadlem1  25956  lgsquadlem2  25957  lgsquad2  25962  2lgslem1a2  25966  2lgsoddprmlem1  25984  2lgsoddprmlem2  25985  2sqlem2  25994  2sqlem7  26000  rplogsumlem2  26061  axlowdimlem13  26740  wlk1walk  27420  clwwisshclwwslemlem  27791  ipasslem5  28612  rearchi  30915  pdivsq  32981  dvdspw  32982  knoppndvlem9  33859  poimirlem19  34926  itg2addnclem2  34959  dvdsexpim  39201  zexpgcd  39205  zrtelqelz  39212  zrtdvds  39213  dffltz  39291  lzenom  39387  rexzrexnn0  39421  pell1234qrne0  39470  pell1234qrreccl  39471  pell1234qrmulcl  39472  pell1234qrdich  39478  pell14qrdich  39486  reglogexp  39511  reglogexpbas  39514  rmxm1  39551  rmym1  39552  rmxdbl  39556  rmydbl  39557  jm2.24  39580  congtr  39582  congadd  39583  congmul  39584  congsym  39585  congneg  39586  congid  39588  congabseq  39591  acongsym  39593  acongneg2  39594  acongtr  39595  acongrep  39597  jm2.19lem3  39608  jm2.19lem4  39609  jm2.19  39610  jm2.25  39616  jm2.26a  39617  oddfl  41563  coskpi2  42167  cosknegpi  42170  dvdsn1add  42244  itgsinexp  42260  fourierdlem42  42454  fourierdlem97  42508  fourierswlem  42535  2elfz2melfz  43538  sfprmdvdsmersenne  43788  proththd  43799  dfodd6  43822  dfeven4  43823  evenm1odd  43824  evenp1odd  43825  enege  43830  onego  43831  dfeven2  43834  bits0ALTV  43864  opoeALTV  43868  opeoALTV  43869  evensumeven  43892  fppr2odd  43916  sbgoldbwt  43962  nnsum3primesgbe  43977  0nodd  44097  2nodd  44099  1neven  44223  2zlidl  44225  2zrngamgm  44230  2zrngasgrp  44231  2zrngagrp  44234  2zrngmmgm  44237  2zrngmsgrp  44238  2zrngnmrid  44241  zlmodzxzsub  44428  flsubz  44597  mod0mul  44599  m1modmmod  44601  zofldiv2  44611  dignn0flhalflem1  44695  dignn0flhalflem2  44696