Theorem zcn 9462

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8008  ℤcz 9457

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8102

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-rab 2517  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010  df-neg 8331  df-z 9458

This theorem is referenced by:  zsscn  9465  zaddcllempos  9494  peano2zm  9495  zaddcllemneg  9496  zaddcl  9497  zsubcl  9498  zrevaddcl  9508  nzadd  9510  zlem1lt  9514  zltlem1  9515  zapne  9532  zdiv  9546  zdivadd  9547  zdivmul  9548  zextlt  9550  zneo  9559  zeo2  9564  peano5uzti  9566  zindd  9576  divfnzn  9828  qmulz  9830  zq  9833  qaddcl  9842  qnegcl  9843  qmulcl  9844  qreccl  9849  fzen  10251  uzsubsubfz  10255  fz01en  10261  fzmmmeqm  10266  fzsubel  10268  fztp  10286  fzsuc2  10287  fzrev2  10293  fzrev3  10295  elfzp1b  10305  fzrevral  10313  fzrevral2  10314  fzrevral3  10315  fzshftral  10316  fzo0addel  10406  fzo0addelr  10407  fzoaddel2  10408  fzosubel2  10413  eluzgtdifelfzo  10415  fzocatel  10417  elfzom1elp1fzo  10420  fzval3  10422  zpnn0elfzo1  10426  fzosplitprm1  10452  fzoshftral  10456  flqzadd  10530  2tnp1ge0ge0  10533  ceilid  10549  intfracq  10554  zmod10  10574  modqmuladdnn0  10602  addmodlteq  10632  frecfzen2  10661  seqshft2g  10716  ser3mono  10721  m1expeven  10820  expsubap  10821  zesq  10892  sqoddm1div8  10927  bccmpl  10988  swrd00g  11196  swrdswrd  11252  swrdpfx  11254  pfxccatin12lem4  11273  pfxccatin12lem1  11275  swrdccatin2  11276  pfxccatin12lem2  11278  pfxccatin12  11280  shftuz  11343  nnabscl  11626  climshftlemg  11828  climshft  11830  mptfzshft  11968  fsumrev  11969  fisum0diag2  11973  efexp  12208  efzval  12209  demoivre  12299  dvdsval2  12316  iddvds  12330  1dvds  12331  dvds0  12332  negdvdsb  12333  dvdsnegb  12334  0dvds  12337  dvdsmul1  12339  iddvdsexp  12341  muldvds1  12342  muldvds2  12343  dvdscmul  12344  dvdsmulc  12345  summodnegmod  12348  modmulconst  12349  dvds2ln  12350  dvds2add  12351  dvds2sub  12352  dvdstr  12354  dvdssub2  12361  dvdsadd  12362  dvdsaddr  12363  dvdssub  12364  dvdssubr  12365  dvdsadd2b  12366  dvdsabseq  12373  divconjdvds  12375  alzdvds  12380  addmodlteqALT  12385  zeo3  12394  odd2np1lem  12398  odd2np1  12399  even2n  12400  oddp1even  12402  mulsucdiv2z  12411  zob  12417  ltoddhalfle  12419  halfleoddlt  12420  opoe  12421  omoe  12422  opeo  12423  omeo  12424  m1exp1  12427  divalgb  12451  divalgmod  12453  modremain  12455  ndvdssub  12456  ndvdsadd  12457  flodddiv4  12462  flodddiv4t2lthalf  12465  bits0  12474  bitsp1e  12478  bitsp1o  12479  gcdneg  12518  gcdadd  12521  gcdid  12522  modgcd  12527  dvdsgcd  12548  mulgcd  12552  absmulgcd  12553  mulgcdr  12554  gcddiv  12555  gcdmultiplez  12557  dvdssqim  12560  dvdssq  12567  bezoutr1  12569  lcmneg  12611  lcmgcdlem  12614  lcmgcd  12615  lcmid  12617  lcm1  12618  coprmdvds  12629  coprmdvds2  12630  qredeq  12633  qredeu  12634  divgcdcoprmex  12639  cncongr1  12640  cncongr2  12641  prmdvdsexp  12685  rpexp1i  12691  sqrt2irr  12699  divnumden  12733  phiprmpw  12759  nnnn0modprm0  12793  modprmn0modprm0  12794  coprimeprodsq2  12796  pclemub  12825  pcprendvds2  12829  pcmul  12839  pcneg  12863  fldivp1  12886  prmpwdvds  12893  zgz  12911  4sqexercise1  12936  4sqexercise2  12937  modxai  12954  mulgz  13702  mulgassr  13712  mulgmodid  13713  gsumfzconst  13893  zsubrg  14560  zsssubrg  14564  zringmulg  14577  zringinvg  14583  mulgrhm2  14589  znunit  14638  ef2kpi  15495  efper  15496  sinperlem  15497  sin2kpi  15500  cos2kpi  15501  abssinper  15535  sinkpi  15536  coskpi  15537  cxpexprp  15584  sgmval2  15673  lgslem3  15696  lgsneg  15718  lgsdir2lem2  15723  lgsdir2lem4  15725  lgsdir2  15727  lgssq  15734  lgsmulsqcoprm  15740  lgsdirnn0  15741  gausslemma2dlem3  15757  lgsquadlem1  15771  lgsquadlem2  15772  lgsquad2  15777  2lgslem1a2  15781  2lgsoddprmlem1  15799  2lgsoddprmlem2  15800  2sqlem2  15809  2sqlem7  15815  wlk1walkdom  16100