Theorem zcn 9376

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

Syntax hints:   → wi 4   ∈ wcel 2175  ℂcc 7922  ℤcz 9371

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-resscn 8016

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rex 2489  df-rab 2492  df-v 2773  df-un 3169  df-in 3171  df-ss 3178  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-iota 5231  df-fv 5278  df-ov 5946  df-neg 8245  df-z 9372

This theorem is referenced by:  zsscn  9379  zaddcllempos  9408  peano2zm  9409  zaddcllemneg  9410  zaddcl  9411  zsubcl  9412  zrevaddcl  9422  nzadd  9424  zlem1lt  9428  zltlem1  9429  zapne  9446  zdiv  9460  zdivadd  9461  zdivmul  9462  zextlt  9464  zneo  9473  zeo2  9478  peano5uzti  9480  zindd  9490  divfnzn  9741  qmulz  9743  zq  9746  qaddcl  9755  qnegcl  9756  qmulcl  9757  qreccl  9762  fzen  10164  uzsubsubfz  10168  fz01en  10174  fzmmmeqm  10179  fzsubel  10181  fztp  10199  fzsuc2  10200  fzrev2  10206  fzrev3  10208  elfzp1b  10218  fzrevral  10226  fzrevral2  10227  fzrevral3  10228  fzshftral  10229  fzo0addel  10315  fzo0addelr  10316  fzoaddel2  10317  fzosubel2  10322  eluzgtdifelfzo  10324  fzocatel  10326  elfzom1elp1fzo  10329  fzval3  10331  zpnn0elfzo1  10335  fzosplitprm1  10361  fzoshftral  10365  flqzadd  10439  2tnp1ge0ge0  10442  ceilid  10458  intfracq  10463  zmod10  10483  modqmuladdnn0  10511  addmodlteq  10541  frecfzen2  10570  seqshft2g  10625  ser3mono  10630  m1expeven  10729  expsubap  10730  zesq  10801  sqoddm1div8  10836  bccmpl  10897  shftuz  11070  nnabscl  11353  climshftlemg  11555  climshft  11557  mptfzshft  11695  fsumrev  11696  fisum0diag2  11700  efexp  11935  efzval  11936  demoivre  12026  dvdsval2  12043  iddvds  12057  1dvds  12058  dvds0  12059  negdvdsb  12060  dvdsnegb  12061  0dvds  12064  dvdsmul1  12066  iddvdsexp  12068  muldvds1  12069  muldvds2  12070  dvdscmul  12071  dvdsmulc  12072  summodnegmod  12075  modmulconst  12076  dvds2ln  12077  dvds2add  12078  dvds2sub  12079  dvdstr  12081  dvdssub2  12088  dvdsadd  12089  dvdsaddr  12090  dvdssub  12091  dvdssubr  12092  dvdsadd2b  12093  dvdsabseq  12100  divconjdvds  12102  alzdvds  12107  addmodlteqALT  12112  zeo3  12121  odd2np1lem  12125  odd2np1  12126  even2n  12127  oddp1even  12129  mulsucdiv2z  12138  zob  12144  ltoddhalfle  12146  halfleoddlt  12147  opoe  12148  omoe  12149  opeo  12150  omeo  12151  m1exp1  12154  divalgb  12178  divalgmod  12180  modremain  12182  ndvdssub  12183  ndvdsadd  12184  flodddiv4  12189  flodddiv4t2lthalf  12192  bits0  12201  bitsp1e  12205  bitsp1o  12206  gcdneg  12245  gcdadd  12248  gcdid  12249  modgcd  12254  dvdsgcd  12275  mulgcd  12279  absmulgcd  12280  mulgcdr  12281  gcddiv  12282  gcdmultiplez  12284  dvdssqim  12287  dvdssq  12294  bezoutr1  12296  lcmneg  12338  lcmgcdlem  12341  lcmgcd  12342  lcmid  12344  lcm1  12345  coprmdvds  12356  coprmdvds2  12357  qredeq  12360  qredeu  12361  divgcdcoprmex  12366  cncongr1  12367  cncongr2  12368  prmdvdsexp  12412  rpexp1i  12418  sqrt2irr  12426  divnumden  12460  phiprmpw  12486  nnnn0modprm0  12520  modprmn0modprm0  12521  coprimeprodsq2  12523  pclemub  12552  pcprendvds2  12556  pcmul  12566  pcneg  12590  fldivp1  12613  prmpwdvds  12620  zgz  12638  4sqexercise1  12663  4sqexercise2  12664  modxai  12681  mulgz  13428  mulgassr  13438  mulgmodid  13439  gsumfzconst  13619  zsubrg  14285  zsssubrg  14289  zringmulg  14302  zringinvg  14308  mulgrhm2  14314  znunit  14363  ef2kpi  15220  efper  15221  sinperlem  15222  sin2kpi  15225  cos2kpi  15226  abssinper  15260  sinkpi  15261  coskpi  15262  cxpexprp  15309  sgmval2  15398  lgslem3  15421  lgsneg  15443  lgsdir2lem2  15448  lgsdir2lem4  15450  lgsdir2  15452  lgssq  15459  lgsmulsqcoprm  15465  lgsdirnn0  15466  gausslemma2dlem3  15482  lgsquadlem1  15496  lgsquadlem2  15497  lgsquad2  15502  2lgslem1a2  15506  2lgsoddprmlem1  15524  2lgsoddprmlem2  15525  2sqlem2  15534  2sqlem7  15540