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

Theorem nnre 9843
Description: A natural number 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 9840 . 2  |-  NN  C_  RR
21sseli 3252 1  |-  ( A  e.  NN  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710   RRcr 8826   NNcn 9836
This theorem is referenced by:  nnrei  9845  nn2ge  9861  nnge1  9862  nngt1ne1  9863  nnle1eq1  9864  nngt0  9865  nnnlt1  9866  nndivre  9871  nnrecgt0  9873  nnsub  9874  nnunb  10053  arch  10054  nnrecl  10055  bndndx  10056  nnnegz  10119  elnnz  10126  elz2  10132  gtndiv  10181  prime  10184  btwnz  10206  indstr  10379  qre  10413  rpnnen1lem1  10434  rpnnen1lem2  10435  rpnnen1lem3  10436  rpnnen1lem5  10438  nnrp  10455  qbtwnre  10618  quoremz  11051  quoremnn0  11052  quoremnn0ALT  11053  intfracq  11055  fldiv  11056  modmulnn  11080  nnlesq  11299  digit2  11327  digit1  11328  facdiv  11393  facndiv  11394  faclbnd  11396  faclbnd3  11398  faclbnd4lem4  11402  faclbnd5  11404  bcval5  11423  seqcoll  11497  isercolllem1  12234  harmonic  12414  efaddlem  12471  rpnnen2lem9  12598  rpnnen2  12601  sqr2irr  12624  nndivdvds  12634  dvdsle  12671  dvdseq  12673  fzm1ndvds  12677  divalg2  12701  divalgmod  12702  ndvdsadd  12704  modgcd  12812  gcdmultiple  12826  gcdmultiplez  12827  gcdeq  12828  sqgcd  12834  dvdssqlem  12835  isprm3  12864  qredeq  12882  qredeu  12883  isprm5  12888  divdenle  12917  phibndlem  12935  eulerthlem2  12947  oddprm  12965  pythagtriplem10  12970  pythagtriplem12  12976  pythagtriplem14  12978  pythagtriplem16  12980  pythagtriplem19  12983  pclem  12988  pc2dvds  13028  pcmpt  13037  fldivp1  13042  pcbc  13045  infpnlem1  13054  infpn2  13057  prmreclem1  13060  prmreclem3  13062  vdwlem3  13127  ram0  13166  mulgnegnn  14676  odmodnn0  14954  gexdvds  14994  sylow3lem6  15042  prmirredlem  16552  znidomb  16621  ovolunlem1a  18959  ovoliunlem2  18966  ovolicc2lem3  18982  ovolicc2lem4  18983  iundisj2  19010  dyadss  19053  volsup2  19064  volivth  19066  vitali  19072  ismbf3d  19113  mbfi1fseqlem3  19176  mbfi1fseqlem4  19177  mbfi1fseqlem5  19178  itg2seq  19201  itg2gt0  19219  itg2cnlem1  19220  plyeq0lem  19696  dgreq0  19750  dgrcolem2  19759  elqaalem2  19804  elqaalem3  19805  logtayllem  20117  leibpi  20349  birthdaylem3  20359  basellem1  20430  basellem2  20431  basellem3  20432  basellem6  20435  basellem9  20438  prmorcht  20528  dvdsdivcl  20533  dvdsflsumcom  20540  muinv  20545  vmalelog  20556  chtublem  20562  logfac2  20568  logfaclbnd  20573  pcbcctr  20627  bcmono  20628  bposlem1  20635  bposlem5  20639  bposlem6  20640  bpos  20644  lgsval4a  20669  lgsquadlem1  20705  lgsquadlem2  20706  dchrisum0re  20774  dchrisum0lem1  20777  logdivbnd  20817  ostth2lem1  20879  ostth2lem3  20896  gxnn0neg  21042  gxmodid  21058  nmounbseqi  21469  nmounbseqiOLD  21470  nmobndseqi  21471  nmobndseqiOLD  21472  ubthlem1  21563  minvecolem3  21569  lnconi  22727  iundisj2f  23228  esumpmono  23735  zetacvg  24048  eldmgm  24055  subfaclim  24123  subfacval3  24124  snmlff  24316  fz0n  24503  nndivsub  25455  nndivlub  25456  nn0prpwlem  25562  nn0prpw  25563  fzmul  25767  incsequz  25782  nnubfi  25784  nninfnub  25785  irrapxlem1  26230  irrapxlem2  26231  pellexlem1  26237  pellexlem5  26241  pellqrex  26287  monotoddzzfi  26350  jm2.24nn  26369  congabseq  26384  acongrep  26390  acongeq  26393  expdiophlem1  26437  idomrootle  26834  idomodle  26835  hashgcdlem  26839  rfcnnnub  27030  fmuldfeq  27036  stoweidlem1  27073  stoweidlem3  27075  stoweidlem11  27083  stoweidlem14  27086  stoweidlem17  27089  stoweidlem20  27092  stoweidlem25  27097  stoweidlem26  27098  stoweidlem30  27102  stoweidlem34  27106  stoweidlem38  27110  stoweidlem42  27114  stoweidlem44  27116  stoweidlem49  27121  stoweidlem51  27123  stoweidlem60  27132  wallispilem3  27139  wallispilem4  27140  wallispilem5  27141  wallispi  27142  wallispi2lem1  27143  wallispi2lem2  27144  stirlinglem1  27146  stirlinglem3  27148  stirlinglem4  27149  stirlinglem6  27151  stirlinglem7  27152  stirlinglem10  27155  stirlinglem11  27156  stirlinglem12  27157  stirlinglem13  27158  stirlingr  27162
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-un 4594  ax-1cn 8885  ax-icn 8886  ax-addcl 8887  ax-addrcl 8888  ax-mulcl 8889  ax-mulrcl 8890  ax-i2m1 8895  ax-1ne0 8896  ax-rrecex 8899  ax-cnre 8900
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3909  df-iun 3988  df-br 4105  df-opab 4159  df-mpt 4160  df-tr 4195  df-eprel 4387  df-id 4391  df-po 4396  df-so 4397  df-fr 4434  df-we 4436  df-ord 4477  df-on 4478  df-lim 4479  df-suc 4480  df-om 4739  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344  df-fv 5345  df-ov 5948  df-recs 6475  df-rdg 6510  df-nn 9837
  Copyright terms: Public domain W3C validator