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

Theorem nncn 9799
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 9796 . 2  |-  NN  C_  CC
21sseli 3210 1  |-  ( A  e.  NN  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1701   CCcc 8780   NNcn 9791
This theorem is referenced by:  nn1m1nn  9811  nn1suc  9812  nnaddcl  9813  nnmulcl  9814  nnsub  9829  nndiv  9831  nndivtr  9832  nnnn0addcl  10042  nn0nnaddcl  10043  elnnnn0  10054  nn0sub  10061  nnnegz  10074  elz2  10087  zaddcl  10106  nnaddm1cl  10120  zdiv  10129  zdivadd  10130  zdivmul  10131  nneo  10142  peano5uzi  10147  uzindOLD  10153  elq  10365  qmulz  10366  qaddcl  10379  qnegcl  10380  qmulcl  10381  qreccl  10383  rpnnen1lem5  10393  fseq1m1p1  10905  quoremz  11006  quoremnn0ALT  11008  intfracq  11010  fldiv  11011  fldiv2  11012  modmulnn  11035  nn0ennn  11088  ser1const  11149  expneg  11158  expm1t  11177  nnsqcl  11220  nnlesq  11253  digit2  11281  digit1  11282  facdiv  11347  facndiv  11348  faclbnd  11350  faclbnd4lem1  11353  faclbnd4lem4  11356  bcn1  11372  bcm1k  11374  bcp1n  11375  bcval5  11377  isercoll2  12189  divcnv  12359  harmonic  12364  arisum  12365  arisum2  12366  expcnv  12369  geomulcvg  12379  mertenslem2  12388  ef0lem  12407  efexp  12428  ruclem12  12566  sqr2irr  12574  divalgmod  12652  ndvdsadd  12654  modgcd  12762  gcddiv  12775  gcdmultiple  12776  gcdmultiplez  12777  rpmulgcd  12781  rplpwr  12782  sqgcd  12784  prmind2  12816  qredeq  12832  qredeu  12833  isprm6  12835  divnumden  12866  divdenle  12867  nn0gcdsq  12870  pythagtriplem1  12916  pythagtriplem2  12917  pythagtriplem6  12921  pythagtriplem7  12922  pythagtriplem12  12926  pythagtriplem14  12928  pythagtriplem15  12929  pythagtriplem16  12930  pythagtriplem17  12931  pythagtriplem19  12933  pcqcl  12956  pcexp  12959  pcneg  12973  fldivp1  12992  prmpwdvds  12998  infpnlem2  13005  prmreclem1  13010  prmreclem6  13015  4sqlem19  13057  vdwapun  13068  vdwapid1  13069  mulgnegnn  14626  mulgnnass  14644  odmod  14910  cnfldmulg  16462  prmirredlem  16502  znidomb  16571  znrrg  16575  ovolunlem1  18909  uniioombllem3  18993  vitali  19021  mbfi1fseqlem3  19125  dvexp  19355  dvexp3  19378  plyeq0lem  19645  dgrcolem1  19707  aaliou3lem2  19776  aaliou3lem7  19782  pserdv2  19859  abelthlem6  19865  logtayl  20060  logtaylsum  20061  logtayl2  20062  cxpexp  20068  cxproot  20090  root1id  20147  root1eq1  20148  cxpeq  20150  atantayl  20286  atantayl2  20287  birthdaylem2  20300  dfef2  20318  emcllem2  20343  emcllem3  20344  basellem2  20372  basellem3  20373  basellem5  20375  basellem8  20378  mumul  20472  dvdsdivcl  20474  dvdsflip  20475  fsumdvdscom  20478  muinv  20486  chtublem  20503  perfect  20523  pcbcctr  20568  bclbnd  20572  bposlem1  20576  bposlem6  20581  lgssq  20627  lgssq2  20628  2sqlem6  20661  2sqlem10  20666  rplogsumlem1  20686  dchrmusumlema  20695  dchrmusum2  20696  dchrvmasumiflem1  20703  dchrvmaeq0  20706  dchrisum0re  20715  logdivbnd  20758  gxnn0neg  20983  ipasslem4  21467  ipasslem5  21468  zetacvg  23973  subfacp1lem6  24000  subfaclim  24003  snmlff  24196  circum  24291  divcnvlin  24393  faclim  24484  faclim2  24486  nndivsub  25282  ovoliunnfl  25315  nn0prpwlem  25387  irrapxlem1  26055  pellexlem1  26062  pellqrex  26112  2nn0ind  26178  jm2.17c  26197  acongrep  26215  jm2.18  26229  jm2.20nn  26238  jm2.16nn0  26245  hashgcdlem  26664  proot1ex  26668  clim1fr1  26875  dvsinexp  26888  itgsinexp  26897  stoweidlem1  26898  stoweidlem11  26908  stoweidlem14  26911  stoweidlem25  26922  stoweidlem26  26923  stoweidlem34  26931  stoweidlem37  26934  stoweidlem38  26935  stoweidlem42  26939  wallispilem4  26965  wallispilem5  26966  wallispi  26967  wallispi2lem1  26968  wallispi2lem2  26969  wallispi2  26970  stirlinglem1  26971  stirlinglem3  26973  stirlinglem4  26974  stirlinglem5  26975  stirlinglem6  26976  stirlinglem7  26977  stirlinglem8  26978  stirlinglem10  26980  stirlinglem11  26981  stirlinglem12  26982  stirlinglem13  26983  stirlinglem14  26984  stirlinglem15  26985
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-resscn 8839  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-i2m1 8850  ax-1ne0 8851  ax-rrecex 8854  ax-cnre 8855
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 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-reu 2584  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-iun 3944  df-br 4061  df-opab 4115  df-mpt 4116  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-ov 5903  df-recs 6430  df-rdg 6465  df-nn 9792
  Copyright terms: Public domain W3C validator