Theorem zcn 12476

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11007  ℤcz 12471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11066

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-neg 11350  df-z 12472

This theorem is referenced by:  zsscn  12479  zsubcl  12517  zrevaddcl  12520  nzadd  12523  zlem1lt  12527  zltlem1  12528  zdiv  12546  zdivadd  12547  zdivmul  12548  zextlt  12550  zneo  12559  zeo2  12563  peano5uzi  12565  zindd  12577  znnn0nn  12587  zriotaneg  12589  zmax  12846  rebtwnz  12848  qmulz  12852  zq  12855  qaddcl  12866  qnegcl  12867  qmulcl  12868  qreccl  12870  fzen  13444  uzsubsubfz  13449  fz01en  13455  fzmmmeqm  13460  fzsubel  13463  fztp  13483  fzsuc2  13485  fzrev2  13491  fzrev3  13493  elfzp1b  13504  fzrevral  13515  fzrevral2  13516  fzrevral3  13517  fzshftral  13518  fzo0addel  13621  fzo0addelr  13622  fzoaddel2  13623  fzosubel2  13628  eluzgtdifelfzo  13630  fzocatel  13632  elfzom1elp1fzo  13635  fzval3  13637  zpnn0elfzo1  13642  fzosplitprm1  13680  fzoshftral  13687  flzadd  13730  2tnp1ge0ge0  13733  ceilid  13755  quoremz  13759  intfracq  13763  mulmod0  13781  zmod10  13791  modcyc  13810  modcyc2  13811  muladdmodid  13817  mulp1mod1  13818  modmuladdnn0  13822  modmul1  13831  modmulmodr  13844  modaddmulmod  13845  uzrdgxfr  13874  fzen2  13876  seqshft2  13935  sermono  13941  m1expeven  14016  expsub  14017  zesq  14133  modexp  14145  sqoddm1div8  14150  bccmpl  14216  swrd00  14551  swrdswrd  14611  swrdpfx  14613  pfxccatin12lem4  14632  pfxccatin12lem1  14634  swrdccatin2  14635  pfxccatin12lem2  14637  pfxccatin12  14639  repswrevw  14693  cshwsublen  14702  cshwidxmodr  14710  cshwidx0mod  14711  2cshw  14719  2cshwid  14720  2cshwcom  14722  cshweqdif2  14725  cshweqrep  14727  cshw1  14728  2cshwcshw  14732  shftuz  14976  seqshft  14992  nn0abscl  15219  zabs0b  15221  nnabscl  15233  climshftlem  15481  climshft  15483  isershft  15571  mptfzshft  15685  fsumrev  15686  fsum0diag2  15690  efexp  16010  efzval  16011  demoivre  16109  sqrt2irr  16158  dvdsval2  16166  iddvds  16180  1dvds  16181  dvds0  16182  negdvdsb  16183  dvdsnegb  16184  0dvds  16187  dvdsmul1  16188  iddvdsexp  16190  muldvds1  16191  muldvds2  16192  dvdscmul  16193  dvdsmulc  16194  dvdscmulr  16195  dvdsmulcr  16196  summodnegmod  16197  difmod0  16198  modmulconst  16199  dvds2ln  16200  dvds2add  16201  dvds2sub  16202  dvdstr  16205  dvdssub2  16212  dvdsadd  16213  dvdsaddr  16214  dvdssub  16215  dvdssubr  16216  dvdsadd2b  16217  dvdsaddre2b  16218  dvdsabseq  16224  divconjdvds  16226  alzdvds  16231  addmodlteqALT  16236  dvdsexp2im  16238  odd2np1lem  16251  odd2np1  16252  even2n  16253  oddp1even  16255  mod2eq1n2dvds  16258  mulsucdiv2z  16264  zob  16270  ltoddhalfle  16272  halfleoddlt  16273  opoe  16274  omoe  16275  opeo  16276  omeo  16277  m1exp1  16287  divalglem0  16304  divalglem2  16306  divalglem4  16307  divalglem5  16308  divalglem9  16312  divalgb  16315  divalgmod  16317  modremain  16319  ndvdssub  16320  ndvdsadd  16321  flodddiv4  16326  flodddiv4t2lthalf  16329  bits0  16339  bitsp1e  16343  bitsp1o  16344  gcdneg  16433  gcdaddmlem  16435  gcdaddm  16436  gcdadd  16437  gcdid  16438  modgcd  16443  gcdmultiplez  16446  bezoutlem1  16450  bezoutlem2  16451  bezoutlem4  16453  dvdsgcd  16455  mulgcd  16459  absmulgcd  16460  mulgcdr  16461  gcddiv  16462  dvdssqim  16465  dvdsexpim  16466  zexpgcd  16476  dvdssq  16478  bezoutr1  16480  lcmcllem  16507  lcmneg  16514  lcmgcdlem  16517  lcmgcd  16518  lcmid  16520  lcm1  16521  coprmdvds  16564  coprmdvds2  16565  qredeq  16568  qredeu  16569  divgcdcoprmex  16577  cncongr1  16578  cncongr2  16579  prmdvdsexp  16626  rpexp1i  16634  divnumden  16659  zsqrtelqelz  16669  phiprmpw  16687  vfermltlALT  16714  nnnn0modprm0  16718  modprmn0modprm0  16719  coprimeprodsq2  16721  iserodd  16747  pclem  16750  pcprendvds2  16753  pcpremul  16755  pcmul  16763  pcneg  16786  fldivp1  16809  prmpwdvds  16816  zgz  16845  modxai  16980  mod2xnegi  16983  mulgfval  18948  mulgz  18981  mulgassr  18991  mulgmodid  18992  odmod  19425  odf1  19441  odf1o1  19451  gexdvds  19463  zaddablx  19751  ablfacrp  19947  pgpfac1lem3  19958  ablsimpgfindlem1  19988  zsubrg  21327  zsssubrg  21332  zringsub  21362  zringmulg  21363  zringinvg  21372  zringunit  21373  zringcyg  21376  prmirred  21381  mulgrhm2  21385  pzriprnglem6  21393  pzriprnglem8  21395  pzriprnglem10  21397  pzriprnglem12  21399  fermltlchr  21436  znunit  21470  degltp1le  25976  ef2kpi  26385  efper  26386  sinperlem  26387  sin2kpi  26390  cos2kpi  26391  abssinper  26428  sinkpi  26429  coskpi  26430  eflogeq  26509  cxpexpz  26574  root1eq1  26663  cxpeq  26665  zrtelqelz  26666  zrtdvds  26667  relogbexp  26688  sgmval2  27051  ppiprm  27059  ppinprm  27060  chtprm  27061  chtnprm  27062  lgslem3  27208  lgsneg  27230  lgsdir2lem2  27235  lgsdir2lem4  27237  lgsdir2  27239  lgssq  27246  lgsmulsqcoprm  27252  lgsdirnn0  27253  gausslemma2dlem3  27277  lgsquadlem1  27289  lgsquadlem2  27290  lgsquad2  27295  2lgslem1a2  27299  2lgsoddprmlem1  27317  2lgsoddprmlem2  27318  2sqlem2  27327  2sqlem7  27333  rplogsumlem2  27394  axlowdimlem13  28899  wlk1walk  29584  clwwisshclwwslemlem  29957  ipasslem5  30779  rearchi  33283  znfermltl  33303  knoppndvlem9  36498  poimirlem19  37623  itg2addnclem2  37656  gcdaddmzz2nncomi  41972  zdivgd  42314  ef11d  42316  cxp112d  42318  cxp111d  42319  cxpi11d  42320  dffltz  42611  lzenom  42747  rexzrexnn0  42781  pell1234qrne0  42830  pell1234qrreccl  42831  pell1234qrmulcl  42832  pell1234qrdich  42838  pell14qrdich  42846  reglogexp  42871  reglogexpbas  42874  rmxm1  42911  rmym1  42912  rmxdbl  42916  rmydbl  42917  jm2.24  42940  congtr  42942  congadd  42943  congmul  42944  congsym  42945  congneg  42946  congid  42948  congabseq  42951  acongsym  42953  acongneg2  42954  acongtr  42955  acongrep  42957  jm2.19lem3  42968  jm2.19lem4  42969  jm2.19  42970  jm2.25  42976  jm2.26a  42977  oddfl  45264  coskpi2  45851  cosknegpi  45854  dvdsn1add  45924  itgsinexp  45940  fourierdlem42  46134  fourierdlem97  46188  fourierswlem  46215  sinnpoly  46879  2elfz2melfz  47306  ceilbi  47321  submodaddmod  47329  submodneaddmod  47339  mod0mul  47344  m1modmmod  47346  modmkpkne  47349  modlt0b  47351  sfprmdvdsmersenne  47591  proththd  47602  dfodd6  47625  dfeven4  47626  evenm1odd  47627  evenp1odd  47628  enege  47633  onego  47634  dfeven2  47637  bits0ALTV  47667  opoeALTV  47671  opeoALTV  47672  evensumeven  47695  fppr2odd  47719  sbgoldbwt  47765  nnsum3primesgbe  47780  gpgedgvtx0  48049  gpg5nbgrvtx03starlem2  48057  gpg5nbgrvtx13starlem2  48060  0nodd  48158  2nodd  48160  1neven  48226  2zlidl  48228  2zrngamgm  48233  2zrngasgrp  48234  2zrngagrp  48237  2zrngmmgm  48240  2zrngmsgrp  48241  2zrngnmrid  48244  zlmodzxzsub  48348  flsubz  48511  zofldiv2  48520  dignn0flhalflem1  48604  dignn0flhalflem2  48605