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

Theorem nncn 9933
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 9930 . 2  |-  NN  C_  CC
21sseli 3280 1  |-  ( A  e.  NN  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   CCcc 8914   NNcn 9925
This theorem is referenced by:  nn1m1nn  9945  nn1suc  9946  nnaddcl  9947  nnmulcl  9948  nnsub  9963  nndiv  9965  nndivtr  9966  nnnn0addcl  10176  nn0nnaddcl  10177  elnnnn0  10188  nn0sub  10195  nnnegz  10210  elz2  10223  zaddcl  10242  nnaddm1cl  10256  zdiv  10265  zdivadd  10266  zdivmul  10267  nneo  10278  peano5uzi  10283  uzindOLD  10289  elq  10501  qmulz  10502  qaddcl  10515  qnegcl  10516  qmulcl  10517  qreccl  10519  rpnnen1lem5  10529  fseq1m1p1  11046  quoremz  11156  quoremnn0ALT  11158  intfracq  11160  fldiv  11161  fldiv2  11162  modmulnn  11185  nn0ennn  11238  ser1const  11299  expneg  11309  expm1t  11328  nnsqcl  11371  nnlesq  11404  digit2  11432  digit1  11433  facdiv  11498  facndiv  11499  faclbnd  11501  faclbnd4lem1  11504  faclbnd4lem4  11507  bcn1  11524  bcm1k  11526  bcp1n  11527  bcval5  11529  bcn2m1  11535  isercoll2  12382  divcnv  12553  harmonic  12558  arisum  12559  arisum2  12560  expcnv  12563  geomulcvg  12573  mertenslem2  12582  ef0lem  12601  efexp  12622  ruclem12  12760  sqr2irr  12768  divalgmod  12846  ndvdsadd  12848  modgcd  12956  gcddiv  12969  gcdmultiple  12970  gcdmultiplez  12971  rpmulgcd  12975  rplpwr  12976  sqgcd  12978  prmind2  13010  qredeq  13026  qredeu  13027  isprm6  13029  divnumden  13060  divdenle  13061  nn0gcdsq  13064  pythagtriplem1  13110  pythagtriplem2  13111  pythagtriplem6  13115  pythagtriplem7  13116  pythagtriplem12  13120  pythagtriplem14  13122  pythagtriplem15  13123  pythagtriplem16  13124  pythagtriplem17  13125  pythagtriplem19  13127  pcqcl  13150  pcexp  13153  pcneg  13167  fldivp1  13186  prmpwdvds  13192  infpnlem2  13199  prmreclem1  13204  prmreclem6  13209  4sqlem19  13251  vdwapun  13262  vdwapid1  13263  mulgnegnn  14820  mulgnnass  14838  odmod  15104  cnfldmulg  16649  prmirredlem  16689  znidomb  16758  znrrg  16762  ovolunlem1  19253  uniioombllem3  19337  vitali  19365  mbfi1fseqlem3  19469  dvexp  19699  dvexp3  19722  plyeq0lem  19989  dgrcolem1  20051  aaliou3lem2  20120  aaliou3lem7  20126  pserdv2  20206  abelthlem6  20212  logtayl  20411  logtaylsum  20412  logtayl2  20413  cxpexp  20419  cxproot  20441  root1id  20498  root1eq1  20499  cxpeq  20501  atantayl  20637  atantayl2  20638  birthdaylem2  20651  dfef2  20669  emcllem2  20695  emcllem3  20696  basellem2  20724  basellem3  20725  basellem5  20727  basellem8  20730  mumul  20824  dvdsdivcl  20826  dvdsflip  20827  fsumdvdscom  20830  muinv  20838  chtublem  20855  perfect  20875  pcbcctr  20920  bclbnd  20924  bposlem1  20928  bposlem6  20933  lgssq  20979  lgssq2  20980  2sqlem6  21013  2sqlem10  21018  rplogsumlem1  21038  dchrmusumlema  21047  dchrmusum2  21048  dchrvmasumiflem1  21055  dchrvmaeq0  21058  dchrisum0re  21067  logdivbnd  21110  cusgrasize2inds  21345  gxnn0neg  21692  ipasslem4  22176  ipasslem5  22177  zetacvg  24571  lgam1  24620  gamfac  24623  subfacp1lem6  24643  subfaclim  24646  snmlff  24788  circum  24883  divcnvlin  24984  faclim  25116  faclim2  25118  nndivsub  25914  ovoliunnfl  25946  voliunnfl  25948  nn0prpwlem  26009  irrapxlem1  26569  pellexlem1  26576  pellqrex  26626  2nn0ind  26692  jm2.17c  26711  acongrep  26729  jm2.18  26743  jm2.20nn  26752  jm2.16nn0  26759  hashgcdlem  27178  proot1ex  27182  clim1fr1  27388  wallispilem4  27478  wallispilem5  27479  wallispi  27480  wallispi2lem1  27481  wallispi2lem2  27482  wallispi2  27483  stirlinglem1  27484  stirlinglem3  27486  stirlinglem4  27487  stirlinglem5  27488  stirlinglem6  27489  stirlinglem7  27490  stirlinglem8  27491  stirlinglem10  27493  stirlinglem11  27494  stirlinglem12  27495  stirlinglem13  27496  stirlinglem14  27497  stirlinglem15  27498
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 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-sep 4264  ax-nul 4272  ax-pow 4311  ax-pr 4337  ax-un 4634  ax-resscn 8973  ax-1cn 8974  ax-icn 8975  ax-addcl 8976  ax-addrcl 8977  ax-mulcl 8978  ax-mulrcl 8979  ax-i2m1 8984  ax-1ne0 8985  ax-rrecex 8988  ax-cnre 8989
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 2235  df-mo 2236  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-ral 2647  df-rex 2648  df-reu 2649  df-rab 2651  df-v 2894  df-sbc 3098  df-csb 3188  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-pss 3272  df-nul 3565  df-if 3676  df-pw 3737  df-sn 3756  df-pr 3757  df-tp 3758  df-op 3759  df-uni 3951  df-iun 4030  df-br 4147  df-opab 4201  df-mpt 4202  df-tr 4237  df-eprel 4428  df-id 4432  df-po 4437  df-so 4438  df-fr 4475  df-we 4477  df-ord 4518  df-on 4519  df-lim 4520  df-suc 4521  df-om 4779  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5351  df-fun 5389  df-fn 5390  df-f 5391  df-f1 5392  df-fo 5393  df-f1o 5394  df-fv 5395  df-ov 6016  df-recs 6562  df-rdg 6597  df-nn 9926
  Copyright terms: Public domain W3C validator