Theorem zcn 9288

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

Syntax hints:   → wi 4   ∈ wcel 2160  ℂcc 7839  ℤcz 9283

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-resscn 7933

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-rab 2477  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-iota 5196  df-fv 5243  df-ov 5899  df-neg 8161  df-z 9284

This theorem is referenced by:  zsscn  9291  zaddcllempos  9320  peano2zm  9321  zaddcllemneg  9322  zaddcl  9323  zsubcl  9324  zrevaddcl  9333  nzadd  9335  zlem1lt  9339  zltlem1  9340  zapne  9357  zdiv  9371  zdivadd  9372  zdivmul  9373  zextlt  9375  zneo  9384  zeo2  9389  peano5uzti  9391  zindd  9401  divfnzn  9651  qmulz  9653  zq  9656  qaddcl  9665  qnegcl  9666  qmulcl  9667  qreccl  9672  fzen  10073  uzsubsubfz  10077  fz01en  10083  fzmmmeqm  10088  fzsubel  10090  fztp  10108  fzsuc2  10109  fzrev2  10115  fzrev3  10117  elfzp1b  10127  fzrevral  10135  fzrevral2  10136  fzrevral3  10137  fzshftral  10138  fzoaddel2  10223  fzosubel2  10225  eluzgtdifelfzo  10227  fzocatel  10229  elfzom1elp1fzo  10232  fzval3  10234  zpnn0elfzo1  10238  fzosplitprm1  10264  fzoshftral  10268  flqzadd  10329  2tnp1ge0ge0  10332  ceilid  10346  intfracq  10351  zmod10  10371  modqmuladdnn0  10399  addmodlteq  10429  frecfzen2  10458  ser3mono  10509  m1expeven  10598  expsubap  10599  zesq  10670  sqoddm1div8  10705  bccmpl  10766  shftuz  10858  nnabscl  11141  climshftlemg  11342  climshft  11344  mptfzshft  11482  fsumrev  11483  fisum0diag2  11487  efexp  11722  efzval  11723  demoivre  11812  dvdsval2  11829  iddvds  11843  1dvds  11844  dvds0  11845  negdvdsb  11846  dvdsnegb  11847  0dvds  11850  dvdsmul1  11852  iddvdsexp  11854  muldvds1  11855  muldvds2  11856  dvdscmul  11857  dvdsmulc  11858  summodnegmod  11861  modmulconst  11862  dvds2ln  11863  dvds2add  11864  dvds2sub  11865  dvdstr  11867  dvdssub2  11874  dvdsadd  11875  dvdsaddr  11876  dvdssub  11877  dvdssubr  11878  dvdsadd2b  11879  dvdsabseq  11885  divconjdvds  11887  alzdvds  11892  addmodlteqALT  11897  zeo3  11905  odd2np1lem  11909  odd2np1  11910  even2n  11911  oddp1even  11913  mulsucdiv2z  11922  zob  11928  ltoddhalfle  11930  halfleoddlt  11931  opoe  11932  omoe  11933  opeo  11934  omeo  11935  m1exp1  11938  divalgb  11962  divalgmod  11964  modremain  11966  ndvdssub  11967  ndvdsadd  11968  flodddiv4  11971  flodddiv4t2lthalf  11974  gcdneg  12015  gcdadd  12018  gcdid  12019  modgcd  12024  dvdsgcd  12045  mulgcd  12049  absmulgcd  12050  mulgcdr  12051  gcddiv  12052  gcdmultiplez  12054  dvdssqim  12057  dvdssq  12064  bezoutr1  12066  lcmneg  12106  lcmgcdlem  12109  lcmgcd  12110  lcmid  12112  lcm1  12113  coprmdvds  12124  coprmdvds2  12125  qredeq  12128  qredeu  12129  divgcdcoprmex  12134  cncongr1  12135  cncongr2  12136  prmdvdsexp  12180  rpexp1i  12186  sqrt2irr  12194  divnumden  12228  phiprmpw  12254  nnnn0modprm0  12287  modprmn0modprm0  12288  coprimeprodsq2  12290  pclemub  12319  pcprendvds2  12323  pcmul  12333  pcneg  12357  fldivp1  12380  prmpwdvds  12387  zgz  12405  4sqexercise1  12430  4sqexercise2  12431  mulgz  13090  mulgassr  13100  mulgmodid  13101  zsubrg  13884  zsssubrg  13888  zringmulg  13897  zringinvg  13903  mulgrhm2  13908  ef2kpi  14684  efper  14685  sinperlem  14686  sin2kpi  14689  cos2kpi  14690  abssinper  14724  sinkpi  14725  coskpi  14726  cxpexprp  14773  lgslem3  14861  lgsneg  14883  lgsdir2lem2  14888  lgsdir2lem4  14890  lgsdir2  14892  lgssq  14899  lgsmulsqcoprm  14905  lgsdirnn0  14906  2lgsoddprmlem1  14911  2lgsoddprmlem2  14912  2sqlem2  14920  2sqlem7  14926