MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nncn Unicode version

Theorem nncn 9756
Description: A natural number is a complex number. (Contributed by NM, 18-Aug-1999.)
Assertion
Ref Expression
nncn  |-  ( A  e.  NN  ->  A  e.  CC )

Proof of Theorem nncn
StepHypRef Expression
1 nnsscn 9753 . 2  |-  NN  C_  CC
21sseli 3178 1  |-  ( A  e.  NN  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1686   CCcc 8737   NNcn 9748
This theorem is referenced by:  nn1m1nn  9768  nn1suc  9769  nnaddcl  9770  nnmulcl  9771  nnsub  9786  nndiv  9788  nndivtr  9789  nnnn0addcl  9997  nn0nnaddcl  9998  elnnnn0  10009  nn0sub  10016  nnnegz  10029  elz2  10042  zaddcl  10061  nnaddm1cl  10075  zdiv  10084  zdivadd  10085  zdivmul  10086  nneo  10097  peano5uzi  10102  uzindOLD  10108  elq  10320  qmulz  10321  qaddcl  10334  qnegcl  10335  qmulcl  10336  qreccl  10338  rpnnen1lem5  10348  fseq1m1p1  10860  quoremz  10961  quoremnn0ALT  10963  intfracq  10965  fldiv  10966  fldiv2  10967  modmulnn  10990  nn0ennn  11043  ser1const  11104  expneg  11113  expm1t  11132  nnsqcl  11175  nnlesq  11208  digit2  11236  digit1  11237  facdiv  11302  facndiv  11303  faclbnd  11305  faclbnd4lem1  11308  faclbnd4lem4  11311  bcn1  11327  bcm1k  11329  bcp1n  11330  bcval5  11332  isercoll2  12144  divcnv  12314  harmonic  12319  arisum  12320  arisum2  12321  expcnv  12324  geomulcvg  12334  mertenslem2  12343  ef0lem  12362  efexp  12383  ruclem12  12521  sqr2irr  12529  divalgmod  12607  ndvdsadd  12609  modgcd  12717  gcddiv  12730  gcdmultiple  12731  gcdmultiplez  12732  rpmulgcd  12736  rplpwr  12737  sqgcd  12739  prmind2  12771  qredeq  12787  qredeu  12788  isprm6  12790  divnumden  12821  divdenle  12822  nn0gcdsq  12825  pythagtriplem1  12871  pythagtriplem2  12872  pythagtriplem6  12876  pythagtriplem7  12877  pythagtriplem12  12881  pythagtriplem14  12883  pythagtriplem15  12884  pythagtriplem16  12885  pythagtriplem17  12886  pythagtriplem19  12888  pcqcl  12911  pcexp  12914  pcneg  12928  fldivp1  12947  prmpwdvds  12953  infpnlem2  12960  prmreclem1  12965  prmreclem6  12970  4sqlem19  13012  vdwapun  13023  vdwapid1  13024  mulgnegnn  14579  mulgnnass  14597  odmod  14863  cnfldmulg  16408  prmirredlem  16448  znidomb  16517  znrrg  16521  ovolunlem1  18858  uniioombllem3  18942  vitali  18970  mbfi1fseqlem3  19074  dvexp  19304  dvexp3  19327  plyeq0lem  19594  dgrcolem1  19656  aaliou3lem2  19725  aaliou3lem7  19731  pserdv2  19808  abelthlem6  19814  logtayl  20009  logtaylsum  20010  logtayl2  20011  cxpexp  20017  cxproot  20039  root1id  20096  root1eq1  20097  cxpeq  20099  atantayl  20235  atantayl2  20236  birthdaylem2  20249  dfef2  20267  emcllem2  20292  emcllem3  20293  basellem2  20321  basellem3  20322  basellem5  20324  basellem8  20327  mumul  20421  dvdsdivcl  20423  dvdsflip  20424  fsumdvdscom  20427  muinv  20435  chtublem  20452  perfect  20472  pcbcctr  20517  bclbnd  20521  bposlem1  20525  bposlem6  20530  lgssq  20576  lgssq2  20577  2sqlem6  20610  2sqlem10  20615  rplogsumlem1  20635  dchrmusumlema  20644  dchrmusum2  20645  dchrvmasumiflem1  20652  dchrvmaeq0  20655  dchrisum0re  20664  logdivbnd  20707  gxnn0neg  20932  ipasslem4  21414  ipasslem5  21415  zetacvg  23691  subfacp1lem6  23718  subfaclim  23721  snmlff  23914  circum  24009  nndivsub  24898  nn0prpwlem  26249  irrapxlem1  26918  pellexlem1  26925  pellqrex  26975  2nn0ind  27041  jm2.17c  27060  acongrep  27078  jm2.18  27092  jm2.20nn  27101  jm2.16nn0  27108  hashgcdlem  27527  proot1ex  27531  clim1fr1  27738  dvsinexp  27751  itgsinexp  27760  stoweidlem1  27761  stoweidlem11  27771  stoweidlem14  27774  stoweidlem25  27785  stoweidlem26  27786  stoweidlem34  27794  stoweidlem37  27797  stoweidlem38  27798  stoweidlem42  27802  wallispilem4  27828  wallispilem5  27829  wallispi  27830  wallispi2lem1  27831  wallispi2lem2  27832  wallispi2  27833  stirlinglem1  27834  stirlinglem3  27836  stirlinglem4  27837  stirlinglem5  27838  stirlinglem6  27839  stirlinglem7  27840  stirlinglem8  27841  stirlinglem10  27843  stirlinglem11  27844  stirlinglem12  27845  stirlinglem13  27846  stirlinglem14  27847  stirlinglem15  27848
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514  ax-resscn 8796  ax-1cn 8797  ax-icn 8798  ax-addcl 8799  ax-addrcl 8800  ax-mulcl 8801  ax-mulrcl 8802  ax-i2m1 8807  ax-1ne0 8808  ax-rrecex 8811  ax-cnre 8812
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4307  df-id 4311  df-po 4316  df-so 4317  df-fr 4354  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-ov 5863  df-recs 6390  df-rdg 6425  df-nn 9749
  Copyright terms: Public domain W3C validator