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  11234  swrdswrd  11290  swrdpfx  11292  pfxccatin12lem4  11311  pfxccatin12lem1  11313  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12  11318  shftuz  11395  nnabscl  11678  climshftlemg  11880  climshft  11882  mptfzshft  12021  fsumrev  12022  fisum0diag2  12026  efexp  12261  efzval  12262  demoivre  12352  dvdsval2  12369  iddvds  12383  1dvds  12384  dvds0  12385  negdvdsb  12386  dvdsnegb  12387  0dvds  12390  dvdsmul1  12392  iddvdsexp  12394  muldvds1  12395  muldvds2  12396  dvdscmul  12397  dvdsmulc  12398  summodnegmod  12401  modmulconst  12402  dvds2ln  12403  dvds2add  12404  dvds2sub  12405  dvdstr  12407  dvdssub2  12414  dvdsadd  12415  dvdsaddr  12416  dvdssub  12417  dvdssubr  12418  dvdsadd2b  12419  dvdsabseq  12426  divconjdvds  12428  alzdvds  12433  addmodlteqALT  12438  zeo3  12447  odd2np1lem  12451  odd2np1  12452  even2n  12453  oddp1even  12455  mulsucdiv2z  12464  zob  12470  ltoddhalfle  12472  halfleoddlt  12473  opoe  12474  omoe  12475  opeo  12476  omeo  12477  m1exp1  12480  divalgb  12504  divalgmod  12506  modremain  12508  ndvdssub  12509  ndvdsadd  12510  flodddiv4  12515  flodddiv4t2lthalf  12518  bits0  12527  bitsp1e  12531  bitsp1o  12532  gcdneg  12571  gcdadd  12574  gcdid  12575  modgcd  12580  dvdsgcd  12601  mulgcd  12605  absmulgcd  12606  mulgcdr  12607  gcddiv  12608  gcdmultiplez  12610  dvdssqim  12613  dvdssq  12620  bezoutr1  12622  lcmneg  12664  lcmgcdlem  12667  lcmgcd  12668  lcmid  12670  lcm1  12671  coprmdvds  12682  coprmdvds2  12683  qredeq  12686  qredeu  12687  divgcdcoprmex  12692  cncongr1  12693  cncongr2  12694  prmdvdsexp  12738  rpexp1i  12744  sqrt2irr  12752  divnumden  12786  phiprmpw  12812  nnnn0modprm0  12846  modprmn0modprm0  12847  coprimeprodsq2  12849  pclemub  12878  pcprendvds2  12882  pcmul  12892  pcneg  12916  fldivp1  12939  prmpwdvds  12946  zgz  12964  4sqexercise1  12989  4sqexercise2  12990  modxai  13007  mulgz  13755  mulgassr  13765  mulgmodid  13766  gsumfzconst  13946  zsubrg  14614  zsssubrg  14618  zringmulg  14631  zringinvg  14637  mulgrhm2  14643  znunit  14692  ef2kpi  15549  efper  15550  sinperlem  15551  sin2kpi  15554  cos2kpi  15555  abssinper  15589  sinkpi  15590  coskpi  15591  cxpexprp  15638  sgmval2  15727  lgslem3  15750  lgsneg  15772  lgsdir2lem2  15777  lgsdir2lem4  15779  lgsdir2  15781  lgssq  15788  lgsmulsqcoprm  15794  lgsdirnn0  15795  gausslemma2dlem3  15811  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2  15831  2lgslem1a2  15835  2lgsoddprmlem1  15853  2lgsoddprmlem2  15854  2sqlem2  15863  2sqlem7  15869  wlk1walkdom  16229