Theorem zcn 12529

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  ℤcz 12524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-neg 11380  df-z 12525

This theorem is referenced by:  zsscn  12532  zsubcl  12569  zrevaddcl  12572  nzadd  12575  zlem1lt  12579  zltlem1  12580  zdiv  12599  zdivadd  12600  zdivmul  12601  zextlt  12603  zneo  12612  zeo2  12616  peano5uzi  12618  zindd  12630  znnn0nn  12640  zriotaneg  12642  zmax  12895  rebtwnz  12897  qmulz  12901  zq  12904  qaddcl  12915  qnegcl  12916  qmulcl  12917  qreccl  12919  fzen  13495  uzsubsubfz  13500  fz01en  13506  fzmmmeqm  13511  fzsubel  13514  fztp  13534  fzsuc2  13536  fzrev2  13542  fzrev3  13544  elfzp1b  13555  fzrevral  13566  fzrevral2  13567  fzrevral3  13568  fzshftral  13569  fzo0addel  13673  fzo0addelr  13674  fzoaddel2  13675  fzosubel2  13680  eluzgtdifelfzo  13682  fzocatel  13684  elfzom1elp1fzo  13687  fzval3  13689  zpnn0elfzo1  13694  fzosplitprm1  13733  fzoshftral  13742  flzadd  13785  2tnp1ge0ge0  13788  ceilid  13810  quoremz  13814  intfracq  13818  mulmod0  13836  zmod10  13846  modcyc  13865  modcyc2  13866  muladdmodid  13872  mulp1mod1  13873  modmuladdnn0  13877  modmul1  13886  modmulmodr  13899  modaddmulmod  13900  uzrdgxfr  13929  fzen2  13931  seqshft2  13990  sermono  13996  m1expeven  14071  expsub  14072  zesq  14188  modexp  14200  sqoddm1div8  14205  bccmpl  14271  swrd00  14607  swrdswrd  14667  swrdpfx  14669  pfxccatin12lem4  14688  pfxccatin12lem1  14690  swrdccatin2  14691  pfxccatin12lem2  14693  pfxccatin12  14695  repswrevw  14749  cshwsublen  14758  cshwidxmodr  14766  cshwidx0mod  14767  2cshw  14775  2cshwid  14776  2cshwcom  14778  cshweqdif2  14781  cshweqrep  14783  cshw1  14784  2cshwcshw  14787  shftuz  15031  seqshft  15047  nn0abscl  15274  zabs0b  15276  nnabscl  15288  climshftlem  15536  climshft  15538  isershft  15626  mptfzshft  15740  fsumrev  15741  fsum0diag2  15745  efexp  16068  efzval  16069  demoivre  16167  sqrt2irr  16216  dvdsval2  16224  iddvds  16238  1dvds  16239  dvds0  16240  negdvdsb  16241  dvdsnegb  16242  0dvds  16245  dvdsmul1  16246  iddvdsexp  16248  muldvds1  16249  muldvds2  16250  dvdscmul  16251  dvdsmulc  16252  dvdscmulr  16253  dvdsmulcr  16254  summodnegmod  16255  difmod0  16256  modmulconst  16257  dvds2ln  16258  dvds2add  16259  dvds2sub  16260  dvdstr  16263  dvdssub2  16270  dvdsadd  16271  dvdsaddr  16272  dvdssub  16273  dvdssubr  16274  dvdsadd2b  16275  dvdsaddre2b  16276  dvdsabseq  16282  divconjdvds  16284  alzdvds  16289  addmodlteqALT  16294  dvdsexp2im  16296  odd2np1lem  16309  odd2np1  16310  even2n  16311  oddp1even  16313  mod2eq1n2dvds  16316  mulsucdiv2z  16322  zob  16328  ltoddhalfle  16330  halfleoddlt  16331  opoe  16332  omoe  16333  opeo  16334  omeo  16335  m1exp1  16345  divalglem0  16362  divalglem2  16364  divalglem4  16365  divalglem5  16366  divalglem9  16370  divalgb  16373  divalgmod  16375  modremain  16377  ndvdssub  16378  ndvdsadd  16379  flodddiv4  16384  flodddiv4t2lthalf  16387  bits0  16397  bitsp1e  16401  bitsp1o  16402  gcdneg  16491  gcdaddmlem  16493  gcdaddm  16494  gcdadd  16495  gcdid  16496  modgcd  16501  gcdmultiplez  16504  bezoutlem1  16508  bezoutlem2  16509  bezoutlem4  16511  dvdsgcd  16513  mulgcd  16517  absmulgcd  16518  mulgcdr  16519  gcddiv  16520  dvdssqim  16523  dvdsexpim  16524  zexpgcd  16534  dvdssq  16536  bezoutr1  16538  lcmcllem  16565  lcmneg  16572  lcmgcdlem  16575  lcmgcd  16576  lcmid  16578  lcm1  16579  coprmdvds  16622  coprmdvds2  16623  qredeq  16626  qredeu  16627  divgcdcoprmex  16635  cncongr1  16636  cncongr2  16637  prmdvdsexp  16685  rpexp1i  16693  divnumden  16718  zsqrtelqelz  16728  phiprmpw  16746  vfermltlALT  16773  nnnn0modprm0  16777  modprmn0modprm0  16778  coprimeprodsq2  16780  iserodd  16806  pclem  16809  pcprendvds2  16812  pcpremul  16814  pcmul  16822  pcneg  16845  fldivp1  16868  prmpwdvds  16875  zgz  16904  modxai  17039  mod2xnegi  17042  chnccat  18592  chnrev  18593  mulgfval  19045  mulgz  19078  mulgassr  19088  mulgmodid  19089  odmod  19521  odf1  19537  odf1o1  19547  gexdvds  19559  zaddablx  19847  ablfacrp  20043  pgpfac1lem3  20054  ablsimpgfindlem1  20084  zsubrg  21400  zsssubrg  21405  zringsub  21435  zringmulg  21436  zringinvg  21445  zringunit  21446  zringcyg  21449  prmirred  21454  mulgrhm2  21458  pzriprnglem6  21466  pzriprnglem8  21468  pzriprnglem10  21470  pzriprnglem12  21472  fermltlchr  21509  znunit  21543  degltp1le  26038  ef2kpi  26442  efper  26443  sinperlem  26444  sin2kpi  26447  cos2kpi  26448  abssinper  26485  sinkpi  26486  coskpi  26487  eflogeq  26566  cxpexpz  26631  root1eq1  26719  cxpeq  26721  zrtelqelz  26722  zrtdvds  26723  relogbexp  26744  sgmval2  27106  ppiprm  27114  ppinprm  27115  chtprm  27116  chtnprm  27117  lgslem3  27262  lgsneg  27284  lgsdir2lem2  27289  lgsdir2lem4  27291  lgsdir2  27293  lgssq  27300  lgsmulsqcoprm  27306  lgsdirnn0  27307  gausslemma2dlem3  27331  lgsquadlem1  27343  lgsquadlem2  27344  lgsquad2  27349  2lgslem1a2  27353  2lgsoddprmlem1  27371  2lgsoddprmlem2  27372  2sqlem2  27381  2sqlem7  27387  rplogsumlem2  27448  axlowdimlem13  29023  wlk1walk  29707  clwwisshclwwslemlem  30083  ipasslem5  30906  rearchi  33406  znfermltl  33426  knoppndvlem9  36780  poimirlem19  37960  itg2addnclem2  37993  gcdaddmzz2nncomi  42434  zdivgd  42769  ef11d  42771  cxp112d  42773  cxp111d  42774  cxpi11d  42775  dffltz  43067  lzenom  43202  rexzrexnn0  43232  pell1234qrne0  43281  pell1234qrreccl  43282  pell1234qrmulcl  43283  pell1234qrdich  43289  pell14qrdich  43297  reglogexp  43322  reglogexpbas  43325  rmxm1  43362  rmym1  43363  rmxdbl  43367  rmydbl  43368  jm2.24  43391  congtr  43393  congadd  43394  congmul  43395  congsym  43396  congneg  43397  congid  43399  congabseq  43402  acongsym  43404  acongneg2  43405  acongtr  43406  acongrep  43408  jm2.19lem3  43419  jm2.19lem4  43420  jm2.19  43421  jm2.25  43427  jm2.26a  43428  oddfl  45711  coskpi2  46294  cosknegpi  46297  dvdsn1add  46367  itgsinexp  46383  fourierdlem42  46577  fourierdlem97  46631  fourierswlem  46658  sinnpoly  47339  2elfz2melfz  47766  ceilbi  47785  flmrecm1  47791  submodaddmod  47795  submodneaddmod  47805  mod0mul  47810  m1modmmod  47812  modmkpkne  47815  modlt0b  47817  sfprmdvdsmersenne  48066  proththd  48077  ppivalnnprm  48088  ppivalnnnprmge6  48089  dfodd6  48113  dfeven4  48114  evenm1odd  48115  evenp1odd  48116  enege  48121  onego  48122  dfeven2  48125  bits0ALTV  48155  opoeALTV  48159  opeoALTV  48160  evensumeven  48183  fppr2odd  48207  sbgoldbwt  48253  nnsum3primesgbe  48268  gpgedgvtx0  48537  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx13starlem2  48548  0nodd  48646  2nodd  48648  1neven  48714  2zlidl  48716  2zrngamgm  48721  2zrngasgrp  48722  2zrngagrp  48725  2zrngmmgm  48728  2zrngmsgrp  48729  2zrngnmrid  48732  zlmodzxzsub  48836  flsubz  48998  zofldiv2  49007  dignn0flhalflem1  49091  dignn0flhalflem2  49092