Theorem zcn 9528

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8073  ℤcz 9523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-resscn 8167

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-rab 2520  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031  df-neg 8395  df-z 9524

This theorem is referenced by:  zsscn  9531  zaddcllempos  9560  peano2zm  9561  zaddcllemneg  9562  zaddcl  9563  zsubcl  9564  zrevaddcl  9574  nzadd  9576  zlem1lt  9580  zltlem1  9581  zapne  9598  zdiv  9612  zdivadd  9613  zdivmul  9614  zextlt  9616  zneo  9625  zeo2  9630  peano5uzti  9632  zindd  9642  divfnzn  9899  qmulz  9901  zq  9904  qaddcl  9913  qnegcl  9914  qmulcl  9915  qreccl  9920  fzen  10323  uzsubsubfz  10327  fz01en  10333  fzmmmeqm  10338  fzsubel  10340  fztp  10358  fzsuc2  10359  fzrev2  10365  fzrev3  10367  elfzp1b  10377  fzrevral  10385  fzrevral2  10386  fzrevral3  10387  fzshftral  10388  fzo0addel  10479  fzo0addelr  10480  fzoaddel2  10481  fzosubel2  10486  eluzgtdifelfzo  10488  fzocatel  10490  elfzom1elp1fzo  10493  fzval3  10495  zpnn0elfzo1  10499  fzosplitprm1  10526  fzoshftral  10530  flqzadd  10604  2tnp1ge0ge0  10607  ceilid  10623  intfracq  10628  zmod10  10648  modqmuladdnn0  10676  addmodlteq  10706  frecfzen2  10735  seqshft2g  10790  ser3mono  10795  m1expeven  10894  expsubap  10895  zesq  10966  sqoddm1div8  11001  bccmpl  11062  swrd00g  11279  swrdswrd  11335  swrdpfx  11337  pfxccatin12lem4  11356  pfxccatin12lem1  11358  swrdccatin2  11359  pfxccatin12lem2  11361  pfxccatin12  11363  shftuz  11440  nnabscl  11723  climshftlemg  11925  climshft  11927  mptfzshft  12066  fsumrev  12067  fisum0diag2  12071  efexp  12306  efzval  12307  demoivre  12397  dvdsval2  12414  iddvds  12428  1dvds  12429  dvds0  12430  negdvdsb  12431  dvdsnegb  12432  0dvds  12435  dvdsmul1  12437  iddvdsexp  12439  muldvds1  12440  muldvds2  12441  dvdscmul  12442  dvdsmulc  12443  summodnegmod  12446  modmulconst  12447  dvds2ln  12448  dvds2add  12449  dvds2sub  12450  dvdstr  12452  dvdssub2  12459  dvdsadd  12460  dvdsaddr  12461  dvdssub  12462  dvdssubr  12463  dvdsadd2b  12464  dvdsabseq  12471  divconjdvds  12473  alzdvds  12478  addmodlteqALT  12483  zeo3  12492  odd2np1lem  12496  odd2np1  12497  even2n  12498  oddp1even  12500  mulsucdiv2z  12509  zob  12515  ltoddhalfle  12517  halfleoddlt  12518  opoe  12519  omoe  12520  opeo  12521  omeo  12522  m1exp1  12525  divalgb  12549  divalgmod  12551  modremain  12553  ndvdssub  12554  ndvdsadd  12555  flodddiv4  12560  flodddiv4t2lthalf  12563  bits0  12572  bitsp1e  12576  bitsp1o  12577  gcdneg  12616  gcdadd  12619  gcdid  12620  modgcd  12625  dvdsgcd  12646  mulgcd  12650  absmulgcd  12651  mulgcdr  12652  gcddiv  12653  gcdmultiplez  12655  dvdssqim  12658  dvdssq  12665  bezoutr1  12667  lcmneg  12709  lcmgcdlem  12712  lcmgcd  12713  lcmid  12715  lcm1  12716  coprmdvds  12727  coprmdvds2  12728  qredeq  12731  qredeu  12732  divgcdcoprmex  12737  cncongr1  12738  cncongr2  12739  prmdvdsexp  12783  rpexp1i  12789  sqrt2irr  12797  divnumden  12831  phiprmpw  12857  nnnn0modprm0  12891  modprmn0modprm0  12892  coprimeprodsq2  12894  pclemub  12923  pcprendvds2  12927  pcmul  12937  pcneg  12961  fldivp1  12984  prmpwdvds  12991  zgz  13009  4sqexercise1  13034  4sqexercise2  13035  modxai  13052  mulgz  13800  mulgassr  13810  mulgmodid  13811  gsumfzconst  13991  zsubrg  14660  zsssubrg  14664  zringmulg  14677  zringinvg  14683  mulgrhm2  14689  znunit  14738  ef2kpi  15600  efper  15601  sinperlem  15602  sin2kpi  15605  cos2kpi  15606  abssinper  15640  sinkpi  15641  coskpi  15642  cxpexprp  15689  sgmval2  15781  lgslem3  15804  lgsneg  15826  lgsdir2lem2  15831  lgsdir2lem4  15833  lgsdir2  15835  lgssq  15842  lgsmulsqcoprm  15848  lgsdirnn0  15849  gausslemma2dlem3  15865  lgsquadlem1  15879  lgsquadlem2  15880  lgsquad2  15885  2lgslem1a2  15889  2lgsoddprmlem1  15907  2lgsoddprmlem2  15908  2sqlem2  15917  2sqlem7  15923  wlk1walkdom  16283