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

Theorem nnre 9753
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 9750 . 2  |-  NN  C_  RR
21sseli 3176 1  |-  ( A  e.  NN  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   RRcr 8736   NNcn 9746
This theorem is referenced by:  nnrei  9755  nn2ge  9771  nnge1  9772  nngt1ne1  9773  nnle1eq1  9774  nngt0  9775  nnnlt1  9776  nndivre  9781  nnrecgt0  9783  nnsub  9784  nnunb  9961  arch  9962  nnrecl  9963  bndndx  9964  nnnegz  10027  elnnz  10034  elz2  10040  gtndiv  10089  prime  10092  btwnz  10114  indstr  10287  qre  10321  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem5  10346  nnrp  10363  qbtwnre  10526  quoremz  10959  quoremnn0  10960  quoremnn0ALT  10961  intfracq  10963  fldiv  10964  modmulnn  10988  nnlesq  11206  digit2  11234  digit1  11235  facdiv  11300  facndiv  11301  faclbnd  11303  faclbnd3  11305  faclbnd4lem4  11309  faclbnd5  11311  bcval5  11330  seqcoll  11401  isercolllem1  12138  harmonic  12317  efaddlem  12374  rpnnen2lem9  12501  rpnnen2  12504  sqr2irr  12527  nndivdvds  12537  dvdsle  12574  dvdseq  12576  fzm1ndvds  12580  divalg2  12604  divalgmod  12605  ndvdsadd  12607  modgcd  12715  gcdmultiple  12729  gcdmultiplez  12730  gcdeq  12731  sqgcd  12737  dvdssqlem  12738  isprm3  12767  qredeq  12785  qredeu  12786  isprm5  12791  divdenle  12820  phibndlem  12838  eulerthlem2  12850  oddprm  12868  pythagtriplem10  12873  pythagtriplem12  12879  pythagtriplem14  12881  pythagtriplem16  12883  pythagtriplem19  12886  pclem  12891  pc2dvds  12931  pcmpt  12940  fldivp1  12945  pcbc  12948  infpnlem1  12957  infpn2  12960  prmreclem1  12963  prmreclem3  12965  vdwlem3  13030  ram0  13069  mulgnegnn  14577  odmodnn0  14855  gexdvds  14895  sylow3lem6  14943  prmirredlem  16446  znidomb  16515  ovolunlem1a  18855  ovoliunlem2  18862  ovolicc2lem3  18878  ovolicc2lem4  18879  iundisj2  18906  dyadss  18949  volsup2  18960  volivth  18962  vitali  18968  ismbf3d  19009  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  itg2seq  19097  itg2gt0  19115  itg2cnlem1  19116  plyeq0lem  19592  dgreq0  19646  dgrcolem2  19655  elqaalem2  19700  elqaalem3  19701  logtayllem  20006  leibpi  20238  birthdaylem3  20248  basellem1  20318  basellem2  20319  basellem3  20320  basellem6  20323  basellem9  20326  prmorcht  20416  dvdsdivcl  20421  dvdsflsumcom  20428  muinv  20433  vmalelog  20444  chtublem  20450  logfac2  20456  logfaclbnd  20461  pcbcctr  20515  bcmono  20516  bposlem1  20523  bposlem5  20527  bposlem6  20528  bpos  20532  lgsval4a  20557  lgsquadlem1  20593  lgsquadlem2  20594  dchrisum0re  20662  dchrisum0lem1  20665  logdivbnd  20705  ostth2lem1  20767  ostth2lem3  20784  gxnn0neg  20930  gxmodid  20946  nmounbseqi  21355  nmounbseqiOLD  21356  nmobndseqi  21357  nmobndseqiOLD  21358  ubthlem1  21449  minvecolem3  21455  lnconi  22613  iundisj2f  23366  esumpmono  23447  zetacvg  23689  eldmgm  23694  subfaclim  23719  subfacval3  23720  snmlff  23912  fz0n  24097  nndivsub  24896  nndivlub  24897  nn0prpwlem  26238  nn0prpw  26239  fzmul  26443  incsequz  26458  nnubfi  26460  nninfnub  26461  irrapxlem1  26907  irrapxlem2  26908  pellexlem1  26914  pellexlem5  26918  pellqrex  26964  monotoddzzfi  27027  jm2.24nn  27046  congabseq  27061  acongrep  27067  acongeq  27070  expdiophlem1  27114  idomrootle  27511  idomodle  27512  hashgcdlem  27516  rfcnnnub  27707  fmuldfeq  27713  stoweidlem1  27750  stoweidlem3  27752  stoweidlem11  27760  stoweidlem14  27763  stoweidlem17  27766  stoweidlem20  27769  stoweidlem25  27774  stoweidlem26  27775  stoweidlem30  27779  stoweidlem34  27783  stoweidlem38  27787  stoweidlem42  27791  stoweidlem44  27793  stoweidlem49  27798  stoweidlem51  27800  stoweidlem60  27809  wallispilem3  27816  wallispilem4  27817  wallispilem5  27818  wallispi  27819  wallispi2lem1  27820  wallispi2lem2  27821  stirlinglem1  27823  stirlinglem3  27825  stirlinglem4  27826  stirlinglem6  27828  stirlinglem7  27829  stirlinglem10  27832  stirlinglem11  27833  stirlinglem12  27834  stirlinglem13  27835  stirlingr  27839
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-i2m1 8805  ax-1ne0 8806  ax-rrecex 8809  ax-cnre 8810
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 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-recs 6388  df-rdg 6423  df-nn 9747
  Copyright terms: Public domain W3C validator