Theorem zcn 9484

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8030  ℤcz 9479

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8124

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-rab 2519  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021  df-neg 8353  df-z 9480

This theorem is referenced by:  zsscn  9487  zaddcllempos  9516  peano2zm  9517  zaddcllemneg  9518  zaddcl  9519  zsubcl  9520  zrevaddcl  9530  nzadd  9532  zlem1lt  9536  zltlem1  9537  zapne  9554  zdiv  9568  zdivadd  9569  zdivmul  9570  zextlt  9572  zneo  9581  zeo2  9586  peano5uzti  9588  zindd  9598  divfnzn  9855  qmulz  9857  zq  9860  qaddcl  9869  qnegcl  9870  qmulcl  9871  qreccl  9876  fzen  10278  uzsubsubfz  10282  fz01en  10288  fzmmmeqm  10293  fzsubel  10295  fztp  10313  fzsuc2  10314  fzrev2  10320  fzrev3  10322  elfzp1b  10332  fzrevral  10340  fzrevral2  10341  fzrevral3  10342  fzshftral  10343  fzo0addel  10434  fzo0addelr  10435  fzoaddel2  10436  fzosubel2  10441  eluzgtdifelfzo  10443  fzocatel  10445  elfzom1elp1fzo  10448  fzval3  10450  zpnn0elfzo1  10454  fzosplitprm1  10481  fzoshftral  10485  flqzadd  10559  2tnp1ge0ge0  10562  ceilid  10578  intfracq  10583  zmod10  10603  modqmuladdnn0  10631  addmodlteq  10661  frecfzen2  10690  seqshft2g  10745  ser3mono  10750  m1expeven  10849  expsubap  10850  zesq  10921  sqoddm1div8  10956  bccmpl  11017  swrd00g  11231  swrdswrd  11287  swrdpfx  11289  pfxccatin12lem4  11308  pfxccatin12lem1  11310  swrdccatin2  11311  pfxccatin12lem2  11313  pfxccatin12  11315  shftuz  11379  nnabscl  11662  climshftlemg  11864  climshft  11866  mptfzshft  12005  fsumrev  12006  fisum0diag2  12010  efexp  12245  efzval  12246  demoivre  12336  dvdsval2  12353  iddvds  12367  1dvds  12368  dvds0  12369  negdvdsb  12370  dvdsnegb  12371  0dvds  12374  dvdsmul1  12376  iddvdsexp  12378  muldvds1  12379  muldvds2  12380  dvdscmul  12381  dvdsmulc  12382  summodnegmod  12385  modmulconst  12386  dvds2ln  12387  dvds2add  12388  dvds2sub  12389  dvdstr  12391  dvdssub2  12398  dvdsadd  12399  dvdsaddr  12400  dvdssub  12401  dvdssubr  12402  dvdsadd2b  12403  dvdsabseq  12410  divconjdvds  12412  alzdvds  12417  addmodlteqALT  12422  zeo3  12431  odd2np1lem  12435  odd2np1  12436  even2n  12437  oddp1even  12439  mulsucdiv2z  12448  zob  12454  ltoddhalfle  12456  halfleoddlt  12457  opoe  12458  omoe  12459  opeo  12460  omeo  12461  m1exp1  12464  divalgb  12488  divalgmod  12490  modremain  12492  ndvdssub  12493  ndvdsadd  12494  flodddiv4  12499  flodddiv4t2lthalf  12502  bits0  12511  bitsp1e  12515  bitsp1o  12516  gcdneg  12555  gcdadd  12558  gcdid  12559  modgcd  12564  dvdsgcd  12585  mulgcd  12589  absmulgcd  12590  mulgcdr  12591  gcddiv  12592  gcdmultiplez  12594  dvdssqim  12597  dvdssq  12604  bezoutr1  12606  lcmneg  12648  lcmgcdlem  12651  lcmgcd  12652  lcmid  12654  lcm1  12655  coprmdvds  12666  coprmdvds2  12667  qredeq  12670  qredeu  12671  divgcdcoprmex  12676  cncongr1  12677  cncongr2  12678  prmdvdsexp  12722  rpexp1i  12728  sqrt2irr  12736  divnumden  12770  phiprmpw  12796  nnnn0modprm0  12830  modprmn0modprm0  12831  coprimeprodsq2  12833  pclemub  12862  pcprendvds2  12866  pcmul  12876  pcneg  12900  fldivp1  12923  prmpwdvds  12930  zgz  12948  4sqexercise1  12973  4sqexercise2  12974  modxai  12991  mulgz  13739  mulgassr  13749  mulgmodid  13750  gsumfzconst  13930  zsubrg  14598  zsssubrg  14602  zringmulg  14615  zringinvg  14621  mulgrhm2  14627  znunit  14676  ef2kpi  15533  efper  15534  sinperlem  15535  sin2kpi  15538  cos2kpi  15539  abssinper  15573  sinkpi  15574  coskpi  15575  cxpexprp  15622  sgmval2  15711  lgslem3  15734  lgsneg  15756  lgsdir2lem2  15761  lgsdir2lem4  15763  lgsdir2  15765  lgssq  15772  lgsmulsqcoprm  15778  lgsdirnn0  15779  gausslemma2dlem3  15795  lgsquadlem1  15809  lgsquadlem2  15810  lgsquad2  15815  2lgslem1a2  15819  2lgsoddprmlem1  15837  2lgsoddprmlem2  15838  2sqlem2  15847  2sqlem7  15853  wlk1walkdom  16213