Theorem zcn 9257

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

Syntax hints:   -> wi 4   e. wcel 2148   CCcc 7808   ZZcz 9252

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7902

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-rab 2464  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877  df-neg 8130  df-z 9253

This theorem is referenced by:  zsscn  9260  zaddcllempos  9289  peano2zm  9290  zaddcllemneg  9291  zaddcl  9292  zsubcl  9293  zrevaddcl  9302  nzadd  9304  zlem1lt  9308  zltlem1  9309  zapne  9326  zdiv  9340  zdivadd  9341  zdivmul  9342  zextlt  9344  zneo  9353  zeo2  9358  peano5uzti  9360  zindd  9370  divfnzn  9620  qmulz  9622  zq  9625  qaddcl  9634  qnegcl  9635  qmulcl  9636  qreccl  9641  fzen  10042  uzsubsubfz  10046  fz01en  10052  fzmmmeqm  10057  fzsubel  10059  fztp  10077  fzsuc2  10078  fzrev2  10084  fzrev3  10086  elfzp1b  10096  fzrevral  10104  fzrevral2  10105  fzrevral3  10106  fzshftral  10107  fzoaddel2  10192  fzosubel2  10194  eluzgtdifelfzo  10196  fzocatel  10198  elfzom1elp1fzo  10201  fzval3  10203  zpnn0elfzo1  10207  fzosplitprm1  10233  fzoshftral  10237  flqzadd  10297  2tnp1ge0ge0  10300  ceilid  10314  intfracq  10319  zmod10  10339  modqmuladdnn0  10367  addmodlteq  10397  frecfzen2  10426  ser3mono  10477  m1expeven  10566  expsubap  10567  zesq  10638  sqoddm1div8  10673  bccmpl  10733  shftuz  10825  nnabscl  11108  climshftlemg  11309  climshft  11311  mptfzshft  11449  fsumrev  11450  fisum0diag2  11454  efexp  11689  efzval  11690  demoivre  11779  dvdsval2  11796  iddvds  11810  1dvds  11811  dvds0  11812  negdvdsb  11813  dvdsnegb  11814  0dvds  11817  dvdsmul1  11819  iddvdsexp  11821  muldvds1  11822  muldvds2  11823  dvdscmul  11824  dvdsmulc  11825  summodnegmod  11828  modmulconst  11829  dvds2ln  11830  dvds2add  11831  dvds2sub  11832  dvdstr  11834  dvdssub2  11841  dvdsadd  11842  dvdsaddr  11843  dvdssub  11844  dvdssubr  11845  dvdsadd2b  11846  dvdsabseq  11852  divconjdvds  11854  alzdvds  11859  addmodlteqALT  11864  zeo3  11872  odd2np1lem  11876  odd2np1  11877  even2n  11878  oddp1even  11880  mulsucdiv2z  11889  zob  11895  ltoddhalfle  11897  halfleoddlt  11898  opoe  11899  omoe  11900  opeo  11901  omeo  11902  m1exp1  11905  divalgb  11929  divalgmod  11931  modremain  11933  ndvdssub  11934  ndvdsadd  11935  flodddiv4  11938  flodddiv4t2lthalf  11941  gcdneg  11982  gcdadd  11985  gcdid  11986  modgcd  11991  dvdsgcd  12012  mulgcd  12016  absmulgcd  12017  mulgcdr  12018  gcddiv  12019  gcdmultiplez  12021  dvdssqim  12024  dvdssq  12031  bezoutr1  12033  lcmneg  12073  lcmgcdlem  12076  lcmgcd  12077  lcmid  12079  lcm1  12080  coprmdvds  12091  coprmdvds2  12092  qredeq  12095  qredeu  12096  divgcdcoprmex  12101  cncongr1  12102  cncongr2  12103  prmdvdsexp  12147  rpexp1i  12153  sqrt2irr  12161  divnumden  12195  phiprmpw  12221  nnnn0modprm0  12254  modprmn0modprm0  12255  coprimeprodsq2  12257  pclemub  12286  pcprendvds2  12290  pcmul  12300  pcneg  12323  fldivp1  12345  prmpwdvds  12352  zgz  12370  mulgz  13009  mulgassr  13019  mulgmodid  13020  zsubrg  13445  zsssubrg  13449  zringmulg  13458  zringinvg  13464  ef2kpi  14197  efper  14198  sinperlem  14199  sin2kpi  14202  cos2kpi  14203  abssinper  14237  sinkpi  14238  coskpi  14239  cxpexprp  14286  lgslem3  14373  lgsneg  14395  lgsdir2lem2  14400  lgsdir2lem4  14402  lgsdir2  14404  lgssq  14411  lgsmulsqcoprm  14417  lgsdirnn0  14418  2lgsoddprmlem1  14423  2lgsoddprmlem2  14424  2sqlem2  14432  2sqlem7  14438