Theorem zcn 9462

Description: An integer is a complex number. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
zcn	|- ( N e. ZZ -> N e. CC )

Proof of Theorem zcn

Step	Hyp	Ref	Expression
1		zre 9461	. 2 |- ( N e. ZZ -> N e. RR )
2	1	recnd 8186	1 |- ( N e. ZZ -> N e. CC )

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 8008   ZZcz 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  11197  swrdswrd  11253  swrdpfx  11255  pfxccatin12lem4  11274  pfxccatin12lem1  11276  swrdccatin2  11277  pfxccatin12lem2  11279  pfxccatin12  11281  shftuz  11344  nnabscl  11627  climshftlemg  11829  climshft  11831  mptfzshft  11969  fsumrev  11970  fisum0diag2  11974  efexp  12209  efzval  12210  demoivre  12300  dvdsval2  12317  iddvds  12331  1dvds  12332  dvds0  12333  negdvdsb  12334  dvdsnegb  12335  0dvds  12338  dvdsmul1  12340  iddvdsexp  12342  muldvds1  12343  muldvds2  12344  dvdscmul  12345  dvdsmulc  12346  summodnegmod  12349  modmulconst  12350  dvds2ln  12351  dvds2add  12352  dvds2sub  12353  dvdstr  12355  dvdssub2  12362  dvdsadd  12363  dvdsaddr  12364  dvdssub  12365  dvdssubr  12366  dvdsadd2b  12367  dvdsabseq  12374  divconjdvds  12376  alzdvds  12381  addmodlteqALT  12386  zeo3  12395  odd2np1lem  12399  odd2np1  12400  even2n  12401  oddp1even  12403  mulsucdiv2z  12412  zob  12418  ltoddhalfle  12420  halfleoddlt  12421  opoe  12422  omoe  12423  opeo  12424  omeo  12425  m1exp1  12428  divalgb  12452  divalgmod  12454  modremain  12456  ndvdssub  12457  ndvdsadd  12458  flodddiv4  12463  flodddiv4t2lthalf  12466  bits0  12475  bitsp1e  12479  bitsp1o  12480  gcdneg  12519  gcdadd  12522  gcdid  12523  modgcd  12528  dvdsgcd  12549  mulgcd  12553  absmulgcd  12554  mulgcdr  12555  gcddiv  12556  gcdmultiplez  12558  dvdssqim  12561  dvdssq  12568  bezoutr1  12570  lcmneg  12612  lcmgcdlem  12615  lcmgcd  12616  lcmid  12618  lcm1  12619  coprmdvds  12630  coprmdvds2  12631  qredeq  12634  qredeu  12635  divgcdcoprmex  12640  cncongr1  12641  cncongr2  12642  prmdvdsexp  12686  rpexp1i  12692  sqrt2irr  12700  divnumden  12734  phiprmpw  12760  nnnn0modprm0  12794  modprmn0modprm0  12795  coprimeprodsq2  12797  pclemub  12826  pcprendvds2  12830  pcmul  12840  pcneg  12864  fldivp1  12887  prmpwdvds  12894  zgz  12912  4sqexercise1  12937  4sqexercise2  12938  modxai  12955  mulgz  13703  mulgassr  13713  mulgmodid  13714  gsumfzconst  13894  zsubrg  14561  zsssubrg  14565  zringmulg  14578  zringinvg  14584  mulgrhm2  14590  znunit  14639  ef2kpi  15496  efper  15497  sinperlem  15498  sin2kpi  15501  cos2kpi  15502  abssinper  15536  sinkpi  15537  coskpi  15538  cxpexprp  15585  sgmval2  15674  lgslem3  15697  lgsneg  15719  lgsdir2lem2  15724  lgsdir2lem4  15726  lgsdir2  15728  lgssq  15735  lgsmulsqcoprm  15741  lgsdirnn0  15742  gausslemma2dlem3  15758  lgsquadlem1  15772  lgsquadlem2  15773  lgsquad2  15778  2lgslem1a2  15782  2lgsoddprmlem1  15800  2lgsoddprmlem2  15801  2sqlem2  15810  2sqlem7  15816  wlk1walkdom  16105