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

Theorem nnred 10624
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 10613 . 2  |-  NN  C_  RR
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3430 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1887   RRcr 9538   NNcn 10609
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-i2m1 9607  ax-1ne0 9608  ax-rrecex 9611  ax-cnre 9612
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-ov 6293  df-om 6693  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-nn 10610
This theorem is referenced by:  uzwo3  11259  modmulnn  12114  bernneq3  12400  expmulnbnd  12404  facwordi  12474  faclbnd  12475  faclbnd2  12476  faclbnd3  12477  faclbnd5  12483  faclbnd6  12484  facubnd  12485  facavg  12486  bcp1nk  12502  hashf1  12620  swrds2  13020  isercolllem1  13728  isercoll  13731  o1fsum  13873  climcndslem1  13907  climcndslem2  13908  climcnds  13909  eftabs  14130  efcllem  14132  ege2le3  14144  efcj  14146  eftlub  14163  eflegeo  14175  eirrlem  14256  fzm1ndvds  14357  bitsfzolem  14407  bitsfzolemOLD  14408  bitsfzo  14409  bitsinv1lem  14415  sadcaddlem  14431  smueqlem  14464  bezoutlem3OLD  14505  bezoutlem4OLD  14506  bezoutlem3  14508  bezoutlem4  14509  sqgcd  14526  lcmgcdlem  14571  lcmf  14606  prmind2  14635  coprm  14657  prmfac1  14671  divdenle  14698  qnumgt0  14699  zsqrtelqelz  14707  hashdvds  14723  eulerthlem2  14730  odzdvds  14740  odzdvdsOLD  14746  modprm1div  14748  vfermltl  14752  modprm0  14756  pythagtriplem11  14775  pythagtriplem13  14777  pythagtriplem19  14783  pclem  14788  pcpre1  14792  pcidlem  14821  pcadd  14834  pcmpt  14837  pcmpt2  14838  pcfaclem  14843  pcfac  14844  qexpz  14846  pockthlem  14849  pockthg  14850  prmreclem1  14860  prmreclem3  14862  prmreclem4  14863  prmreclem5  14864  1arithlem4  14870  1arith  14871  4sqlem5  14886  4sqlem6  14887  4sqlem10  14891  mul4sqlem  14897  4sqlem11  14899  4sqlem12  14900  4sqlem13OLD  14901  4sqlem14OLD  14902  4sqlem15OLD  14903  4sqlem16OLD  14904  4sqlem17OLD  14905  4sqlem13  14907  4sqlem14  14908  4sqlem15  14909  4sqlem16  14910  4sqlem17  14911  vdwlem1  14931  vdwlem3  14933  vdwlem6  14936  vdwlem9  14939  vdwlem10  14940  vdwlem12  14942  vdwnnlem3  14947  ramub1lem1  14984  prmolefac  15004  prmorlefacOLD  15018  prmgaplem4  15024  prmgaplem5  15025  prmgaplem6  15026  prmgaplem8  15028  2expltfac  15063  cshwshashnsame  15074  psgnunilem4  17138  mndodconglem  17190  oddvds  17196  sylow1lem1  17250  sylow1lem5  17254  fislw  17277  efgredlem  17397  gexexlem  17490  zringlpirlem3OLD  19055  zringlpirlem3  19057  prmirredlem  19064  fvmptnn04if  19873  fvmptnn04ifb  19875  fvmptnn04ifc  19876  fvmptnn04ifd  19877  chfacfisf  19878  chfacfisfcpmat  19879  chfacfscmulgsum  19884  chfacfpmmulgsum  19888  lebnumii  21997  lmnn  22233  ovolunlem1a  22449  ovoliunlem1  22455  ovolicc2lem3  22472  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  iundisj  22501  voliunlem1  22503  uniioombllem3  22543  dyadf  22549  dyadovol  22551  dyaddisjlem  22553  dyadmaxlem  22555  opnmbllem  22559  vitalilem4  22569  mbfi1fseqlem1  22673  mbfi1fseqlem3  22675  mbfi1fseqlem4  22676  mbfi1fseqlem5  22677  mbfi1fseqlem6  22678  itg2gt0  22718  itg2cnlem2  22720  dgreq0  23219  dgrco  23229  elqaalem2  23273  elqaalem2OLD  23276  aaliou3lem2  23299  aaliou3lem8  23301  aaliou3lem9  23306  leibpi  23868  log2tlbnd  23871  birthdaylem3  23879  amgm  23916  emcllem2  23922  harmonicbnd4  23936  lgamgulmlem1  23954  lgamgulmlem2  23955  lgamgulmlem3  23956  lgamgulmlem4  23957  lgamgulmlem5  23958  lgamgulmlem6  23959  lgamucov  23963  lgamcvg2  23980  wilthlem1  23993  ftalem5  24001  ftalem5OLD  24003  basellem1  24007  basellem2  24008  basellem3  24009  basellem4  24010  basellem5  24011  basellem6  24012  basellem8  24014  chtge0  24039  chtwordi  24083  vma1  24093  dvdsdivcl  24110  dvdsflf1o  24116  dvdsflsumcom  24117  fsumfldivdiaglem  24118  sgmmul  24129  chtublem  24139  fsumvma2  24142  logfac2  24145  chpchtsum  24147  chpub  24148  logfaclbnd  24150  logexprlim  24153  mersenne  24155  perfectlem2  24158  dchrelbas4  24171  bposlem1  24212  bposlem2  24213  bposlem3  24214  bposlem4  24215  bposlem5  24216  bposlem6  24217  bposlem7  24218  bposlem9  24220  lgslem1  24224  lgslem4  24227  lgsval2lem  24234  lgsdirprm  24257  lgsdir  24258  lgsne0  24261  lgsqrlem2  24270  lgseisenlem1  24277  lgseisenlem2  24278  lgseisenlem3  24279  lgseisenlem4  24280  lgseisen  24281  lgsquadlem1  24282  lgsquadlem2  24283  lgsquadlem3  24284  m1lgs  24290  2sqlem3  24294  2sqlem8  24300  2sqblem  24305  chebbnd1lem1  24307  chebbnd1lem3  24309  chtppilimlem1  24311  rplogsumlem1  24322  rplogsumlem2  24323  dchrisum0lem1a  24324  rpvmasumlem  24325  dchrisumlema  24326  dchrisumlem1  24327  dchrisumlem2  24328  dchrisumlem3  24329  dchrvmasumiflem1  24339  dchrisum0flblem2  24347  dchrisum0re  24351  dchrisum0lem1b  24353  dchrisum0lem1  24354  dirith2  24366  selbergb  24387  selberg2lem  24388  logdivbnd  24394  selberg3lem2  24396  selberg4lem1  24398  pntrsumo1  24403  pntrsumbnd2  24405  pntrlog2bndlem1  24415  pntrlog2bndlem2  24416  pntrlog2bndlem3  24417  pntrlog2bndlem4  24418  pntrlog2bndlem5  24419  pntpbnd1a  24423  pntpbnd1  24424  pntibndlem2a  24428  pntibndlem2  24429  pntlemg  24436  pntlemh  24437  pntlemj  24441  pntlemf  24443  ostth2lem1  24456  padicabvf  24469  padicabvcxp  24470  ostth2lem2  24472  ostth2lem3  24473  ostth2lem4  24474  ostth2  24475  ostth3  24476  eupap1  25704  numclwwlk5  25840  numclwwlk7  25842  ubthlem2  26513  minvecolem4  26522  minvecolem4OLD  26532  iundisjf  28199  ssnnssfz  28367  iundisjfi  28372  2sqmod  28409  pmtrto1cl  28612  psgnfzto1stlem  28613  fzto1st1  28615  fzto1st  28616  psgnfzto1st  28618  smatrcl  28622  smattr  28625  smatbl  28626  smatbr  28627  1smat1  28630  submateqlem1  28633  submateqlem2  28634  submateq  28635  esumcst  28884  fiunelros  28996  oddpwdc  29187  eulerpartlems  29193  eulerpartlemgc  29195  fiblem  29231  dstfrvunirn  29307  dstfrvclim1  29310  ballotlemimin  29338  ballotlemiminOLD  29376  subfaclim  29911  subfacval3  29912  erdszelem7  29920  erdszelem8  29921  erdsze2lem2  29927  cvmliftlem2  30009  cvmliftlem6  30013  cvmliftlem7  30014  cvmliftlem8  30015  cvmliftlem9  30016  cvmliftlem10  30017  cvmliftlem13  30019  bcprod  30374  bccolsum  30375  faclimlem2  30380  faclim2  30384  nn0prpwlem  30978  poimirlem3  31943  poimirlem6  31946  poimirlem7  31947  poimirlem8  31948  poimirlem9  31949  poimirlem10  31950  poimirlem11  31951  poimirlem12  31952  poimirlem13  31953  poimirlem15  31955  poimirlem16  31956  poimirlem17  31957  poimirlem19  31959  poimirlem20  31960  poimirlem21  31961  poimirlem22  31962  poimirlem23  31963  poimirlem26  31966  poimirlem28  31968  opnmbllem0  31976  mblfinlem2  31978  incsequz  32077  nninfnub  32080  irrapxlem3  35668  irrapxlem4  35669  irrapxlem5  35670  pellexlem2  35674  pellexlem6  35678  pell14qrgt0  35705  pell14qrgapw  35722  pellfundgt1  35731  rmspecsqrtnq  35754  ltrmxnn0  35799  jm3.1lem1  35872  jm3.1lem3  35874  dgraa0p  36015  hashnzfz2  36670  rfcnnnub  37357  nnxrd  37363  fzisoeu  37518  fsumnncl  37650  sumnnodd  37710  stoweidlem1  37861  stoweidlem3  37863  stoweidlem11  37871  stoweidlem17  37877  stoweidlem20  37880  stoweidlem25  37885  stoweidlem26  37886  stoweidlem34  37895  stoweidlem38  37899  stoweidlem42  37903  stoweidlem44  37905  stoweidlem51  37912  stoweidlem59  37920  stoweidlem60  37921  wallispi  37932  wallispi2  37935  stirlinglem3  37938  stirlinglem4  37939  stirlinglem8  37943  stirlinglem10  37945  stirlinglem12  37947  stirlinglem15  37950  dirkertrigeqlem2  37961  dirkertrigeqlem3  37962  dirkercncflem2  37966  fourierdlem11  37980  fourierdlem14  37983  fourierdlem15  37984  fourierdlem20  37989  fourierdlem31  38000  fourierdlem31OLD  38001  fourierdlem64  38034  fourierdlem93  38063  fourierdlem95  38065  fourierdlem103  38073  fourierdlem104  38074  fourierdlem112  38082  sqwvfourb  38093  etransclem3  38102  etransclem19  38118  etransclem23  38122  etransclem24  38123  etransclem25  38124  etransclem32  38131  etransclem35  38134  etransclem41  38140  etransclem48OLD  38147  etransclem48  38148  qndenserrnbllem  38163  hoiqssbllem1  38444  hoiqssbllem2  38445  iccpartlt  38738  iccpartgt  38741  perfectALTVlem2  38844  gboge7  38864  proththdlem  38913  ztprmneprm  40181  pgrple2abl  40203  nno  40381  logbpw2m1  40431  nnpw2pmod  40447  nnolog2flm1  40454  blennngt2o2  40456
  Copyright terms: Public domain W3C validator