Theorem zcn 11796

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

Syntax hints:   → wi 4   ∈ wcel 2050  ℂcc 10331  ℤcz 11791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744  ax-resscn 10390

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rex 3088  df-rab 3091  df-v 3411  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4709  df-br 4926  df-iota 6149  df-fv 6193  df-ov 6977  df-neg 10671  df-z 11792

This theorem is referenced by:  zsscn  11799  zsubcl  11835  zrevaddcl  11838  nzadd  11841  zlem1lt  11845  zltlem1  11846  zdiv  11863  zdivadd  11864  zdivmul  11865  zextlt  11867  zneo  11876  zeo2  11880  peano5uzi  11882  zindd  11894  znnn0nn  11905  zriotaneg  11907  zmax  12157  rebtwnz  12159  qmulz  12163  zq  12166  zqOLD  12167  qaddcl  12177  qnegcl  12178  qmulcl  12179  qreccl  12181  fzen  12738  uzsubsubfz  12743  fz01en  12749  fzmmmeqm  12754  fzsubel  12757  fztp  12777  fzsuc2  12779  fzrev2  12785  fzrev3  12787  elfzp1b  12798  fzrevral  12806  fzrevral2  12807  fzrevral3  12808  fzshftral  12809  fzo0addel  12904  fzo0addelr  12905  fzoaddel2  12906  elfzoext  12907  fzosubel2  12910  eluzgtdifelfzo  12912  fzocatel  12914  elfzom1elp1fzo  12917  fzval3  12919  zpnn0elfzo1  12924  fzosplitprm1  12960  fzoshftral  12967  flzadd  13009  2tnp1ge0ge0  13012  ceilid  13032  quoremz  13036  intfracq  13040  mulmod0  13058  zmod10  13068  modcyc  13087  modcyc2  13088  muladdmodid  13092  mulp1mod1  13093  modmuladdnn0  13096  modmul1  13105  modmulmodr  13118  modaddmulmod  13119  uzrdgxfr  13148  fzen2  13150  seqshft2  13209  sermono  13215  m1expeven  13289  expsub  13290  zesq  13400  modexp  13412  sqoddm1div8  13417  bccmpl  13482  swrd00  13805  addlenrevswrdOLD  13827  addlenrevpfx  13870  swrdswrd  13885  swrdswrd0OLD  13888  swrdpfx  13889  swrdccatin12lem1  13923  pfxccatin12lem1  13925  swrdccatin12lem2bOLD  13926  swrdccatin2  13927  pfxccatin12lem2  13929  swrdccatin12lem2OLD  13930  pfxccatin12  13932  swrdccatin12OLD  13933  repswrevw  14004  cshwsublen  14018  cshwidxmodr  14026  cshwidx0mod  14027  2cshw  14035  2cshwid  14036  2cshwcom  14038  cshweqdif2  14041  cshweqrep  14043  cshw1  14044  2cshwcshw  14047  shftuz  14287  seqshft  14303  nn0abscl  14531  nnabscl  14544  climshftlem  14790  climshft  14792  isershft  14879  mptfzshft  14991  fsumrev  14992  fsum0diag2  14996  efexp  15312  efzval  15313  demoivre  15411  sqrt2irr  15460  dvdsval2  15468  iddvds  15481  1dvds  15482  dvds0  15483  negdvdsb  15484  dvdsnegb  15485  0dvds  15488  dvdsmul1  15489  iddvdsexp  15491  muldvds1  15492  muldvds2  15493  dvdscmul  15494  dvdsmulc  15495  dvdscmulr  15496  dvdsmulcr  15497  summodnegmod  15498  modmulconst  15499  dvds2ln  15500  dvds2add  15501  dvds2sub  15502  dvdstr  15504  dvdssub2  15509  dvdsadd  15510  dvdsaddr  15511  dvdssub  15512  dvdssubr  15513  dvdsadd2b  15514  dvdsaddre2b  15515  dvdsabseq  15521  divconjdvds  15523  alzdvds  15528  addmodlteqALT  15533  odd2np1lem  15547  odd2np1  15548  even2n  15549  oddp1even  15551  mod2eq1n2dvds  15554  mulsucdiv2z  15560  zob  15566  ltoddhalfle  15568  halfleoddlt  15569  opoe  15570  omoe  15571  opeo  15572  omeo  15573  m1exp1  15585  divalglem0  15602  divalglem2  15604  divalglem4  15605  divalglem5  15606  divalglem9  15610  divalgb  15613  divalgmod  15615  modremain  15617  ndvdssub  15618  ndvdsadd  15619  flodddiv4  15622  flodddiv4t2lthalf  15625  bits0  15635  bitsp1e  15639  bitsp1o  15640  gcdneg  15728  gcdaddmlem  15730  gcdaddm  15731  gcdadd  15732  gcdid  15733  modgcd  15738  bezoutlem1  15741  bezoutlem2  15742  bezoutlem4  15744  dvdsgcd  15746  mulgcd  15750  absmulgcd  15751  mulgcdr  15752  gcddiv  15753  gcdmultiplez  15755  dvdssqim  15758  dvdssq  15765  bezoutr1  15767  lcmcllem  15794  lcmneg  15801  lcmgcdlem  15804  lcmgcd  15805  lcmid  15807  lcm1  15808  coprmdvds  15851  coprmdvds2  15852  qredeq  15855  qredeu  15856  divgcdcoprmex  15864  cncongr1  15865  cncongr2  15866  prmdvdsexp  15913  rpexp1i  15919  divnumden  15942  zsqrtelqelz  15952  phiprmpw  15967  vfermltlALT  15993  nnnn0modprm0  15997  modprmn0modprm0  15998  coprimeprodsq2  16000  iserodd  16026  pclem  16029  pcprendvds2  16032  pcpremul  16034  pcmul  16042  pcneg  16064  fldivp1  16087  prmpwdvds  16094  zgz  16123  modxai  16258  mod2xnegi  16261  mulgfval  18025  mulgz  18051  mulgassr  18061  mulgmodid  18062  odmod  18448  odf1  18462  odf1o1  18470  gexdvds  18482  zaddablx  18760  cygabl  18777  ablfacrp  18950  pgpfac1lem3  18961  zsubrg  20312  zsssubrg  20317  zringmulg  20339  zringinvg  20348  zringunit  20349  zringcyg  20352  prmirred  20356  mulgrhm2  20360  znunit  20424  degltp1le  24382  ef2kpi  24779  efper  24780  sinperlem  24781  sin2kpi  24784  cos2kpi  24785  abssinper  24821  sinkpi  24822  coskpi  24823  eflogeq  24898  cxpexpz  24963  root1eq1  25049  cxpeq  25051  relogbexp  25071  leibpilem1OLD  25232  sgmval2  25434  ppiprm  25442  ppinprm  25443  chtprm  25444  chtnprm  25445  lgslem3  25589  lgsneg  25611  lgsdir2lem2  25616  lgsdir2lem4  25618  lgsdir2  25620  lgssq  25627  lgsmulsqcoprm  25633  lgsdirnn0  25634  gausslemma2dlem3  25658  lgsquadlem1  25670  lgsquadlem2  25671  lgsquad2  25676  2lgslem1a2  25680  2lgsoddprmlem1  25698  2lgsoddprmlem2  25699  2sqlem2  25708  2sqlem7  25714  rplogsumlem2  25775  axlowdimlem13  26455  wlk1walk  27135  clwwisshclwwslemlem  27540  ipasslem5  28401  rearchi  30623  pdivsq  32530  dvdspw  32531  knoppndvlem9  33408  poimirlem19  34381  itg2addnclem2  34414  dvdsexpim  38642  zexpgcd  38646  zrtelqelz  38653  zrtdvds  38654  dffltz  38707  lzenom  38791  rexzrexnn0  38826  pell1234qrne0  38875  pell1234qrreccl  38876  pell1234qrmulcl  38877  pell1234qrdich  38883  pell14qrdich  38891  reglogexp  38916  reglogexpbas  38919  rmxm1  38956  rmym1  38957  rmxdbl  38961  rmydbl  38962  jm2.24  38985  congtr  38987  congadd  38988  congmul  38989  congsym  38990  congneg  38991  congid  38993  congabseq  38996  acongsym  38998  acongneg2  38999  acongtr  39000  acongrep  39002  jm2.19lem3  39013  jm2.19lem4  39014  jm2.19  39015  jm2.25  39021  jm2.26a  39022  ablsimpgfindlem1  40072  oddfl  40997  coskpi2  41602  cosknegpi  41605  dvdsn1add  41679  itgsinexp  41695  fourierdlem42  41890  fourierdlem97  41944  fourierswlem  41971  2elfz2melfz  42949  sfprmdvdsmersenne  43161  proththd  43172  dfodd6  43195  dfeven4  43196  evenm1odd  43197  evenp1odd  43198  enege  43203  onego  43204  dfeven2  43207  bits0ALTV  43237  opoeALTV  43241  opeoALTV  43242  evensumeven  43265  fppr2odd  43289  sbgoldbwt  43335  nnsum3primesgbe  43350  0nodd  43470  2nodd  43472  1neven  43592  2zlidl  43594  2zrngamgm  43599  2zrngasgrp  43600  2zrngagrp  43603  2zrngmmgm  43606  2zrngmsgrp  43607  2zrngnmrid  43610  zlmodzxzsub  43797  flsubz  43970  mod0mul  43972  m1modmmod  43974  zofldiv2  43984  dignn0flhalflem1  44068  dignn0flhalflem2  44069