Theorem zcn 9451

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 9450	. 2 |- ( N e. ZZ -> N e. RR )
2	1	recnd 8175	1 |- ( N e. ZZ -> N e. CC )

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 7997   ZZcz 9446

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 8091

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 6004  df-neg 8320  df-z 9447

This theorem is referenced by:  zsscn  9454  zaddcllempos  9483  peano2zm  9484  zaddcllemneg  9485  zaddcl  9486  zsubcl  9487  zrevaddcl  9497  nzadd  9499  zlem1lt  9503  zltlem1  9504  zapne  9521  zdiv  9535  zdivadd  9536  zdivmul  9537  zextlt  9539  zneo  9548  zeo2  9553  peano5uzti  9555  zindd  9565  divfnzn  9816  qmulz  9818  zq  9821  qaddcl  9830  qnegcl  9831  qmulcl  9832  qreccl  9837  fzen  10239  uzsubsubfz  10243  fz01en  10249  fzmmmeqm  10254  fzsubel  10256  fztp  10274  fzsuc2  10275  fzrev2  10281  fzrev3  10283  elfzp1b  10293  fzrevral  10301  fzrevral2  10302  fzrevral3  10303  fzshftral  10304  fzo0addel  10394  fzo0addelr  10395  fzoaddel2  10396  fzosubel2  10401  eluzgtdifelfzo  10403  fzocatel  10405  elfzom1elp1fzo  10408  fzval3  10410  zpnn0elfzo1  10414  fzosplitprm1  10440  fzoshftral  10444  flqzadd  10518  2tnp1ge0ge0  10521  ceilid  10537  intfracq  10542  zmod10  10562  modqmuladdnn0  10590  addmodlteq  10620  frecfzen2  10649  seqshft2g  10704  ser3mono  10709  m1expeven  10808  expsubap  10809  zesq  10880  sqoddm1div8  10915  bccmpl  10976  swrd00g  11181  swrdswrd  11237  swrdpfx  11239  pfxccatin12lem4  11258  pfxccatin12lem1  11260  swrdccatin2  11261  pfxccatin12lem2  11263  pfxccatin12  11265  shftuz  11328  nnabscl  11611  climshftlemg  11813  climshft  11815  mptfzshft  11953  fsumrev  11954  fisum0diag2  11958  efexp  12193  efzval  12194  demoivre  12284  dvdsval2  12301  iddvds  12315  1dvds  12316  dvds0  12317  negdvdsb  12318  dvdsnegb  12319  0dvds  12322  dvdsmul1  12324  iddvdsexp  12326  muldvds1  12327  muldvds2  12328  dvdscmul  12329  dvdsmulc  12330  summodnegmod  12333  modmulconst  12334  dvds2ln  12335  dvds2add  12336  dvds2sub  12337  dvdstr  12339  dvdssub2  12346  dvdsadd  12347  dvdsaddr  12348  dvdssub  12349  dvdssubr  12350  dvdsadd2b  12351  dvdsabseq  12358  divconjdvds  12360  alzdvds  12365  addmodlteqALT  12370  zeo3  12379  odd2np1lem  12383  odd2np1  12384  even2n  12385  oddp1even  12387  mulsucdiv2z  12396  zob  12402  ltoddhalfle  12404  halfleoddlt  12405  opoe  12406  omoe  12407  opeo  12408  omeo  12409  m1exp1  12412  divalgb  12436  divalgmod  12438  modremain  12440  ndvdssub  12441  ndvdsadd  12442  flodddiv4  12447  flodddiv4t2lthalf  12450  bits0  12459  bitsp1e  12463  bitsp1o  12464  gcdneg  12503  gcdadd  12506  gcdid  12507  modgcd  12512  dvdsgcd  12533  mulgcd  12537  absmulgcd  12538  mulgcdr  12539  gcddiv  12540  gcdmultiplez  12542  dvdssqim  12545  dvdssq  12552  bezoutr1  12554  lcmneg  12596  lcmgcdlem  12599  lcmgcd  12600  lcmid  12602  lcm1  12603  coprmdvds  12614  coprmdvds2  12615  qredeq  12618  qredeu  12619  divgcdcoprmex  12624  cncongr1  12625  cncongr2  12626  prmdvdsexp  12670  rpexp1i  12676  sqrt2irr  12684  divnumden  12718  phiprmpw  12744  nnnn0modprm0  12778  modprmn0modprm0  12779  coprimeprodsq2  12781  pclemub  12810  pcprendvds2  12814  pcmul  12824  pcneg  12848  fldivp1  12871  prmpwdvds  12878  zgz  12896  4sqexercise1  12921  4sqexercise2  12922  modxai  12939  mulgz  13687  mulgassr  13697  mulgmodid  13698  gsumfzconst  13878  zsubrg  14545  zsssubrg  14549  zringmulg  14562  zringinvg  14568  mulgrhm2  14574  znunit  14623  ef2kpi  15480  efper  15481  sinperlem  15482  sin2kpi  15485  cos2kpi  15486  abssinper  15520  sinkpi  15521  coskpi  15522  cxpexprp  15569  sgmval2  15658  lgslem3  15681  lgsneg  15703  lgsdir2lem2  15708  lgsdir2lem4  15710  lgsdir2  15712  lgssq  15719  lgsmulsqcoprm  15725  lgsdirnn0  15726  gausslemma2dlem3  15742  lgsquadlem1  15756  lgsquadlem2  15757  lgsquad2  15762  2lgslem1a2  15766  2lgsoddprmlem1  15784  2lgsoddprmlem2  15785  2sqlem2  15794  2sqlem7  15800  wlk1walkdom  16070