Theorem zcn 8911

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

Syntax hints:   → wi 4   ∈ wcel 1448  ℂcc 7498  ℤcz 8906

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-resscn 7587

This theorem depends on definitions:  df-bi 116  df-3or 931  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-rex 2381  df-rab 2384  df-v 2643  df-un 3025  df-in 3027  df-ss 3034  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-br 3876  df-iota 5024  df-fv 5067  df-ov 5709  df-neg 7807  df-z 8907

This theorem is referenced by:  zsscn  8914  zaddcllempos  8943  peano2zm  8944  zaddcllemneg  8945  zaddcl  8946  zsubcl  8947  zrevaddcl  8956  nzadd  8958  zlem1lt  8962  zltlem1  8963  zapne  8977  zdiv  8991  zdivadd  8992  zdivmul  8993  zextlt  8995  zneo  9004  zeo2  9009  peano5uzti  9011  zindd  9021  divfnzn  9263  qmulz  9265  zq  9268  qaddcl  9277  qnegcl  9278  qmulcl  9279  qreccl  9284  fzen  9664  uzsubsubfz  9668  fz01en  9674  fzmmmeqm  9679  fzsubel  9681  fztp  9699  fzsuc2  9700  fzrev2  9706  fzrev3  9708  elfzp1b  9718  fzrevral  9726  fzrevral2  9727  fzrevral3  9728  fzshftral  9729  fzoaddel2  9811  fzosubel2  9813  eluzgtdifelfzo  9815  fzocatel  9817  elfzom1elp1fzo  9820  fzval3  9822  zpnn0elfzo1  9826  fzosplitprm1  9852  fzoshftral  9856  flqzadd  9912  2tnp1ge0ge0  9915  ceilid  9929  intfracq  9934  zmod10  9954  modqmuladdnn0  9982  addmodlteq  10012  frecfzen2  10041  ser3mono  10092  m1expeven  10181  expsubap  10182  zesq  10251  sqoddm1div8  10285  bccmpl  10341  shftuz  10430  nnabscl  10712  climshftlemg  10910  climshft  10912  mptfzshft  11050  fsumrev  11051  fisum0diag2  11055  efexp  11186  efzval  11187  demoivre  11276  dvdsval2  11291  iddvds  11301  1dvds  11302  dvds0  11303  negdvdsb  11304  dvdsnegb  11305  0dvds  11308  dvdsmul1  11310  iddvdsexp  11312  muldvds1  11313  muldvds2  11314  dvdscmul  11315  dvdsmulc  11316  summodnegmod  11319  modmulconst  11320  dvds2ln  11321  dvds2add  11322  dvds2sub  11323  dvdstr  11325  dvdssub2  11330  dvdsadd  11331  dvdsaddr  11332  dvdssub  11333  dvdssubr  11334  dvdsadd2b  11335  dvdsabseq  11340  divconjdvds  11342  alzdvds  11347  addmodlteqALT  11352  zeo3  11360  odd2np1lem  11364  odd2np1  11365  even2n  11366  oddp1even  11368  mulsucdiv2z  11377  zob  11383  ltoddhalfle  11385  halfleoddlt  11386  opoe  11387  omoe  11388  opeo  11389  omeo  11390  m1exp1  11393  divalgb  11417  divalgmod  11419  modremain  11421  ndvdssub  11422  ndvdsadd  11423  flodddiv4  11426  flodddiv4t2lthalf  11429  gcdneg  11465  gcdadd  11468  gcdid  11469  modgcd  11474  dvdsgcd  11493  mulgcd  11497  absmulgcd  11498  mulgcdr  11499  gcddiv  11500  gcdmultiplez  11502  dvdssqim  11505  dvdssq  11512  bezoutr1  11514  lcmneg  11548  lcmgcdlem  11551  lcmgcd  11552  lcmid  11554  lcm1  11555  coprmdvds  11566  coprmdvds2  11567  qredeq  11570  qredeu  11571  divgcdcoprmex  11576  cncongr1  11577  cncongr2  11578  prmdvdsexp  11619  rpexp1i  11625  sqrt2irr  11633  divnumden  11666  phiprmpw  11690