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

Theorem nnre 10644
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 10641 . 2  |-  NN  C_  RR
21sseli 3440 1  |-  ( A  e.  NN  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898   RRcr 9564   NNcn 10637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-i2m1 9633  ax-1ne0 9634  ax-rrecex 9637  ax-cnre 9638
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6318  df-om 6720  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-nn 10638
This theorem is referenced by:  nnrei  10646  nn2ge  10662  nnge1  10663  nngt1ne1  10664  nnle1eq1  10665  nngt0  10666  nnnlt1  10667  nnnle0  10668  nndivre  10673  nnrecgt0  10675  nnsub  10676  nnunb  10894  arch  10895  nnrecl  10896  bndndx  10897  0mnnnnn0  10931  nnnegz  10969  elnnz  10976  elz2  10983  gtndiv  11042  prime  11045  btwnz  11066  indstr  11256  qre  11298  rpnnen1lem1  11319  rpnnen1lem2  11320  rpnnen1lem3  11321  rpnnen1lem5  11323  nnrp  11340  qbtwnre  11521  fzo1fzo0n0  11988  elfzo0le  11990  fzonmapblen  11992  ubmelfzo  12010  fzonn0p1p1  12023  elfzom1p1elfzo  12024  ubmelm1fzo  12038  flltdivnn0lt  12097  quoremz  12114  quoremnn0ALT  12116  intfracq  12118  fldiv  12119  modmulnn  12146  modidmul0OLD  12155  addmodid  12171  modifeq2int  12184  modaddmodup  12185  modaddmodlo  12186  nnlesq  12410  digit2  12437  digit1  12438  facdiv  12504  facndiv  12505  faclbnd  12507  faclbnd3  12509  faclbnd4lem4  12513  faclbnd5  12515  bcval5  12535  seqcoll  12660  cshwidxmod  12942  cshwidxm1  12945  repswcshw  12948  isercolllem1  13777  harmonic  13966  efaddlem  14196  rpnnen2lem9  14324  rpnnen2  14327  sqrt2irr  14350  nndivdvds  14360  dvdsle  14399  dvdseq  14401  fzm1ndvds  14406  divalg2  14435  divalgmod  14436  ndvdsadd  14438  modgcd  14549  gcdmultiple  14567  gcdmultiplez  14568  gcdeq  14569  sqgcd  14575  dvdssqlem  14576  lcmgcdlem  14620  lcmf  14655  isprm3  14682  prmdvdsfz  14698  isprm5  14700  coprmgcdb  14703  qredeq  14712  qredeu  14713  ncoprmlnprm  14726  divdenle  14747  phibndlem  14767  eulerthlem2  14779  oddprm  14814  pythagtriplem10  14819  pythagtriplem12  14825  pythagtriplem14  14827  pythagtriplem16  14829  pythagtriplem19  14832  pclem  14837  pc2dvds  14877  pcmpt  14886  fldivp1  14891  pcbc  14894  infpnlem1  14903  infpn2  14906  prmreclem1  14909  prmreclem3  14911  vdwlem3  14982  ram0  15029  prmgaplem4  15073  prmgaplem7  15076  cshwshashlem1  15115  cshwshashlem2  15116  mulgnegnn  16817  odmodnn0  17238  gexdvds  17284  sylow3lem6  17333  prmirredlem  19113  znidomb  19181  chfacfisf  19927  chfacfisfcpmat  19928  chfacffsupp  19929  chfacfscmul0  19931  chfacfpmmul0  19935  ovolunlem1a  22498  ovoliunlem2  22505  ovolicc2lem3  22521  ovolicc2lem4OLD  22522  ovolicc2lem4  22523  iundisj2  22551  dyadss  22601  volsup2  22612  volivth  22614  vitali  22620  ismbf3d  22659  mbfi1fseqlem3  22724  mbfi1fseqlem4  22725  mbfi1fseqlem5  22726  itg2seq  22749  itg2gt0  22767  itg2cnlem1  22768  plyeq0lem  23213  dgreq0  23268  dgrcolem2  23277  elqaalem2  23322  elqaalem3  23323  elqaalem2OLD  23325  elqaalem3OLD  23326  logtayllem  23653  leibpi  23917  birthdaylem3  23928  zetacvg  23989  eldmgm  23996  basellem1  24056  basellem2  24057  basellem3  24058  basellem6  24061  basellem9  24064  prmorcht  24154  dvdsdivcl  24159  dvdsflsumcom  24166  muinv  24171  vmalelog  24182  chtublem  24188  logfac2  24194  logfaclbnd  24199  pcbcctr  24253  bcmono  24254  bposlem1  24261  bposlem5  24265  bposlem6  24266  bpos  24270  lgsval4a  24295  lgsquadlem1  24331  lgsquadlem2  24332  dchrisum0re  24400  dchrisum0lem1  24403  logdivbnd  24443  ostth2lem1  24505  ostth2lem3  24522  clwwlkel  25570  clwwlkf  25571  clwwlkf1  25573  wwlkext2clwwlk  25580  wwlksubclwwlk  25581  clwwisshclwwlem  25583  numclwlk2lem2f  25880  gxnn0neg  26040  gxmodid  26056  nmounbseqi  26467  nmounbseqiALT  26468  nmobndseqi  26469  nmobndseqiALT  26470  ubthlem1  26561  minvecolem3  26567  minvecolem3OLD  26577  lnconi  27735  iundisj2f  28249  xrsmulgzz  28489  esumpmono  28949  eulerpartlemb  29250  fibp1  29283  subfaclim  29960  subfacval3  29961  snmlff  30101  fz0n  30413  bcprod  30423  nn0prpwlem  31027  nn0prpw  31028  nndivsub  31166  nndivlub  31167  poimirlem13  31998  poimirlem14  31999  poimirlem31  32016  poimirlem32  32017  mblfinlem2  32023  fzmul  32114  incsequz  32122  nnubfi  32124  nninfnub  32125  irrapxlem1  35711  irrapxlem2  35712  pellexlem1  35718  pellexlem5  35722  pellqrex  35771  monotoddzzfi  35835  jm2.24nn  35854  congabseq  35869  acongrep  35875  acongeq  35878  expdiophlem1  35921  idomrootle  36114  idomodle  36115  hashgcdlem  36119  relexpmulnn  36346  prmunb2  36703  hashnzfzclim  36715  fmuldfeq  37699  sumnnodd  37748  stoweidlem14  37912  stoweidlem17  37915  stoweidlem20  37918  stoweidlem49  37948  stoweidlem60  37959  wallispilem3  37967  wallispilem4  37968  wallispilem5  37969  wallispi  37970  wallispi2lem1  37971  wallispi2lem2  37972  stirlinglem1  37974  stirlinglem3  37976  stirlinglem4  37977  stirlinglem6  37979  stirlinglem7  37980  stirlinglem10  37983  stirlinglem11  37984  stirlinglem12  37985  stirlinglem13  37986  stirlingr  37990  dirker2re  37992  dirkerval2  37994  dirkerre  37995  dirkertrigeqlem1  37998  fourierdlem66  38074  fourierdlem73  38081  fourierdlem83  38091  fourierdlem87  38095  fourierdlem103  38111  fourierdlem104  38112  fourierdlem111  38119  fouriersw  38133  etransclem24  38161  sge0rpcpnf  38301  hoicvr  38408  hoicvrrex  38416  gcdzeq  38831  nn0oALTV  38863  nnsum4primes4  38922  nnsum4primesprm  38924  nnsum4primesgbe  38926  nnsum4primesle9  38928  bgoldbachlt  38944  tgoldbach  38949  subsubelfzo0  39104  pthdlem2lem  39793  altgsumbcALT  40407  modn0mul  40596  m1modmmod  40597  difmodm1lt  40598  nno  40601  nnlog2ge0lt1  40650  logbpw2m1  40651  blennn  40659  blennnelnn  40660  nnpw2pmod  40667  nnolog2flm1  40674  digvalnn0  40683  dignn0fr  40685  dignn0ldlem  40686  dignnld  40687  dig2nn1st  40689
  Copyright terms: Public domain W3C validator