Theorem zcn 8356

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

Syntax hints:   -> wi 4   e. wcel 1433   CCcc 6979   ZZcz 8351

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-resscn 7068

This theorem depends on definitions:  df-bi 115  df-3or 920  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-rex 2354  df-rab 2357  df-v 2603  df-un 2977  df-in 2979  df-ss 2986  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-br 3786  df-iota 4887  df-fv 4930  df-ov 5535  df-neg 7282  df-z 8352

This theorem is referenced by:  zsscn  8359  zaddcllempos  8388  peano2zm  8389  zaddcllemneg  8390  zaddcl  8391  zsubcl  8392  zrevaddcl  8401  nzadd  8403  zlem1lt  8407  zltlem1  8408  zapne  8422  zdiv  8435  zdivadd  8436  zdivmul  8437  zextlt  8439  zneo  8448  zeo2  8453  peano5uzti  8455  zindd  8465  divfnzn  8706  qmulz  8708  zq  8711  qaddcl  8720  qnegcl  8721  qmulcl  8722  qreccl  8727  fzen  9062  uzsubsubfz  9066  fz01en  9072  fzmmmeqm  9076  fzsubel  9078  fztp  9095  fzsuc2  9096  fzrev2  9102  fzrev3  9104  elfzp1b  9114  fzrevral  9122  fzrevral2  9123  fzrevral3  9124  fzshftral  9125  fzoaddel2  9202  fzosubel2  9204  eluzgtdifelfzo  9206  fzocatel  9208  elfzom1elp1fzo  9211  fzval3  9213  zpnn0elfzo1  9217  fzosplitprm1  9243  fzoshftral  9247  flqzadd  9300  2tnp1ge0ge0  9303  ceilid  9317  intfracq  9322  zmod10  9342  modqmuladdnn0  9370  addmodlteq  9400  frecfzen2  9420  iseqshft2  9452  isermono  9457  m1expeven  9523  expsubap  9524  zesq  9591  sqoddm1div8  9625  bccmpl  9681  shftuz  9705  nnabscl  9986  climshftlemg  10141  climshft  10143  dvdsval2  10198  iddvds  10208  1dvds  10209  dvds0  10210  negdvdsb  10211  dvdsnegb  10212  0dvds  10215  dvdsmul1  10217  iddvdsexp  10219  muldvds1  10220  muldvds2  10221  dvdscmul  10222  dvdsmulc  10223  summodnegmod  10226  modmulconst  10227  dvds2ln  10228  dvds2add  10229  dvds2sub  10230  dvdstr  10232  dvdssub2  10237  dvdsadd  10238  dvdsaddr  10239  dvdssub  10240  dvdssubr  10241  dvdsadd2b  10242  dvdsabseq  10247  divconjdvds  10249  alzdvds  10254  addmodlteqALT  10259  zeo3  10267  odd2np1lem  10271  odd2np1  10272  even2n  10273  oddp1even  10275  mulsucdiv2z  10285  zob  10291  ltoddhalfle  10293  halfleoddlt  10294  opoe  10295  omoe  10296  opeo  10297  omeo  10298  m1exp1  10301  divalgb  10325  divalgmod  10327  modremain  10329  ndvdssub  10330  ndvdsadd  10331  flodddiv4  10334  flodddiv4t2lthalf  10337  gcdneg  10373  gcdadd  10376  gcdid  10377  modgcd  10382  dvdsgcd  10401  mulgcd  10405  absmulgcd  10406  mulgcdr  10407  gcddiv  10408  gcdmultiplez  10410  dvdssqim  10413  dvdssq  10420  bezoutr1  10422  lcmneg  10456  lcmgcdlem  10459  lcmgcd  10460  lcmid  10462  lcm1  10463  coprmdvds  10474  coprmdvds2  10475  qredeq  10478  qredeu  10479  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  prmdvdsexp  10527  rpexp1i  10533  sqrt2irr  10541