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

Theorem nnre 10543
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 10540 . 2  |-  NN  C_  RR
21sseli 3500 1  |-  ( A  e.  NN  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   RRcr 9491   NNcn 10536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-i2m1 9560  ax-1ne0 9561  ax-rrecex 9564  ax-cnre 9565
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-ov 6287  df-om 6685  df-recs 7042  df-rdg 7076  df-nn 10537
This theorem is referenced by:  nnrei  10545  nn2ge  10561  nnge1  10562  nngt1ne1  10563  nnle1eq1  10564  nngt0  10565  nnnlt1  10566  nndivre  10571  nnrecgt0  10573  nnsub  10574  nnunb  10791  arch  10792  nnrecl  10793  bndndx  10794  0mnnnnn0  10828  nnnegz  10867  elnnz  10874  elz2  10881  gtndiv  10938  prime  10941  btwnz  10963  indstr  11150  qre  11187  rpnnen1lem1  11208  rpnnen1lem2  11209  rpnnen1lem3  11210  rpnnen1lem5  11212  nnrp  11229  qbtwnre  11398  fzo1fzo0n0  11832  elfzo0le  11834  fzonmapblen  11836  ubmelfzo  11849  fzonn0p1p1  11862  elfzom1p1elfzo  11863  ubmelm1fzo  11876  flltdivnn0lt  11933  quoremz  11950  quoremnn0ALT  11952  intfracq  11954  fldiv  11955  modmulnn  11981  modidmul0  11990  addmodid  12004  modifeq2int  12017  modaddmodup  12018  modaddmodlo  12019  nnlesq  12239  digit2  12267  digit1  12268  facdiv  12333  facndiv  12334  faclbnd  12336  faclbnd3  12338  faclbnd4lem4  12342  faclbnd5  12344  bcval5  12364  seqcoll  12478  lswcl  12554  lswccatn0lsw  12571  swrdn0  12618  cshwidxmod  12737  cshwidxm1  12740  repswcshw  12743  isercolllem1  13450  harmonic  13633  efaddlem  13690  rpnnen2lem9  13817  rpnnen2  13820  sqrt2irr  13843  nndivdvds  13853  dvdsle  13890  dvdseq  13892  fzm1ndvds  13897  divalg2  13922  divalgmod  13923  ndvdsadd  13925  modgcd  14033  gcdmultiple  14047  gcdmultiplez  14048  gcdeq  14049  sqgcd  14055  dvdssqlem  14056  isprm3  14085  qredeq  14106  qredeu  14107  isprm5  14112  divdenle  14141  phibndlem  14159  eulerthlem2  14171  oddprm  14198  pythagtriplem10  14203  pythagtriplem12  14209  pythagtriplem14  14211  pythagtriplem16  14213  pythagtriplem19  14216  pclem  14221  pc2dvds  14261  pcmpt  14270  fldivp1  14275  pcbc  14278  infpnlem1  14287  infpn2  14290  prmreclem1  14293  prmreclem3  14295  vdwlem3  14360  ram0  14399  cshwshashlem1  14438  cshwshashlem2  14439  mulgnegnn  15962  odmodnn0  16370  gexdvds  16410  sylow3lem6  16458  prmirredlem  18318  prmirredlemOLD  18321  znidomb  18395  chfacfisf  19150  chfacfisfcpmat  19151  chfacffsupp  19152  chfacfscmul0  19154  chfacfpmmul0  19158  ovolunlem1a  21670  ovoliunlem2  21677  ovolicc2lem3  21693  ovolicc2lem4  21694  iundisj2  21722  dyadss  21766  volsup2  21777  volivth  21779  vitali  21785  ismbf3d  21824  mbfi1fseqlem3  21887  mbfi1fseqlem4  21888  mbfi1fseqlem5  21889  itg2seq  21912  itg2gt0  21930  itg2cnlem1  21931  plyeq0lem  22370  dgreq0  22424  dgrcolem2  22433  elqaalem2  22478  elqaalem3  22479  logtayllem  22796  leibpi  23029  birthdaylem3  23039  basellem1  23110  basellem2  23111  basellem3  23112  basellem6  23115  basellem9  23118  prmorcht  23208  dvdsdivcl  23213  dvdsflsumcom  23220  muinv  23225  vmalelog  23236  chtublem  23242  logfac2  23248  logfaclbnd  23253  pcbcctr  23307  bcmono  23308  bposlem1  23315  bposlem5  23319  bposlem6  23320  bpos  23324  lgsval4a  23349  lgsquadlem1  23385  lgsquadlem2  23386  dchrisum0re  23454  dchrisum0lem1  23457  logdivbnd  23497  ostth2lem1  23559  ostth2lem3  23576  clwwlkel  24497  clwwlkf  24498  clwwlkf1  24500  wwlkext2clwwlk  24507  wwlksubclwwlk  24508  clwwisshclwwlem  24510  numclwlk2lem2f  24808  gxnn0neg  24969  gxmodid  24985  nmounbseqi  25396  nmounbseqiOLD  25397  nmobndseqi  25398  nmobndseqiOLD  25399  ubthlem1  25490  minvecolem3  25496  lnconi  26656  iundisj2f  27150  esumpmono  27753  eulerpartlemb  27975  fibp1  28008  zetacvg  28225  eldmgm  28232  subfaclim  28300  subfacval3  28301  snmlff  28442  fz0n  28613  nndivsub  29527  nndivlub  29528  mblfinlem2  29657  nn0prpwlem  29745  nn0prpw  29746  fzmul  29864  incsequz  29872  nnubfi  29874  nninfnub  29875  irrapxlem1  30390  irrapxlem2  30391  pellexlem1  30397  pellexlem5  30401  pellqrex  30447  monotoddzzfi  30510  jm2.24nn  30529  congabseq  30544  acongrep  30550  acongeq  30553  expdiophlem1  30595  idomrootle  30785  idomodle  30786  hashgcdlem  30790  prmunb2  30822  lcmgcdlem  30840  hashnzfzclim  30855  fmuldfeq  31161  sumnnodd  31200  stoweidlem14  31342  stoweidlem17  31345  stoweidlem20  31348  stoweidlem49  31377  stoweidlem60  31388  wallispilem3  31395  wallispilem4  31396  wallispilem5  31397  wallispi  31398  wallispi2lem1  31399  wallispi2lem2  31400  stirlinglem1  31402  stirlinglem3  31404  stirlinglem4  31405  stirlinglem6  31407  stirlinglem7  31408  stirlinglem10  31411  stirlinglem11  31412  stirlinglem12  31413  stirlinglem13  31414  stirlingr  31418  dirker2re  31420  dirkerval2  31422  dirkerre  31423  dirkertrigeqlem1  31426  fourierdlem66  31501  fourierdlem73  31508  fourierdlem83  31518  fourierdlem87  31522  fourierdlem103  31538  fourierdlem104  31539  fourierdlem111  31546  fouriersw  31560  subsubelfzo0  31833  altgsumbcALT  32038
  Copyright terms: Public domain W3C validator