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

Theorem nncn 9968
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 9965 . 2  |-  NN  C_  CC
21sseli 3308 1  |-  ( A  e.  NN  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   CCcc 8948   NNcn 9960
This theorem is referenced by:  nn1m1nn  9980  nn1suc  9981  nnaddcl  9982  nnmulcl  9983  nnsub  9998  nndiv  10000  nndivtr  10001  nnnn0addcl  10211  nn0nnaddcl  10212  elnnnn0  10223  nn0sub  10230  nnnegz  10245  elz2  10258  zaddcl  10277  nnaddm1cl  10291  zdiv  10300  zdivadd  10301  zdivmul  10302  nneo  10313  peano5uzi  10318  uzindOLD  10324  elq  10536  qmulz  10537  qaddcl  10550  qnegcl  10551  qmulcl  10552  qreccl  10554  rpnnen1lem5  10564  fseq1m1p1  11082  quoremz  11195  quoremnn0ALT  11197  intfracq  11199  fldiv  11200  fldiv2  11201  modmulnn  11224  nn0ennn  11277  ser1const  11338  expneg  11348  expm1t  11367  nnsqcl  11410  nnlesq  11443  digit2  11471  digit1  11472  facdiv  11537  facndiv  11538  faclbnd  11540  faclbnd4lem1  11543  faclbnd4lem4  11546  bcn1  11563  bcm1k  11565  bcp1n  11566  bcval5  11568  bcn2m1  11574  isercoll2  12421  divcnv  12592  harmonic  12597  arisum  12598  arisum2  12599  expcnv  12602  geomulcvg  12612  mertenslem2  12621  ef0lem  12640  efexp  12661  ruclem12  12799  sqr2irr  12807  divalgmod  12885  ndvdsadd  12887  modgcd  12995  gcddiv  13008  gcdmultiple  13009  gcdmultiplez  13010  rpmulgcd  13014  rplpwr  13015  sqgcd  13017  prmind2  13049  qredeq  13065  qredeu  13066  isprm6  13068  divnumden  13099  divdenle  13100  nn0gcdsq  13103  pythagtriplem1  13149  pythagtriplem2  13150  pythagtriplem6  13154  pythagtriplem7  13155  pythagtriplem12  13159  pythagtriplem14  13161  pythagtriplem15  13162  pythagtriplem16  13163  pythagtriplem17  13164  pythagtriplem19  13166  pcqcl  13189  pcexp  13192  pcneg  13206  fldivp1  13225  prmpwdvds  13231  infpnlem2  13238  prmreclem1  13243  prmreclem6  13248  4sqlem19  13290  vdwapun  13301  vdwapid1  13302  mulgnegnn  14859  mulgnnass  14877  odmod  15143  cnfldmulg  16692  prmirredlem  16732  znidomb  16801  znrrg  16805  ovolunlem1  19350  uniioombllem3  19434  vitali  19462  mbfi1fseqlem3  19566  dvexp  19796  dvexp3  19819  plyeq0lem  20086  dgrcolem1  20148  aaliou3lem2  20217  aaliou3lem7  20223  pserdv2  20303  abelthlem6  20309  logtayl  20508  logtaylsum  20509  logtayl2  20510  cxpexp  20516  cxproot  20538  root1id  20595  root1eq1  20596  cxpeq  20598  atantayl  20734  atantayl2  20735  birthdaylem2  20748  dfef2  20766  emcllem2  20792  emcllem3  20793  basellem2  20821  basellem3  20822  basellem5  20824  basellem8  20827  mumul  20921  dvdsdivcl  20923  dvdsflip  20924  fsumdvdscom  20927  muinv  20935  chtublem  20952  perfect  20972  pcbcctr  21017  bclbnd  21021  bposlem1  21025  bposlem6  21030  lgssq  21076  lgssq2  21077  2sqlem6  21110  2sqlem10  21115  rplogsumlem1  21135  dchrmusumlema  21144  dchrmusum2  21145  dchrvmasumiflem1  21152  dchrvmaeq0  21155  dchrisum0re  21164  logdivbnd  21207  cusgrasize2inds  21443  gxnn0neg  21808  ipasslem4  22292  ipasslem5  22293  zetacvg  24756  lgam1  24805  gamfac  24808  subfacp1lem6  24828  subfaclim  24831  snmlff  24973  circum  25068  divcnvlin  25169  iprodgam  25276  faclim  25317  faclim2  25319  nndivsub  26115  mblfinlem  26147  ovoliunnfl  26151  voliunnfl  26153  nn0prpwlem  26219  irrapxlem1  26779  pellexlem1  26786  pellqrex  26836  2nn0ind  26902  jm2.17c  26921  acongrep  26939  jm2.18  26953  jm2.20nn  26962  jm2.16nn0  26969  hashgcdlem  27388  proot1ex  27392  clim1fr1  27598  wallispilem4  27688  wallispilem5  27689  wallispi  27690  wallispi2lem1  27691  wallispi2lem2  27692  wallispi2  27693  stirlinglem1  27694  stirlinglem3  27696  stirlinglem4  27697  stirlinglem5  27698  stirlinglem6  27699  stirlinglem7  27700  stirlinglem8  27701  stirlinglem10  27703  stirlinglem11  27704  stirlinglem12  27705  stirlinglem13  27706  stirlinglem14  27707  stirlinglem15  27708  swrdccatin12lem3  28028  swrdccatin12  28030
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664  ax-resscn 9007  ax-1cn 9008  ax-icn 9009  ax-addcl 9010  ax-addrcl 9011  ax-mulcl 9012  ax-mulrcl 9013  ax-i2m1 9018  ax-1ne0 9019  ax-rrecex 9022  ax-cnre 9023
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-reu 2677  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-pss 3300  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-tp 3786  df-op 3787  df-uni 3980  df-iun 4059  df-br 4177  df-opab 4231  df-mpt 4232  df-tr 4267  df-eprel 4458  df-id 4462  df-po 4467  df-so 4468  df-fr 4505  df-we 4507  df-ord 4548  df-on 4549  df-lim 4550  df-suc 4551  df-om 4809  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-ov 6047  df-recs 6596  df-rdg 6631  df-nn 9961
  Copyright terms: Public domain W3C validator