Theorem zcn 9334

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7880  ℤcz 9329

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-resscn 7974

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-rab 2484  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5926  df-neg 8203  df-z 9330

This theorem is referenced by:  zsscn  9337  zaddcllempos  9366  peano2zm  9367  zaddcllemneg  9368  zaddcl  9369  zsubcl  9370  zrevaddcl  9379  nzadd  9381  zlem1lt  9385  zltlem1  9386  zapne  9403  zdiv  9417  zdivadd  9418  zdivmul  9419  zextlt  9421  zneo  9430  zeo2  9435  peano5uzti  9437  zindd  9447  divfnzn  9698  qmulz  9700  zq  9703  qaddcl  9712  qnegcl  9713  qmulcl  9714  qreccl  9719  fzen  10121  uzsubsubfz  10125  fz01en  10131  fzmmmeqm  10136  fzsubel  10138  fztp  10156  fzsuc2  10157  fzrev2  10163  fzrev3  10165  elfzp1b  10175  fzrevral  10183  fzrevral2  10184  fzrevral3  10185  fzshftral  10186  fzoaddel2  10272  fzosubel2  10274  eluzgtdifelfzo  10276  fzocatel  10278  elfzom1elp1fzo  10281  fzval3  10283  zpnn0elfzo1  10287  fzosplitprm1  10313  fzoshftral  10317  flqzadd  10391  2tnp1ge0ge0  10394  ceilid  10410  intfracq  10415  zmod10  10435  modqmuladdnn0  10463  addmodlteq  10493  frecfzen2  10522  seqshft2g  10577  ser3mono  10582  m1expeven  10681  expsubap  10682  zesq  10753  sqoddm1div8  10788  bccmpl  10849  shftuz  10985  nnabscl  11268  climshftlemg  11470  climshft  11472  mptfzshft  11610  fsumrev  11611  fisum0diag2  11615  efexp  11850  efzval  11851  demoivre  11941  dvdsval2  11958  iddvds  11972  1dvds  11973  dvds0  11974  negdvdsb  11975  dvdsnegb  11976  0dvds  11979  dvdsmul1  11981  iddvdsexp  11983  muldvds1  11984  muldvds2  11985  dvdscmul  11986  dvdsmulc  11987  summodnegmod  11990  modmulconst  11991  dvds2ln  11992  dvds2add  11993  dvds2sub  11994  dvdstr  11996  dvdssub2  12003  dvdsadd  12004  dvdsaddr  12005  dvdssub  12006  dvdssubr  12007  dvdsadd2b  12008  dvdsabseq  12015  divconjdvds  12017  alzdvds  12022  addmodlteqALT  12027  zeo3  12036  odd2np1lem  12040  odd2np1  12041  even2n  12042  oddp1even  12044  mulsucdiv2z  12053  zob  12059  ltoddhalfle  12061  halfleoddlt  12062  opoe  12063  omoe  12064  opeo  12065  omeo  12066  m1exp1  12069  divalgb  12093  divalgmod  12095  modremain  12097  ndvdssub  12098  ndvdsadd  12099  flodddiv4  12104  flodddiv4t2lthalf  12107  bits0  12116  bitsp1e  12120  bitsp1o  12121  gcdneg  12160  gcdadd  12163  gcdid  12164  modgcd  12169  dvdsgcd  12190  mulgcd  12194  absmulgcd  12195  mulgcdr  12196  gcddiv  12197  gcdmultiplez  12199  dvdssqim  12202  dvdssq  12209  bezoutr1  12211  lcmneg  12253  lcmgcdlem  12256  lcmgcd  12257  lcmid  12259  lcm1  12260  coprmdvds  12271  coprmdvds2  12272  qredeq  12275  qredeu  12276  divgcdcoprmex  12281  cncongr1  12282  cncongr2  12283  prmdvdsexp  12327  rpexp1i  12333  sqrt2irr  12341  divnumden  12375  phiprmpw  12401  nnnn0modprm0  12435  modprmn0modprm0  12436  coprimeprodsq2  12438  pclemub  12467  pcprendvds2  12471  pcmul  12481  pcneg  12505  fldivp1  12528  prmpwdvds  12535  zgz  12553  4sqexercise1  12578  4sqexercise2  12579  modxai  12596  mulgz  13306  mulgassr  13316  mulgmodid  13317  gsumfzconst  13497  zsubrg  14163  zsssubrg  14167  zringmulg  14180  zringinvg  14186  mulgrhm2  14192  znunit  14241  ef2kpi  15068  efper  15069  sinperlem  15070  sin2kpi  15073  cos2kpi  15074  abssinper  15108  sinkpi  15109  coskpi  15110  cxpexprp  15157  sgmval2  15246  lgslem3  15269  lgsneg  15291  lgsdir2lem2  15296  lgsdir2lem4  15298  lgsdir2  15300  lgssq  15307  lgsmulsqcoprm  15313  lgsdirnn0  15314  gausslemma2dlem3  15330  lgsquadlem1  15344  lgsquadlem2  15345  lgsquad2  15350  2lgslem1a2  15354  2lgsoddprmlem1  15372  2lgsoddprmlem2  15373  2sqlem2  15382  2sqlem7  15388