Theorem zcn 9654

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℂcc 8178  ℤcz 9649

This proof depends on 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 8272

This proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088  df-neg 8502  df-z 9650

This theorem is used by:  zsscn  9657  zaddcllempos  9686  peano2zm  9687  zaddcllemneg  9688  zaddcl  9689  zsubcl  9690  zrevaddcl  9700  nzadd  9702  zlem1lt  9706  zltlem1  9707  zapne  9724  zdiv  9739  zdivadd  9740  zdivmul  9741  zextlt  9743  zneo  9752  zeo2  9757  peano5uzti  9759  zindd  9769  divfnzn  10031  qmulz  10033  zq  10036  qaddcl  10045  qnegcl  10046  qmulcl  10047  qreccl  10052  fzen  10458  uzsubsubfz  10463  fz01en  10470  fzmmmeqm  10475  fzsubel  10477  fztp  10496  fzsuc2  10497  fzrev2  10503  fzrev3  10505  elfzp1b  10515  fzrevral  10523  fzrevral2  10524  fzrevral3  10525  fzshftral  10526  fzo0addel  10617  fzo0addelr  10618  fzoaddel2  10619  fzosubel2  10624  eluzgtdifelfzo  10626  fzocatel  10628  elfzom1elp1fzo  10631  fzval3  10633  zpnn0elfzo1  10637  fzosplitprm1  10664  fzoshftral  10668  flqzadd  10748  2tnp1ge0ge0  10751  ceilid  10767  intfracq  10772  zmod10  10792  modqmuladdnn0  10820  addmodlteq  10850  frecfzen2  10879  seqshft2g  10934  ser3mono  10939  m1expeven  11038  expsubap  11039  zesq  11111  sqoddm1div8  11146  bccmpl  11208  swrd00g  11437  swrdswrd  11493  swrdpfx  11495  pfxccatin12lem4  11514  pfxccatin12lem1  11516  swrdccatin2  11517  pfxccatin12lem2  11519  pfxccatin12  11521  shftuz  11598  nnabscl  11883  climshftlemg  12087  climshft  12089  mptfzshft  12228  fsumrev  12229  fisum0diag2  12233  efexp  12468  efzval  12469  demoivre  12559  dvdsval2  12576  iddvds  12590  1dvds  12591  dvds0  12592  negdvdsb  12593  dvdsnegb  12594  0dvds  12597  dvdsmul1  12599  iddvdsexp  12601  muldvds1  12602  muldvds2  12603  dvdscmul  12604  dvdsmulc  12605  summodnegmod  12608  modmulconst  12609  dvds2ln  12610  dvds2add  12611  dvds2sub  12612  dvdstr  12614  dvdssub2  12621  dvdsadd  12622  dvdsaddr  12623  dvdssub  12624  dvdssubr  12625  dvdsadd2b  12626  dvdsabseq  12633  divconjdvds  12635  alzdvds  12640  addmodlteqALT  12645  zeo3  12654  odd2np1lem  12658  odd2np1  12659  even2n  12660  oddp1even  12662  mulsucdiv2z  12671  zob  12677  ltoddhalfle  12679  halfleoddlt  12680  opoe  12681  omoe  12682  opeo  12683  omeo  12684  m1exp1  12687  divalgb  12711  divalgmod  12713  modremain  12715  ndvdssub  12716  ndvdsadd  12717  flodddiv4  12722  flodddiv4t2lthalf  12725  bits0  12734  bitsp1e  12738  bitsp1o  12739  gcdneg  12778  gcdadd  12781  gcdid  12782  modgcd  12787  dvdsgcd  12808  mulgcd  12812  absmulgcd  12813  mulgcdr  12814  gcddiv  12815  gcdmultiplez  12817  dvdssqim  12820  dvdssq  12827  bezoutr1  12829  lcmneg  12871  lcmgcdlem  12874  lcmgcd  12875  lcmid  12877  lcm1  12878  coprmdvds  12889  coprmdvds2  12890  qredeq  12893  qredeu  12894  divgcdcoprmex  12899  cncongr1  12900  cncongr2  12901  prmdvdsexp  12946  rpexp1i  12952  sqrt2irr  12960  divnumden  12995  phiprmpw  13023  nnnn0modprm0  13057  modprmn0modprm0  13058  coprimeprodsq2  13060  pclemub  13089  pcprendvds2  13093  pcmul  13103  pcneg  13127  fldivp1  13150  prmpwdvds  13157  zgz  13175  4sqexercise1  13200  4sqexercise2  13201  modxai  13218  mod2xnegi  13221  mulgz  14006  mulgassr  14016  mulgmodid  14017  gzsumconst  14227  zsubrg  15002  zsssubrg  15006  zringmulg  15017  zringinvg  15023  mulgrhm2  15029  znunit  15078  ef2kpi  15999  efper  16000  sinperlem  16001  sin2kpi  16004  cos2kpi  16005  abssinper  16039  sinkpi  16040  coskpi  16041  cxpexprp  16092  sgmval2  16214  ppiprm  16220  ppinprm  16221  chtprm  16222  chtnprm  16223  lgslem3  16287  lgsneg  16309  lgsdir2lem2  16314  lgsdir2lem4  16316  lgsdir2  16318  lgssq  16325  lgsmulsqcoprm  16331  lgsdirnn0  16332  gausslemma2dlem3  16348  lgsquadlem1  16362  lgsquadlem2  16363  lgsquad2  16368  2lgslem1a2  16372  2lgsoddprmlem1  16390  2lgsoddprmlem2  16391  2sqlem2  16400  2sqlem7  16406  wlk1walkdom  16766