Theorem zcn 9628

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

Syntax hints:   → wi 4   ∈ wcel 2209  ℂcc 8167  ℤcz 9623

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8261

This theorem depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-rab 2537  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380  df-ov 6078  df-neg 8490  df-z 9624

This theorem is referenced by:  zsscn  9631  zaddcllempos  9660  peano2zm  9661  zaddcllemneg  9662  zaddcl  9663  zsubcl  9664  zrevaddcl  9674  nzadd  9676  zlem1lt  9680  zltlem1  9681  zapne  9698  zdiv  9713  zdivadd  9714  zdivmul  9715  zextlt  9717  zneo  9726  zeo2  9731  peano5uzti  9733  zindd  9743  divfnzn  10000  qmulz  10002  zq  10005  qaddcl  10014  qnegcl  10015  qmulcl  10016  qreccl  10021  fzen  10426  uzsubsubfz  10430  fz01en  10437  fzmmmeqm  10442  fzsubel  10444  fztp  10463  fzsuc2  10464  fzrev2  10470  fzrev3  10472  elfzp1b  10482  fzrevral  10490  fzrevral2  10491  fzrevral3  10492  fzshftral  10493  fzo0addel  10584  fzo0addelr  10585  fzoaddel2  10586  fzosubel2  10591  eluzgtdifelfzo  10593  fzocatel  10595  elfzom1elp1fzo  10598  fzval3  10600  zpnn0elfzo1  10604  fzosplitprm1  10631  fzoshftral  10635  flqzadd  10711  2tnp1ge0ge0  10714  ceilid  10730  intfracq  10735  zmod10  10755  modqmuladdnn0  10783  addmodlteq  10813  frecfzen2  10842  seqshft2g  10897  ser3mono  10902  m1expeven  11001  expsubap  11002  zesq  11074  sqoddm1div8  11109  bccmpl  11170  swrd00g  11399  swrdswrd  11455  swrdpfx  11457  pfxccatin12lem4  11476  pfxccatin12lem1  11478  swrdccatin2  11479  pfxccatin12lem2  11481  pfxccatin12  11483  shftuz  11560  nnabscl  11844  climshftlemg  12046  climshft  12048  mptfzshft  12187  fsumrev  12188  fisum0diag2  12192  efexp  12427  efzval  12428  demoivre  12518  dvdsval2  12535  iddvds  12549  1dvds  12550  dvds0  12551  negdvdsb  12552  dvdsnegb  12553  0dvds  12556  dvdsmul1  12558  iddvdsexp  12560  muldvds1  12561  muldvds2  12562  dvdscmul  12563  dvdsmulc  12564  summodnegmod  12567  modmulconst  12568  dvds2ln  12569  dvds2add  12570  dvds2sub  12571  dvdstr  12573  dvdssub2  12580  dvdsadd  12581  dvdsaddr  12582  dvdssub  12583  dvdssubr  12584  dvdsadd2b  12585  dvdsabseq  12592  divconjdvds  12594  alzdvds  12599  addmodlteqALT  12604  zeo3  12613  odd2np1lem  12617  odd2np1  12618  even2n  12619  oddp1even  12621  mulsucdiv2z  12630  zob  12636  ltoddhalfle  12638  halfleoddlt  12639  opoe  12640  omoe  12641  opeo  12642  omeo  12643  m1exp1  12646  divalgb  12670  divalgmod  12672  modremain  12674  ndvdssub  12675  ndvdsadd  12676  flodddiv4  12681  flodddiv4t2lthalf  12684  bits0  12693  bitsp1e  12697  bitsp1o  12698  gcdneg  12737  gcdadd  12740  gcdid  12741  modgcd  12746  dvdsgcd  12767  mulgcd  12771  absmulgcd  12772  mulgcdr  12773  gcddiv  12774  gcdmultiplez  12776  dvdssqim  12779  dvdssq  12786  bezoutr1  12788  lcmneg  12830  lcmgcdlem  12833  lcmgcd  12834  lcmid  12836  lcm1  12837  coprmdvds  12848  coprmdvds2  12849  qredeq  12852  qredeu  12853  divgcdcoprmex  12858  cncongr1  12859  cncongr2  12860  prmdvdsexp  12904  rpexp1i  12910  sqrt2irr  12918  divnumden  12952  phiprmpw  12978  nnnn0modprm0  13012  modprmn0modprm0  13013  coprimeprodsq2  13015  pclemub  13044  pcprendvds2  13048  pcmul  13058  pcneg  13082  fldivp1  13105  prmpwdvds  13112  zgz  13130  4sqexercise1  13155  4sqexercise2  13156  modxai  13173  mulgz  13930  mulgassr  13940  mulgmodid  13941  gzsumconst  14120  zsubrg  14890  zsssubrg  14894  zringmulg  14905  zringinvg  14911  mulgrhm2  14917  znunit  14966  ef2kpi  15830  efper  15831  sinperlem  15832  sin2kpi  15835  cos2kpi  15836  abssinper  15870  sinkpi  15871  coskpi  15872  cxpexprp  15920  sgmval2  16012  lgslem3  16035  lgsneg  16057  lgsdir2lem2  16062  lgsdir2lem4  16064  lgsdir2  16066  lgssq  16073  lgsmulsqcoprm  16079  lgsdirnn0  16080  gausslemma2dlem3  16096  lgsquadlem1  16110  lgsquadlem2  16111  lgsquad2  16116  2lgslem1a2  16120  2lgsoddprmlem1  16138  2lgsoddprmlem2  16139  2sqlem2  16148  2sqlem7  16154  wlk1walkdom  16514