Theorem zcn 9582

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℂcc 8125  ℤcz 9577

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 2214  ax-resscn 8219

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-rab 2529  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360  df-ov 6053  df-neg 8447  df-z 9578

This theorem is referenced by:  zsscn  9585  zaddcllempos  9614  peano2zm  9615  zaddcllemneg  9616  zaddcl  9617  zsubcl  9618  zrevaddcl  9628  nzadd  9630  zlem1lt  9634  zltlem1  9635  zapne  9652  zdiv  9666  zdivadd  9667  zdivmul  9668  zextlt  9670  zneo  9679  zeo2  9684  peano5uzti  9686  zindd  9696  divfnzn  9953  qmulz  9955  zq  9958  qaddcl  9967  qnegcl  9968  qmulcl  9969  qreccl  9974  fzen  10377  uzsubsubfz  10381  fz01en  10387  fzmmmeqm  10392  fzsubel  10394  fztp  10412  fzsuc2  10413  fzrev2  10419  fzrev3  10421  elfzp1b  10431  fzrevral  10439  fzrevral2  10440  fzrevral3  10441  fzshftral  10442  fzo0addel  10533  fzo0addelr  10534  fzoaddel2  10535  fzosubel2  10540  eluzgtdifelfzo  10542  fzocatel  10544  elfzom1elp1fzo  10547  fzval3  10549  zpnn0elfzo1  10553  fzosplitprm1  10580  fzoshftral  10584  flqzadd  10658  2tnp1ge0ge0  10661  ceilid  10677  intfracq  10682  zmod10  10702  modqmuladdnn0  10730  addmodlteq  10760  frecfzen2  10789  seqshft2g  10844  ser3mono  10849  m1expeven  10948  expsubap  10949  zesq  11020  sqoddm1div8  11055  bccmpl  11116  swrd00g  11341  swrdswrd  11397  swrdpfx  11399  pfxccatin12lem4  11418  pfxccatin12lem1  11420  swrdccatin2  11421  pfxccatin12lem2  11423  pfxccatin12  11425  shftuz  11502  nnabscl  11785  climshftlemg  11987  climshft  11989  mptfzshft  12128  fsumrev  12129  fisum0diag2  12133  efexp  12368  efzval  12369  demoivre  12459  dvdsval2  12476  iddvds  12490  1dvds  12491  dvds0  12492  negdvdsb  12493  dvdsnegb  12494  0dvds  12497  dvdsmul1  12499  iddvdsexp  12501  muldvds1  12502  muldvds2  12503  dvdscmul  12504  dvdsmulc  12505  summodnegmod  12508  modmulconst  12509  dvds2ln  12510  dvds2add  12511  dvds2sub  12512  dvdstr  12514  dvdssub2  12521  dvdsadd  12522  dvdsaddr  12523  dvdssub  12524  dvdssubr  12525  dvdsadd2b  12526  dvdsabseq  12533  divconjdvds  12535  alzdvds  12540  addmodlteqALT  12545  zeo3  12554  odd2np1lem  12558  odd2np1  12559  even2n  12560  oddp1even  12562  mulsucdiv2z  12571  zob  12577  ltoddhalfle  12579  halfleoddlt  12580  opoe  12581  omoe  12582  opeo  12583  omeo  12584  m1exp1  12587  divalgb  12611  divalgmod  12613  modremain  12615  ndvdssub  12616  ndvdsadd  12617  flodddiv4  12622  flodddiv4t2lthalf  12625  bits0  12634  bitsp1e  12638  bitsp1o  12639  gcdneg  12678  gcdadd  12681  gcdid  12682  modgcd  12687  dvdsgcd  12708  mulgcd  12712  absmulgcd  12713  mulgcdr  12714  gcddiv  12715  gcdmultiplez  12717  dvdssqim  12720  dvdssq  12727  bezoutr1  12729  lcmneg  12771  lcmgcdlem  12774  lcmgcd  12775  lcmid  12777  lcm1  12778  coprmdvds  12789  coprmdvds2  12790  qredeq  12793  qredeu  12794  divgcdcoprmex  12799  cncongr1  12800  cncongr2  12801  prmdvdsexp  12845  rpexp1i  12851  sqrt2irr  12859  divnumden  12893  phiprmpw  12919  nnnn0modprm0  12953  modprmn0modprm0  12954  coprimeprodsq2  12956  pclemub  12985  pcprendvds2  12989  pcmul  12999  pcneg  13023  fldivp1  13046  prmpwdvds  13053  zgz  13071  4sqexercise1  13096  4sqexercise2  13097  modxai  13114  mulgz  13867  mulgassr  13877  mulgmodid  13878  gsumfzconst  14058  zsubrg  14729  zsssubrg  14733  zringmulg  14746  zringinvg  14752  mulgrhm2  14758  znunit  14807  ef2kpi  15671  efper  15672  sinperlem  15673  sin2kpi  15676  cos2kpi  15677  abssinper  15711  sinkpi  15712  coskpi  15713  cxpexprp  15760  sgmval2  15852  lgslem3  15875  lgsneg  15897  lgsdir2lem2  15902  lgsdir2lem4  15904  lgsdir2  15906  lgssq  15913  lgsmulsqcoprm  15919  lgsdirnn0  15920  gausslemma2dlem3  15936  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2  15956  2lgslem1a2  15960  2lgsoddprmlem1  15978  2lgsoddprmlem2  15979  2sqlem2  15988  2sqlem7  15994  wlk1walkdom  16354