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

Theorem nnred 10546
Description: A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nnred.1  |-  ( ph  ->  A  e.  NN )
Assertion
Ref Expression
nnred  |-  ( ph  ->  A  e.  RR )

Proof of Theorem nnred
StepHypRef Expression
1 nnssre 10535 . 2  |-  NN  C_  RR
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3487 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823   RRcr 9480   NNcn 10531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-i2m1 9549  ax-1ne0 9550  ax-rrecex 9553  ax-cnre 9554
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-ov 6273  df-om 6674  df-recs 7034  df-rdg 7068  df-nn 10532
This theorem is referenced by:  uzwo3  11178  modmulnn  11995  bernneq3  12276  expmulnbnd  12280  facwordi  12349  faclbnd  12350  faclbnd2  12351  faclbnd3  12352  faclbnd5  12358  faclbnd6  12359  facubnd  12360  facavg  12361  bcp1nk  12377  hashf1  12490  swrds2  12874  isercolllem1  13569  isercoll  13572  o1fsum  13709  climcndslem1  13743  climcndslem2  13744  climcnds  13745  eftabs  13893  efcllem  13895  ege2le3  13907  efcj  13909  eftlub  13926  eflegeo  13938  eirrlem  14019  fzm1ndvds  14122  bitsfzolem  14168  bitsfzo  14169  bitsinv1lem  14175  sadcaddlem  14191  smueqlem  14224  bezoutlem3  14262  bezoutlem4  14263  sqgcd  14280  prmind2  14312  coprm  14325  prmfac1  14343  divdenle  14366  qnumgt0  14367  zsqrtelqelz  14375  hashdvds  14389  eulerthlem2  14396  odzdvds  14406  modprm1div  14408  modprm0  14414  pythagtriplem11  14433  pythagtriplem13  14435  pythagtriplem19  14441  pclem  14446  pcpre1  14450  pcidlem  14479  pcadd  14492  pcmpt  14495  pcmpt2  14496  pcfaclem  14501  pcfac  14502  qexpz  14504  pockthlem  14507  pockthg  14508  prmreclem1  14518  prmreclem3  14520  prmreclem4  14521  prmreclem5  14522  1arithlem4  14528  1arith  14529  4sqlem5  14544  4sqlem6  14545  4sqlem10  14549  mul4sqlem  14555  4sqlem11  14557  4sqlem12  14558  4sqlem13  14559  4sqlem14  14560  4sqlem15  14561  4sqlem16  14562  4sqlem17  14563  vdwlem1  14583  vdwlem3  14585  vdwlem6  14588  vdwlem9  14591  vdwlem10  14592  vdwlem12  14594  vdwnnlem3  14599  ramub1lem1  14628  2expltfac  14661  cshwshashnsame  14672  psgnunilem4  16721  mndodconglem  16764  oddvds  16770  sylow1lem1  16817  sylow1lem5  16821  fislw  16844  efgredlem  16964  gexexlem  17057  zringlpirlem3  18699  prmirredlem  18705  fvmptnn04if  19517  fvmptnn04ifb  19519  fvmptnn04ifc  19520  fvmptnn04ifd  19521  chfacfisf  19522  chfacfisfcpmat  19523  chfacfscmulgsum  19528  chfacfpmmulgsum  19532  lebnumii  21632  lmnn  21868  ovolunlem1a  22073  ovoliunlem1  22079  ovolicc2lem3  22096  ovolicc2lem4  22097  iundisj  22124  voliunlem1  22126  uniioombllem3  22160  dyadf  22166  dyadovol  22168  dyaddisjlem  22170  dyadmaxlem  22172  opnmbllem  22176  vitalilem4  22186  mbfi1fseqlem1  22288  mbfi1fseqlem3  22290  mbfi1fseqlem4  22291  mbfi1fseqlem5  22292  mbfi1fseqlem6  22293  itg2gt0  22333  itg2cnlem2  22335  dgreq0  22828  dgrco  22838  elqaalem2  22882  aaliou3lem2  22905  aaliou3lem8  22907  aaliou3lem9  22912  leibpi  23470  log2tlbnd  23473  birthdaylem3  23481  amgm  23518  emcllem2  23524  harmonicbnd4  23538  wilthlem1  23540  ftalem5  23548  basellem1  23552  basellem2  23553  basellem3  23554  basellem4  23555  basellem5  23556  basellem6  23557  basellem8  23559  chtge0  23584  chtwordi  23628  vma1  23638  dvdsdivcl  23655  dvdsflf1o  23661  dvdsflsumcom  23662  fsumfldivdiaglem  23663  sgmmul  23674  chtublem  23684  fsumvma2  23687  logfac2  23690  chpchtsum  23692  chpub  23693  logfaclbnd  23695  logexprlim  23698  mersenne  23700  perfectlem2  23703  dchrelbas4  23716  bposlem1  23757  bposlem2  23758  bposlem3  23759  bposlem4  23760  bposlem5  23761  bposlem6  23762  bposlem7  23763  bposlem9  23765  lgslem1  23769  lgslem4  23772  lgsval2lem  23779  lgsdirprm  23802  lgsdir  23803  lgsne0  23806  lgsqrlem2  23815  lgseisenlem1  23822  lgseisenlem2  23823  lgseisenlem3  23824  lgseisenlem4  23825  lgseisen  23826  lgsquadlem1  23827  lgsquadlem2  23828  lgsquadlem3  23829  m1lgs  23835  2sqlem3  23839  2sqlem8  23845  2sqblem  23850  chebbnd1lem1  23852  chebbnd1lem3  23854  chtppilimlem1  23856  rplogsumlem1  23867  rplogsumlem2  23868  dchrisum0lem1a  23869  rpvmasumlem  23870  dchrisumlema  23871  dchrisumlem1  23872  dchrisumlem2  23873  dchrisumlem3  23874  dchrvmasumiflem1  23884  dchrisum0flblem2  23892  dchrisum0re  23896  dchrisum0lem1b  23898  dchrisum0lem1  23899  dirith2  23911  selbergb  23932  selberg2lem  23933  logdivbnd  23939  selberg3lem2  23941  selberg4lem1  23943  pntrsumo1  23948  pntrsumbnd2  23950  pntrlog2bndlem1  23960  pntrlog2bndlem2  23961  pntrlog2bndlem3  23962  pntrlog2bndlem4  23963  pntrlog2bndlem5  23964  pntpbnd1a  23968  pntpbnd1  23969  pntibndlem2a  23973  pntibndlem2  23974  pntlemg  23981  pntlemh  23982  pntlemj  23986  pntlemf  23988  ostth2lem1  24001  padicabvf  24014  padicabvcxp  24015  ostth2lem2  24017  ostth2lem3  24018  ostth2lem4  24019  ostth2  24020  ostth3  24021  eupap1  25178  numclwwlk5  25314  numclwwlk7  25316  ubthlem2  25985  minvecolem4  25994  iundisjf  27659  ssnnssfz  27831  iundisjfi  27835  2sqmod  27870  esumcst  28292  oddpwdc  28557  eulerpartlems  28563  eulerpartlemgc  28565  fiblem  28601  dstfrvunirn  28677  dstfrvclim1  28680  ballotlemimin  28708  lgamgulmlem1  28835  lgamgulmlem2  28836  lgamgulmlem3  28837  lgamgulmlem4  28838  lgamgulmlem5  28839  lgamgulmlem6  28840  lgamucov  28844  lgamcvg2  28861  subfaclim  28896  subfacval3  28897  erdszelem7  28905  erdszelem8  28906  erdsze2lem2  28912  cvmliftlem2  28995  cvmliftlem6  28999  cvmliftlem7  29000  cvmliftlem8  29001  cvmliftlem9  29002  cvmliftlem10  29003  cvmliftlem13  29005  faclimlem2  29410  faclim2  29414  opnmbllem0  30290  mblfinlem2  30292  nn0prpwlem  30380  incsequz  30481  nninfnub  30484  irrapxlem3  30999  irrapxlem4  31000  irrapxlem5  31001  pellexlem2  31005  pellexlem6  31009  pell14qrgt0  31034  pell14qrgapw  31051  pellfundgt1  31058  rmspecsqrtnq  31081  ltrmxnn0  31126  jm3.1lem1  31198  jm3.1lem3  31200  dgraa0p  31339  lcmgcdlem  31453  hashnzfz2  31467  rfcnnnub  31651  nnxrd  31659  fzisoeu  31739  fsumnncl  31811  sumnnodd  31875  stoweidlem1  32022  stoweidlem3  32024  stoweidlem11  32032  stoweidlem17  32038  stoweidlem20  32041  stoweidlem25  32046  stoweidlem26  32047  stoweidlem34  32055  stoweidlem38  32059  stoweidlem42  32063  stoweidlem44  32065  stoweidlem51  32072  stoweidlem59  32080  stoweidlem60  32081  wallispi  32091  wallispi2  32094  stirlinglem3  32097  stirlinglem4  32098  stirlinglem8  32102  stirlinglem10  32104  stirlinglem12  32106  stirlinglem15  32109  dirkertrigeqlem2  32120  dirkertrigeqlem3  32121  dirkercncflem2  32125  fourierdlem11  32139  fourierdlem14  32142  fourierdlem15  32143  fourierdlem20  32148  fourierdlem31  32159  fourierdlem64  32192  fourierdlem93  32221  fourierdlem95  32223  fourierdlem103  32231  fourierdlem104  32232  fourierdlem112  32240  sqwvfourb  32251  etransclem3  32259  etransclem19  32275  etransclem23  32279  etransclem24  32280  etransclem25  32281  etransclem32  32288  etransclem35  32291  etransclem41  32297  etransclem48  32304  ztprmneprm  33190  pgrple2abl  33212  nno  33392  logbpw2m1  33442  nnpw2pmod  33458  nnolog2flm1  33465  blennngt2o2  33467
  Copyright terms: Public domain W3C validator