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

Theorem nnre 10616
Description: A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
Assertion
Ref Expression
nnre  |-  ( A  e.  NN  ->  A  e.  RR )

Proof of Theorem nnre
StepHypRef Expression
1 nnssre 10613 . 2  |-  NN  C_  RR
21sseli 3460 1  |-  ( A  e.  NN  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1868   RRcr 9538   NNcn 10609
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-i2m1 9607  ax-1ne0 9608  ax-rrecex 9611  ax-cnre 9612
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-ov 6304  df-om 6703  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-nn 10610
This theorem is referenced by:  nnrei  10618  nn2ge  10634  nnge1  10635  nngt1ne1  10636  nnle1eq1  10637  nngt0  10638  nnnlt1  10639  nnnle0  10640  nndivre  10645  nnrecgt0  10647  nnsub  10648  nnunb  10865  arch  10866  nnrecl  10867  bndndx  10868  0mnnnnn0  10902  nnnegz  10940  elnnz  10947  elz2  10954  gtndiv  11013  prime  11016  btwnz  11037  indstr  11227  qre  11269  rpnnen1lem1  11290  rpnnen1lem2  11291  rpnnen1lem3  11292  rpnnen1lem5  11294  nnrp  11311  qbtwnre  11492  fzo1fzo0n0  11957  elfzo0le  11959  fzonmapblen  11961  ubmelfzo  11978  fzonn0p1p1  11991  elfzom1p1elfzo  11992  ubmelm1fzo  12006  flltdivnn0lt  12064  quoremz  12081  quoremnn0ALT  12083  intfracq  12085  fldiv  12086  modmulnn  12113  modidmul0OLD  12122  addmodid  12138  modifeq2int  12151  modaddmodup  12152  modaddmodlo  12153  nnlesq  12377  digit2  12404  digit1  12405  facdiv  12471  facndiv  12472  faclbnd  12474  faclbnd3  12476  faclbnd4lem4  12480  faclbnd5  12482  bcval5  12502  seqcoll  12624  cshwidxmod  12895  cshwidxm1  12898  repswcshw  12901  isercolllem1  13715  harmonic  13904  efaddlem  14134  rpnnen2lem9  14262  rpnnen2  14265  sqrt2irr  14288  nndivdvds  14298  dvdsle  14337  dvdseq  14339  fzm1ndvds  14344  divalg2  14373  divalgmod  14374  ndvdsadd  14376  modgcd  14487  gcdmultiple  14505  gcdmultiplez  14506  gcdeq  14507  sqgcd  14513  dvdssqlem  14514  lcmgcdlem  14558  lcmf  14593  isprm3  14620  prmdvdsfz  14636  isprm5  14638  coprmgcdb  14641  qredeq  14650  qredeu  14651  ncoprmlnprm  14664  divdenle  14685  phibndlem  14705  eulerthlem2  14717  oddprm  14752  pythagtriplem10  14757  pythagtriplem12  14763  pythagtriplem14  14765  pythagtriplem16  14767  pythagtriplem19  14770  pclem  14775  pc2dvds  14815  pcmpt  14824  fldivp1  14829  pcbc  14832  infpnlem1  14841  infpn2  14844  prmreclem1  14847  prmreclem3  14849  vdwlem3  14920  ram0  14967  prmgaplem4  15011  prmgaplem7  15014  cshwshashlem1  15053  cshwshashlem2  15054  mulgnegnn  16755  odmodnn0  17176  gexdvds  17222  sylow3lem6  17271  prmirredlem  19050  znidomb  19118  chfacfisf  19864  chfacfisfcpmat  19865  chfacffsupp  19866  chfacfscmul0  19868  chfacfpmmul0  19872  ovolunlem1a  22435  ovoliunlem2  22442  ovolicc2lem3  22458  ovolicc2lem4OLD  22459  ovolicc2lem4  22460  iundisj2  22488  dyadss  22538  volsup2  22549  volivth  22551  vitali  22557  ismbf3d  22596  mbfi1fseqlem3  22661  mbfi1fseqlem4  22662  mbfi1fseqlem5  22663  itg2seq  22686  itg2gt0  22704  itg2cnlem1  22705  plyeq0lem  23150  dgreq0  23205  dgrcolem2  23214  elqaalem2  23259  elqaalem3  23260  elqaalem2OLD  23262  elqaalem3OLD  23263  logtayllem  23590  leibpi  23854  birthdaylem3  23865  zetacvg  23926  eldmgm  23933  basellem1  23993  basellem2  23994  basellem3  23995  basellem6  23998  basellem9  24001  prmorcht  24091  dvdsdivcl  24096  dvdsflsumcom  24103  muinv  24108  vmalelog  24119  chtublem  24125  logfac2  24131  logfaclbnd  24136  pcbcctr  24190  bcmono  24191  bposlem1  24198  bposlem5  24202  bposlem6  24203  bpos  24207  lgsval4a  24232  lgsquadlem1  24268  lgsquadlem2  24269  dchrisum0re  24337  dchrisum0lem1  24340  logdivbnd  24380  ostth2lem1  24442  ostth2lem3  24459  clwwlkel  25506  clwwlkf  25507  clwwlkf1  25509  wwlkext2clwwlk  25516  wwlksubclwwlk  25517  clwwisshclwwlem  25519  numclwlk2lem2f  25816  gxnn0neg  25976  gxmodid  25992  nmounbseqi  26403  nmounbseqiALT  26404  nmobndseqi  26405  nmobndseqiALT  26406  ubthlem1  26497  minvecolem3  26503  minvecolem3OLD  26513  lnconi  27671  iundisj2f  28189  xrsmulgzz  28434  esumpmono  28895  eulerpartlemb  29196  fibp1  29229  subfaclim  29906  subfacval3  29907  snmlff  30047  fz0n  30358  bcprod  30368  nn0prpwlem  30970  nn0prpw  30971  nndivsub  31109  nndivlub  31110  poimirlem13  31866  poimirlem14  31867  poimirlem31  31884  poimirlem32  31885  mblfinlem2  31891  fzmul  31982  incsequz  31990  nnubfi  31992  nninfnub  31993  irrapxlem1  35585  irrapxlem2  35586  pellexlem1  35592  pellexlem5  35596  pellqrex  35645  monotoddzzfi  35709  jm2.24nn  35728  congabseq  35743  acongrep  35749  acongeq  35752  expdiophlem1  35795  idomrootle  35988  idomodle  35989  hashgcdlem  35993  relexpmulnn  36160  prmunb2  36516  hashnzfzclim  36528  fmuldfeq  37480  sumnnodd  37529  stoweidlem14  37693  stoweidlem17  37696  stoweidlem20  37699  stoweidlem49  37729  stoweidlem60  37740  wallispilem3  37748  wallispilem4  37749  wallispilem5  37750  wallispi  37751  wallispi2lem1  37752  wallispi2lem2  37753  stirlinglem1  37755  stirlinglem3  37757  stirlinglem4  37758  stirlinglem6  37760  stirlinglem7  37761  stirlinglem10  37764  stirlinglem11  37765  stirlinglem12  37766  stirlinglem13  37767  stirlingr  37771  dirker2re  37773  dirkerval2  37775  dirkerre  37776  dirkertrigeqlem1  37779  fourierdlem66  37855  fourierdlem73  37862  fourierdlem83  37872  fourierdlem87  37876  fourierdlem103  37892  fourierdlem104  37893  fourierdlem111  37900  fouriersw  37914  etransclem24  37942  sge0rpcpnf  38050  hoicvr  38144  hoicvrrex  38152  gcdzeq  38504  nn0oALTV  38536  nnsum4primes4  38595  nnsum4primesprm  38597  nnsum4primesgbe  38599  nnsum4primesle9  38601  bgoldbachlt  38617  tgoldbach  38622  subsubelfzo0  38750  altgsumbcALT  39407  modn0mul  39596  m1modmmod  39597  difmodm1lt  39598  nno  39601  nnlog2ge0lt1  39650  logbpw2m1  39651  blennn  39659  blennnelnn  39660  nnpw2pmod  39667  nnolog2flm1  39674  digvalnn0  39683  dignn0fr  39685  dignn0ldlem  39686  dignnld  39687  dig2nn1st  39689
  Copyright terms: Public domain W3C validator