Theorem zcn 9083

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

Syntax hints:   → wi 4   ∈ wcel 1481  ℂcc 7642  ℤcz 9078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-resscn 7736

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-rab 2426  df-v 2691  df-un 3080  df-in 3082  df-ss 3089  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139  df-ov 5785  df-neg 7960  df-z 9079

This theorem is referenced by:  zsscn  9086  zaddcllempos  9115  peano2zm  9116  zaddcllemneg  9117  zaddcl  9118  zsubcl  9119  zrevaddcl  9128  nzadd  9130  zlem1lt  9134  zltlem1  9135  zapne  9149  zdiv  9163  zdivadd  9164  zdivmul  9165  zextlt  9167  zneo  9176  zeo2  9181  peano5uzti  9183  zindd  9193  divfnzn  9440  qmulz  9442  zq  9445  qaddcl  9454  qnegcl  9455  qmulcl  9456  qreccl  9461  fzen  9854  uzsubsubfz  9858  fz01en  9864  fzmmmeqm  9869  fzsubel  9871  fztp  9889  fzsuc2  9890  fzrev2  9896  fzrev3  9898  elfzp1b  9908  fzrevral  9916  fzrevral2  9917  fzrevral3  9918  fzshftral  9919  fzoaddel2  10001  fzosubel2  10003  eluzgtdifelfzo  10005  fzocatel  10007  elfzom1elp1fzo  10010  fzval3  10012  zpnn0elfzo1  10016  fzosplitprm1  10042  fzoshftral  10046  flqzadd  10102  2tnp1ge0ge0  10105  ceilid  10119  intfracq  10124  zmod10  10144  modqmuladdnn0  10172  addmodlteq  10202  frecfzen2  10231  ser3mono  10282  m1expeven  10371  expsubap  10372  zesq  10441  sqoddm1div8  10475  bccmpl  10532  shftuz  10621  nnabscl  10904  climshftlemg  11103  climshft  11105  mptfzshft  11243  fsumrev  11244  fisum0diag2  11248  efexp  11425  efzval  11426  demoivre  11515  dvdsval2  11532  iddvds  11542  1dvds  11543  dvds0  11544  negdvdsb  11545  dvdsnegb  11546  0dvds  11549  dvdsmul1  11551  iddvdsexp  11553  muldvds1  11554  muldvds2  11555  dvdscmul  11556  dvdsmulc  11557  summodnegmod  11560  modmulconst  11561  dvds2ln  11562  dvds2add  11563  dvds2sub  11564  dvdstr  11566  dvdssub2  11571  dvdsadd  11572  dvdsaddr  11573  dvdssub  11574  dvdssubr  11575  dvdsadd2b  11576  dvdsabseq  11581  divconjdvds  11583  alzdvds  11588  addmodlteqALT  11593  zeo3  11601  odd2np1lem  11605  odd2np1  11606  even2n  11607  oddp1even  11609  mulsucdiv2z  11618  zob  11624  ltoddhalfle  11626  halfleoddlt  11627  opoe  11628  omoe  11629  opeo  11630  omeo  11631  m1exp1  11634  divalgb  11658  divalgmod  11660  modremain  11662  ndvdssub  11663  ndvdsadd  11664  flodddiv4  11667  flodddiv4t2lthalf  11670  gcdneg  11706  gcdadd  11709  gcdid  11710  modgcd  11715  dvdsgcd  11736  mulgcd  11740  absmulgcd  11741  mulgcdr  11742  gcddiv  11743  gcdmultiplez  11745  dvdssqim  11748  dvdssq  11755  bezoutr1  11757  lcmneg  11791  lcmgcdlem  11794  lcmgcd  11795  lcmid  11797  lcm1  11798  coprmdvds  11809  coprmdvds2  11810  qredeq  11813  qredeu  11814  divgcdcoprmex  11819  cncongr1  11820  cncongr2  11821  prmdvdsexp  11862  rpexp1i  11868  sqrt2irr  11876  divnumden  11910  phiprmpw  11934  ef2kpi  12935  efper  12936  sinperlem  12937  sin2kpi  12940  cos2kpi  12941  abssinper  12975  sinkpi  12976  coskpi  12977  cxpexprp  13024