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

Theorem nncn 10351
Description: A positive integer 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 10348 . 2  |-  NN  C_  CC
21sseli 3373 1  |-  ( A  e.  NN  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   CCcc 9301   NNcn 10343
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393  ax-resscn 9360  ax-1cn 9361  ax-icn 9362  ax-addcl 9363  ax-addrcl 9364  ax-mulcl 9365  ax-mulrcl 9366  ax-i2m1 9371  ax-1ne0 9372  ax-rrecex 9375  ax-cnre 9376
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-iun 4194  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-ov 6115  df-om 6498  df-recs 6853  df-rdg 6887  df-nn 10344
This theorem is referenced by:  nn1m1nn  10363  nn1suc  10364  nnaddcl  10365  nnmulcl  10366  nnsub  10381  nndiv  10383  nndivtr  10384  nnnn0addcl  10631  nn0nnaddcl  10632  elnnnn0  10644  nn0sub  10651  nnnegz  10670  elz2  10684  zaddcl  10706  nnaddm1cl  10722  zdiv  10733  zdivadd  10734  zdivmul  10735  nneo  10746  peano5uzi  10751  uzindOLD  10757  elq  10976  qmulz  10977  qaddcl  10990  qnegcl  10991  qmulcl  10992  qreccl  10994  rpnnen1lem5  11004  fseq1m1p1  11556  ubmelm1fzo  11644  quoremz  11715  quoremnn0ALT  11717  intfracq  11719  fldiv  11720  fldiv2  11721  modmulnn  11746  modidmul0  11755  modaddmodup  11783  nn0ennn  11822  ser1const  11883  expneg  11894  expm1t  11913  nnsqcl  11956  nnlesq  11990  digit2  12018  digit1  12019  facdiv  12084  facndiv  12085  faclbnd  12087  faclbnd4lem1  12090  faclbnd4lem4  12093  bcn1  12110  bcm1k  12112  bcp1n  12113  bcval5  12115  bcn2m1  12121  swrdccatwrd  12383  cshwidxmod  12461  cshwidxm  12465  cshwidxn  12466  repswcshw  12467  isercoll2  13167  divcnv  13337  harmonic  13342  arisum  13343  arisum2  13344  expcnv  13347  geomulcvg  13357  mertenslem2  13366  ef0lem  13385  efexp  13406  ruclem12  13544  sqr2irr  13552  divalgmod  13631  ndvdsadd  13633  modgcd  13741  gcddiv  13754  gcdmultiple  13755  gcdmultiplez  13756  rpmulgcd  13760  rplpwr  13761  sqgcd  13763  prmind2  13795  qredeq  13813  qredeu  13814  isprm6  13816  divnumden  13847  divdenle  13848  nn0gcdsq  13851  pythagtriplem1  13904  pythagtriplem2  13905  pythagtriplem6  13909  pythagtriplem7  13910  pythagtriplem12  13914  pythagtriplem14  13916  pythagtriplem15  13917  pythagtriplem16  13918  pythagtriplem17  13919  pythagtriplem19  13921  pcqcl  13944  pcexp  13947  pcneg  13961  fldivp1  13980  prmpwdvds  13986  infpnlem2  13993  prmreclem1  13998  prmreclem6  14003  4sqlem19  14045  vdwapun  14056  vdwapid1  14057  mulgnegnn  15658  mulgnnass  15676  odmod  16070  cnfldmulg  17870  prmirredlem  17939  prmirredlemOLD  17942  znidomb  18016  znrrg  18020  ovolunlem1  21002  uniioombllem3  21087  vitali  21115  mbfi1fseqlem3  21217  dvexp  21449  dvexp3  21472  plyeq0lem  21700  dgrcolem1  21762  aaliou3lem2  21831  aaliou3lem7  21837  pserdv2  21917  abelthlem6  21923  logtayl  22127  logtaylsum  22128  logtayl2  22129  cxpexp  22135  cxproot  22157  root1id  22214  root1eq1  22215  cxpeq  22217  atantayl  22354  atantayl2  22355  birthdaylem2  22368  dfef2  22386  emcllem2  22412  emcllem3  22413  basellem2  22441  basellem3  22442  basellem5  22444  basellem8  22447  mumul  22541  dvdsdivcl  22543  dvdsflip  22544  fsumdvdscom  22547  muinv  22555  chtublem  22572  perfect  22592  pcbcctr  22637  bclbnd  22641  bposlem1  22645  bposlem6  22650  lgssq  22696  lgssq2  22697  2sqlem6  22730  2sqlem10  22735  rplogsumlem1  22755  dchrmusumlema  22764  dchrmusum2  22765  dchrvmasumiflem1  22772  dchrvmaeq0  22775  dchrisum0re  22784  logdivbnd  22827  cusgrasize2inds  23407  gxnn0neg  23772  ipasslem4  24256  ipasslem5  24257  isarchi3  26226  oddpwdc  26759  eulerpartlemb  26773  fibp1  26806  zetacvg  27023  lgam1  27072  gamfac  27075  subfacp1lem6  27095  subfaclim  27098  snmlff  27240  circum  27341  divcnvlin  27421  iprodgam  27528  faclim  27574  faclim2  27576  nndivsub  28325  mblfinlem2  28455  ovoliunnfl  28459  voliunnfl  28461  nn0prpwlem  28543  irrapxlem1  29189  pellexlem1  29196  pellqrex  29246  2nn0ind  29312  jm2.17c  29331  acongrep  29349  jm2.18  29363  jm2.20nn  29372  jm2.16nn0  29379  hashgcdlem  29591  proot1ex  29595  clim1fr1  29800  wallispilem4  29889  wallispilem5  29890  wallispi  29891  wallispi2lem1  29892  wallispi2lem2  29893  wallispi2  29894  stirlinglem1  29895  stirlinglem3  29897  stirlinglem4  29898  stirlinglem5  29899  stirlinglem6  29900  stirlinglem7  29901  stirlinglem8  29902  stirlinglem10  29904  stirlinglem11  29905  stirlinglem12  29906  stirlinglem13  29907  stirlinglem14  29908  stirlinglem15  29909  subsubelfzo0  30236  clwwlkel  30481  clwwlkf  30482  clwwlkf1  30484  wwlksubclwwlk  30492  rusgra0edg  30599  clwwlkextfrlem1  30695  numclwwlk2lem1  30721  numclwlk2lem2f  30722  numclwlk2lem2f1o  30724  bcpascm1  30777  altgsumbcALT  30779  cply1mul  30884
  Copyright terms: Public domain W3C validator