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

Theorem nnre 10544
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 10541 . 2  |-  NN  C_  RR
21sseli 3482 1  |-  ( A  e.  NN  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1802   RRcr 9489   NNcn 10537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-i2m1 9558  ax-1ne0 9559  ax-rrecex 9562  ax-cnre 9563
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-ov 6280  df-om 6682  df-recs 7040  df-rdg 7074  df-nn 10538
This theorem is referenced by:  nnrei  10546  nn2ge  10562  nnge1  10563  nngt1ne1  10564  nnle1eq1  10565  nngt0  10566  nnnlt1  10567  nndivre  10572  nnrecgt0  10574  nnsub  10575  nnunb  10792  arch  10793  nnrecl  10794  bndndx  10795  0mnnnnn0  10829  nnnegz  10868  elnnz  10875  elz2  10882  gtndiv  10941  prime  10944  btwnz  10966  indstr  11154  qre  11191  rpnnen1lem1  11212  rpnnen1lem2  11213  rpnnen1lem3  11214  rpnnen1lem5  11216  nnrp  11233  qbtwnre  11402  fzo1fzo0n0  11838  elfzo0le  11840  fzonmapblen  11842  ubmelfzo  11855  fzonn0p1p1  11868  elfzom1p1elfzo  11869  ubmelm1fzo  11882  flltdivnn0lt  11939  quoremz  11956  quoremnn0ALT  11958  intfracq  11960  fldiv  11961  modmulnn  11987  modidmul0  11996  addmodid  12010  modifeq2int  12023  modaddmodup  12024  modaddmodlo  12025  nnlesq  12245  digit2  12273  digit1  12274  facdiv  12339  facndiv  12340  faclbnd  12342  faclbnd3  12344  faclbnd4lem4  12348  faclbnd5  12350  bcval5  12370  seqcoll  12486  lswcl  12563  lswccatn0lsw  12581  swrdn0  12629  cshwidxmod  12748  cshwidxm1  12751  repswcshw  12754  isercolllem1  13461  harmonic  13644  efaddlem  13701  rpnnen2lem9  13828  rpnnen2  13831  sqrt2irr  13854  nndivdvds  13864  dvdsle  13903  dvdseq  13905  fzm1ndvds  13910  divalg2  13935  divalgmod  13936  ndvdsadd  13938  modgcd  14046  gcdmultiple  14060  gcdmultiplez  14061  gcdeq  14062  sqgcd  14068  dvdssqlem  14069  isprm3  14098  qredeq  14119  qredeu  14120  isprm5  14125  divdenle  14154  phibndlem  14172  eulerthlem2  14184  oddprm  14211  pythagtriplem10  14216  pythagtriplem12  14222  pythagtriplem14  14224  pythagtriplem16  14226  pythagtriplem19  14229  pclem  14234  pc2dvds  14274  pcmpt  14283  fldivp1  14288  pcbc  14291  infpnlem1  14300  infpn2  14303  prmreclem1  14306  prmreclem3  14308  vdwlem3  14373  ram0  14412  cshwshashlem1  14452  cshwshashlem2  14453  mulgnegnn  16021  odmodnn0  16433  gexdvds  16473  sylow3lem6  16521  prmirredlem  18390  prmirredlemOLD  18393  znidomb  18467  chfacfisf  19222  chfacfisfcpmat  19223  chfacffsupp  19224  chfacfscmul0  19226  chfacfpmmul0  19230  ovolunlem1a  21773  ovoliunlem2  21780  ovolicc2lem3  21796  ovolicc2lem4  21797  iundisj2  21825  dyadss  21869  volsup2  21880  volivth  21882  vitali  21888  ismbf3d  21927  mbfi1fseqlem3  21990  mbfi1fseqlem4  21991  mbfi1fseqlem5  21992  itg2seq  22015  itg2gt0  22033  itg2cnlem1  22034  plyeq0lem  22473  dgreq0  22527  dgrcolem2  22536  elqaalem2  22581  elqaalem3  22582  logtayllem  22905  leibpi  23138  birthdaylem3  23148  basellem1  23219  basellem2  23220  basellem3  23221  basellem6  23224  basellem9  23227  prmorcht  23317  dvdsdivcl  23322  dvdsflsumcom  23329  muinv  23334  vmalelog  23345  chtublem  23351  logfac2  23357  logfaclbnd  23362  pcbcctr  23416  bcmono  23417  bposlem1  23424  bposlem5  23428  bposlem6  23429  bpos  23433  lgsval4a  23458  lgsquadlem1  23494  lgsquadlem2  23495  dchrisum0re  23563  dchrisum0lem1  23566  logdivbnd  23606  ostth2lem1  23668  ostth2lem3  23685  clwwlkel  24658  clwwlkf  24659  clwwlkf1  24661  wwlkext2clwwlk  24668  wwlksubclwwlk  24669  clwwisshclwwlem  24671  numclwlk2lem2f  24968  gxnn0neg  25130  gxmodid  25146  nmounbseqi  25557  nmounbseqiOLD  25558  nmobndseqi  25559  nmobndseqiOLD  25560  ubthlem1  25651  minvecolem3  25657  lnconi  26817  iundisj2f  27314  xrsmulgzz  27532  esumpmono  27951  eulerpartlemb  28173  fibp1  28206  zetacvg  28423  eldmgm  28430  subfaclim  28498  subfacval3  28499  snmlff  28640  fz0n  28976  nndivsub  29890  nndivlub  29891  mblfinlem2  30020  nn0prpwlem  30108  nn0prpw  30109  fzmul  30201  incsequz  30209  nnubfi  30211  nninfnub  30212  irrapxlem1  30726  irrapxlem2  30727  pellexlem1  30733  pellexlem5  30737  pellqrex  30783  monotoddzzfi  30846  jm2.24nn  30865  congabseq  30880  acongrep  30886  acongeq  30889  expdiophlem1  30931  idomrootle  31121  idomodle  31122  hashgcdlem  31126  prmunb2  31160  lcmgcdlem  31181  hashnzfzclim  31196  fmuldfeq  31501  sumnnodd  31540  stoweidlem14  31681  stoweidlem17  31684  stoweidlem20  31687  stoweidlem49  31716  stoweidlem60  31727  wallispilem3  31734  wallispilem4  31735  wallispilem5  31736  wallispi  31737  wallispi2lem1  31738  wallispi2lem2  31739  stirlinglem1  31741  stirlinglem3  31743  stirlinglem4  31744  stirlinglem6  31746  stirlinglem7  31747  stirlinglem10  31750  stirlinglem11  31751  stirlinglem12  31752  stirlinglem13  31753  stirlingr  31757  dirker2re  31759  dirkerval2  31761  dirkerre  31762  dirkertrigeqlem1  31765  fourierdlem66  31840  fourierdlem73  31847  fourierdlem83  31857  fourierdlem87  31861  fourierdlem103  31877  fourierdlem104  31878  fourierdlem111  31885  fouriersw  31899  subsubelfzo0  32172  altgsumbcALT  32650
  Copyright terms: Public domain W3C validator