Theorem zcn 9649

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

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

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 8271

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 8500  df-z 9645

This theorem is used by:  zsscn  9652  zaddcllempos  9681  peano2zm  9682  zaddcllemneg  9683  zaddcl  9684  zsubcl  9685  zrevaddcl  9695  nzadd  9697  zlem1lt  9701  zltlem1  9702  zapne  9719  zdiv  9734  zdivadd  9735  zdivmul  9736  zextlt  9738  zneo  9747  zeo2  9752  peano5uzti  9754  zindd  9764  divfnzn  10021  qmulz  10023  zq  10026  qaddcl  10035  qnegcl  10036  qmulcl  10037  qreccl  10042  fzen  10447  uzsubsubfz  10452  fz01en  10459  fzmmmeqm  10464  fzsubel  10466  fztp  10485  fzsuc2  10486  fzrev2  10492  fzrev3  10494  elfzp1b  10504  fzrevral  10512  fzrevral2  10513  fzrevral3  10514  fzshftral  10515  fzo0addel  10606  fzo0addelr  10607  fzoaddel2  10608  fzosubel2  10613  eluzgtdifelfzo  10615  fzocatel  10617  elfzom1elp1fzo  10620  fzval3  10622  zpnn0elfzo1  10626  fzosplitprm1  10653  fzoshftral  10657  flqzadd  10733  2tnp1ge0ge0  10736  ceilid  10752  intfracq  10757  zmod10  10777  modqmuladdnn0  10805  addmodlteq  10835  frecfzen2  10864  seqshft2g  10919  ser3mono  10924  m1expeven  11023  expsubap  11024  zesq  11096  sqoddm1div8  11131  bccmpl  11192  swrd00g  11421  swrdswrd  11477  swrdpfx  11479  pfxccatin12lem4  11498  pfxccatin12lem1  11500  swrdccatin2  11501  pfxccatin12lem2  11503  pfxccatin12  11505  shftuz  11582  nnabscl  11866  climshftlemg  12068  climshft  12070  mptfzshft  12209  fsumrev  12210  fisum0diag2  12214  efexp  12449  efzval  12450  demoivre  12540  dvdsval2  12557  iddvds  12571  1dvds  12572  dvds0  12573  negdvdsb  12574  dvdsnegb  12575  0dvds  12578  dvdsmul1  12580  iddvdsexp  12582  muldvds1  12583  muldvds2  12584  dvdscmul  12585  dvdsmulc  12586  summodnegmod  12589  modmulconst  12590  dvds2ln  12591  dvds2add  12592  dvds2sub  12593  dvdstr  12595  dvdssub2  12602  dvdsadd  12603  dvdsaddr  12604  dvdssub  12605  dvdssubr  12606  dvdsadd2b  12607  dvdsabseq  12614  divconjdvds  12616  alzdvds  12621  addmodlteqALT  12626  zeo3  12635  odd2np1lem  12639  odd2np1  12640  even2n  12641  oddp1even  12643  mulsucdiv2z  12652  zob  12658  ltoddhalfle  12660  halfleoddlt  12661  opoe  12662  omoe  12663  opeo  12664  omeo  12665  m1exp1  12668  divalgb  12692  divalgmod  12694  modremain  12696  ndvdssub  12697  ndvdsadd  12698  flodddiv4  12703  flodddiv4t2lthalf  12706  bits0  12715  bitsp1e  12719  bitsp1o  12720  gcdneg  12759  gcdadd  12762  gcdid  12763  modgcd  12768  dvdsgcd  12789  mulgcd  12793  absmulgcd  12794  mulgcdr  12795  gcddiv  12796  gcdmultiplez  12798  dvdssqim  12801  dvdssq  12808  bezoutr1  12810  lcmneg  12852  lcmgcdlem  12855  lcmgcd  12856  lcmid  12858  lcm1  12859  coprmdvds  12870  coprmdvds2  12871  qredeq  12874  qredeu  12875  divgcdcoprmex  12880  cncongr1  12881  cncongr2  12882  prmdvdsexp  12926  rpexp1i  12932  sqrt2irr  12940  divnumden  12974  phiprmpw  13000  nnnn0modprm0  13034  modprmn0modprm0  13035  coprimeprodsq2  13037  pclemub  13066  pcprendvds2  13070  pcmul  13080  pcneg  13104  fldivp1  13127  prmpwdvds  13134  zgz  13152  4sqexercise1  13177  4sqexercise2  13178  modxai  13195  mulgz  13953  mulgassr  13963  mulgmodid  13964  gzsumconst  14143  zsubrg  14918  zsssubrg  14922  zringmulg  14933  zringinvg  14939  mulgrhm2  14945  znunit  14994  ef2kpi  15907  efper  15908  sinperlem  15909  sin2kpi  15912  cos2kpi  15913  abssinper  15947  sinkpi  15948  coskpi  15949  cxpexprp  15997  sgmval2  16098  lgslem3  16121  lgsneg  16143  lgsdir2lem2  16148  lgsdir2lem4  16150  lgsdir2  16152  lgssq  16159  lgsmulsqcoprm  16165  lgsdirnn0  16166  gausslemma2dlem3  16182  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2  16202  2lgslem1a2  16206  2lgsoddprmlem1  16224  2lgsoddprmlem2  16225  2sqlem2  16234  2sqlem7  16240  wlk1walkdom  16600