Theorem zcn 9379

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

Syntax hints:   -> wi 4   e. wcel 2176   CCcc 7925   ZZcz 9374

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-resscn 8019

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-rab 2493  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280  df-ov 5949  df-neg 8248  df-z 9375

This theorem is referenced by:  zsscn  9382  zaddcllempos  9411  peano2zm  9412  zaddcllemneg  9413  zaddcl  9414  zsubcl  9415  zrevaddcl  9425  nzadd  9427  zlem1lt  9431  zltlem1  9432  zapne  9449  zdiv  9463  zdivadd  9464  zdivmul  9465  zextlt  9467  zneo  9476  zeo2  9481  peano5uzti  9483  zindd  9493  divfnzn  9744  qmulz  9746  zq  9749  qaddcl  9758  qnegcl  9759  qmulcl  9760  qreccl  9765  fzen  10167  uzsubsubfz  10171  fz01en  10177  fzmmmeqm  10182  fzsubel  10184  fztp  10202  fzsuc2  10203  fzrev2  10209  fzrev3  10211  elfzp1b  10221  fzrevral  10229  fzrevral2  10230  fzrevral3  10231  fzshftral  10232  fzo0addel  10319  fzo0addelr  10320  fzoaddel2  10321  fzosubel2  10326  eluzgtdifelfzo  10328  fzocatel  10330  elfzom1elp1fzo  10333  fzval3  10335  zpnn0elfzo1  10339  fzosplitprm1  10365  fzoshftral  10369  flqzadd  10443  2tnp1ge0ge0  10446  ceilid  10462  intfracq  10467  zmod10  10487  modqmuladdnn0  10515  addmodlteq  10545  frecfzen2  10574  seqshft2g  10629  ser3mono  10634  m1expeven  10733  expsubap  10734  zesq  10805  sqoddm1div8  10840  bccmpl  10901  swrd00g  11105  shftuz  11161  nnabscl  11444  climshftlemg  11646  climshft  11648  mptfzshft  11786  fsumrev  11787  fisum0diag2  11791  efexp  12026  efzval  12027  demoivre  12117  dvdsval2  12134  iddvds  12148  1dvds  12149  dvds0  12150  negdvdsb  12151  dvdsnegb  12152  0dvds  12155  dvdsmul1  12157  iddvdsexp  12159  muldvds1  12160  muldvds2  12161  dvdscmul  12162  dvdsmulc  12163  summodnegmod  12166  modmulconst  12167  dvds2ln  12168  dvds2add  12169  dvds2sub  12170  dvdstr  12172  dvdssub2  12179  dvdsadd  12180  dvdsaddr  12181  dvdssub  12182  dvdssubr  12183  dvdsadd2b  12184  dvdsabseq  12191  divconjdvds  12193  alzdvds  12198  addmodlteqALT  12203  zeo3  12212  odd2np1lem  12216  odd2np1  12217  even2n  12218  oddp1even  12220  mulsucdiv2z  12229  zob  12235  ltoddhalfle  12237  halfleoddlt  12238  opoe  12239  omoe  12240  opeo  12241  omeo  12242  m1exp1  12245  divalgb  12269  divalgmod  12271  modremain  12273  ndvdssub  12274  ndvdsadd  12275  flodddiv4  12280  flodddiv4t2lthalf  12283  bits0  12292  bitsp1e  12296  bitsp1o  12297  gcdneg  12336  gcdadd  12339  gcdid  12340  modgcd  12345  dvdsgcd  12366  mulgcd  12370  absmulgcd  12371  mulgcdr  12372  gcddiv  12373  gcdmultiplez  12375  dvdssqim  12378  dvdssq  12385  bezoutr1  12387  lcmneg  12429  lcmgcdlem  12432  lcmgcd  12433  lcmid  12435  lcm1  12436  coprmdvds  12447  coprmdvds2  12448  qredeq  12451  qredeu  12452  divgcdcoprmex  12457  cncongr1  12458  cncongr2  12459  prmdvdsexp  12503  rpexp1i  12509  sqrt2irr  12517  divnumden  12551  phiprmpw  12577  nnnn0modprm0  12611  modprmn0modprm0  12612  coprimeprodsq2  12614  pclemub  12643  pcprendvds2  12647  pcmul  12657  pcneg  12681  fldivp1  12704  prmpwdvds  12711  zgz  12729  4sqexercise1  12754  4sqexercise2  12755  modxai  12772  mulgz  13519  mulgassr  13529  mulgmodid  13530  gsumfzconst  13710  zsubrg  14376  zsssubrg  14380  zringmulg  14393  zringinvg  14399  mulgrhm2  14405  znunit  14454  ef2kpi  15311  efper  15312  sinperlem  15313  sin2kpi  15316  cos2kpi  15317  abssinper  15351  sinkpi  15352  coskpi  15353  cxpexprp  15400  sgmval2  15489  lgslem3  15512  lgsneg  15534  lgsdir2lem2  15539  lgsdir2lem4  15541  lgsdir2  15543  lgssq  15550  lgsmulsqcoprm  15556  lgsdirnn0  15557  gausslemma2dlem3  15573  lgsquadlem1  15587  lgsquadlem2  15588  lgsquad2  15593  2lgslem1a2  15597  2lgsoddprmlem1  15615  2lgsoddprmlem2  15616  2sqlem2  15625  2sqlem7  15631