Theorem zcn 11382

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

Syntax hints:   → wi 4   ∈ wcel 1990  ℂcc 9934  ℤcz 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-neg 10269  df-z 11378

This theorem is referenced by:  zsscn  11385  zsubcl  11419  zrevaddcl  11422  nzadd  11425  zlem1lt  11429  zltlem1  11430  zdiv  11447  zdivadd  11448  zdivmul  11449  zextlt  11451  zneo  11460  zeo2  11464  peano5uzi  11466  zindd  11478  znnn0nn  11489  zriotaneg  11491  zmax  11785  rebtwnz  11787  qmulz  11791  zq  11794  qaddcl  11804  qnegcl  11805  qmulcl  11806  qreccl  11808  fzen  12358  uzsubsubfz  12363  fz01en  12369  fzmmmeqm  12374  fzsubel  12377  fztp  12397  fzsuc2  12398  fzrev2  12404  fzrev3  12406  elfzp1b  12417  fzrevral  12425  fzrevral2  12426  fzrevral3  12427  fzshftral  12428  fzo0addel  12521  fzo0addelr  12522  fzoaddel2  12523  elfzoext  12524  fzosubel2  12527  eluzgtdifelfzo  12529  fzocatel  12531  elfzom1elp1fzo  12534  fzval3  12536  zpnn0elfzo1  12541  fzosplitprm1  12578  fzoshftral  12585  flzadd  12627  2tnp1ge0ge0  12630  ceilid  12650  quoremz  12654  intfracq  12658  mulmod0  12676  zmod10  12686  modcyc  12705  modcyc2  12706  muladdmodid  12710  mulp1mod1  12711  modmuladdnn0  12714  modmul1  12723  modmulmodr  12736  modaddmulmod  12737  uzrdgxfr  12766  fzen2  12768  seqshft2  12827  sermono  12833  m1expeven  12907  expsub  12908  zesq  12987  modexp  12999  sqoddm1div8  13028  bccmpl  13096  swrd00  13418  addlenrevswrd  13437  swrdswrd  13460  swrdswrd0  13462  swrdccatin12lem1  13484  swrdccatin12lem2b  13486  swrdccatin2  13487  swrdccatin12lem2  13489  swrdccatin12  13491  repswrevw  13533  cshwsublen  13542  cshwidxmodr  13550  cshwidx0mod  13551  2cshw  13559  2cshwid  13560  2cshwcom  13562  cshweqdif2  13565  cshweqrep  13567  cshw1  13568  2cshwcshw  13571  shftuz  13809  seqshft  13825  nn0abscl  14052  nnabscl  14065  climshftlem  14305  climshft  14307  isershft  14394  mptfzshft  14510  fsumrev  14511  fsum0diag2  14515  efexp  14831  efzval  14832  demoivre  14930  znnenlem  14940  sqrt2irr  14979  dvdsval2  14986  iddvds  14995  1dvds  14996  dvds0  14997  negdvdsb  14998  dvdsnegb  14999  0dvds  15002  dvdsmul1  15003  iddvdsexp  15005  muldvds1  15006  muldvds2  15007  dvdscmul  15008  dvdsmulc  15009  dvdscmulr  15010  dvdsmulcr  15011  summodnegmod  15012  modmulconst  15013  dvds2ln  15014  dvds2add  15015  dvds2sub  15016  dvdstr  15018  dvdssub2  15023  dvdsadd  15024  dvdsaddr  15025  dvdssub  15026  dvdssubr  15027  dvdsadd2b  15028  dvdsaddre2b  15029  dvdsabseq  15035  divconjdvds  15037  alzdvds  15042  addmodlteqALT  15047  mulmoddvds  15051  odd2np1lem  15064  odd2np1  15065  even2n  15066  oddp1even  15068  mod2eq1n2dvds  15071  mulsucdiv2z  15077  zob  15083  ltoddhalfle  15085  halfleoddlt  15086  opoe  15087  omoe  15088  opeo  15089  omeo  15090  m1exp1  15093  divalglem0  15116  divalglem2  15118  divalglem4  15119  divalglem5  15120  divalglem9  15124  divalgb  15127  divalgmod  15129  divalgmodOLD  15130  modremain  15132  ndvdssub  15133  ndvdsadd  15134  flodddiv4  15137  flodddiv4t2lthalf  15140  bits0  15150  bitsp1e  15154  bitsp1o  15155  gcdneg  15243  gcdaddmlem  15245  gcdaddm  15246  gcdadd  15247  gcdid  15248  modgcd  15253  bezoutlem1  15256  bezoutlem2  15257  bezoutlem4  15259  dvdsgcd  15261  mulgcd  15265  absmulgcd  15266  mulgcdr  15267  gcddiv  15268  gcdmultiplez  15270  dvdssqim  15273  dvdssq  15280  bezoutr1  15282  lcmcllem  15309  lcmneg  15316  lcmgcdlem  15319  lcmgcd  15320  lcmid  15322  lcm1  15323  coprmdvds  15366  coprmdvdsOLD  15367  coprmdvds2  15368  qredeq  15371  qredeu  15372  divgcdcoprmex  15380  cncongr1  15381  cncongr2  15382  prmdvdsexp  15427  rpexp1i  15433  divnumden  15456  zsqrtelqelz  15466  phiprmpw  15481  vfermltlALT  15507  nnnn0modprm0  15511  modprmn0modprm0  15512  coprimeprodsq2  15514  iserodd  15540  pclem  15543  pcprendvds2  15546  pcpremul  15548  pcmul  15556  pcneg  15578  fldivp1  15601  prmpwdvds  15608  zgz  15637  modxai  15772  mod2xnegi  15775  mulgz  17568  mulgassr  17580  mulgmodid  17581  odmod  17965  odf1  17979  odf1o1  17987  gexdvds  17999  zaddablx  18275  cygabl  18292  ablfacrp  18465  pgpfac1lem3  18476  zsubrg  19799  zsssubrg  19804  zringmulg  19826  zringinvg  19835  zringunit  19836  zringcyg  19839  prmirred  19843  mulgrhm2  19847  znunit  19912  degltp1le  23833  ef2kpi  24230  efper  24231  sinperlem  24232  sin2kpi  24235  cos2kpi  24236  abssinper  24270  sinkpi  24271  coskpi  24272  eflogeq  24348  cxpexpz  24413  root1eq1  24496  cxpeq  24498  relogbexp  24518  leibpilem1  24667  sgmval2  24869  ppiprm  24877  ppinprm  24878  chtprm  24879  chtnprm  24880  lgslem3  25024  lgsneg  25046  lgsdir2lem2  25051  lgsdir2lem4  25053  lgsdir2  25055  lgssq  25062  lgsmulsqcoprm  25068  lgsdirnn0  25069  gausslemma2dlem3  25093  lgsquadlem1  25105  lgsquadlem2  25106  lgsquad2  25111  2lgslem1a2  25115  2lgsoddprmlem1  25133  2lgsoddprmlem2  25134  2sqlem2  25143  2sqlem7  25149  rplogsumlem2  25174  axlowdimlem13  25834  wlk1walk  26535  clwwisshclwwslemlem  26926  extwwlkfablem2  27210  ipasslem5  27690  rearchi  29842  pdivsq  31635  dvdspw  31636  knoppndvlem9  32511  poimirlem19  33428  itg2addnclem2  33462  lzenom  37333  rexzrexnn0  37368  pell1234qrne0  37417  pell1234qrreccl  37418  pell1234qrmulcl  37419  pell1234qrdich  37425  pell14qrdich  37433  reglogexp  37458  reglogexpbas  37461  rmxm1  37499  rmym1  37500  rmxdbl  37504  rmydbl  37505  jm2.24  37530  congtr  37532  congadd  37533  congmul  37534  congsym  37535  congneg  37536  congid  37538  congabseq  37541  acongsym  37543  acongneg2  37544  acongtr  37545  acongrep  37547  jm2.19lem3  37558  jm2.19lem4  37559  jm2.19  37560  jm2.25  37566  jm2.26a  37567  oddfl  39489  coskpi2  40077  cosknegpi  40080  dvdsn1add  40154  itgsinexp  40170  fourierdlem42  40366  fourierdlem97  40420  fourierswlem  40447  2elfz2melfz  41328  addlenrevpfx  41397  pfxccatin12lem1  41423  pfxccatin12lem2  41424  pfxccatin12  41425  sfprmdvdsmersenne  41520  proththd  41531  dfodd6  41550  dfeven4  41551  evenm1odd  41552  evenp1odd  41553  enege  41558  onego  41559  dfeven2  41562  bits0ALTV  41590  opoeALTV  41594  opeoALTV  41595  evensumeven  41616  sbgoldbwt  41665  nnsum3primesgbe  41680  0nodd  41810  2nodd  41812  1neven  41932  2zlidl  41934  2zrngamgm  41939  2zrngasgrp  41940  2zrngagrp  41943  2zrngmmgm  41946  2zrngmsgrp  41947  2zrngnmrid  41950  zlmodzxzsub  42138  flsubz  42312  mod0mul  42314  m1modmmod  42316  zofldiv2  42325  dignn0flhalflem1  42409  dignn0flhalflem2  42410