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

Theorem nnred 10613
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 10602 . 2  |-  NN  C_  RR
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3459 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1867   RRcr 9527   NNcn 10598
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-i2m1 9596  ax-1ne0 9597  ax-rrecex 9600  ax-cnre 9601
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-iun 4295  df-br 4418  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4756  df-id 4760  df-po 4766  df-so 4767  df-fr 4804  df-we 4806  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-pred 5390  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-ov 6299  df-om 6698  df-wrecs 7027  df-recs 7089  df-rdg 7127  df-nn 10599
This theorem is referenced by:  uzwo3  11248  modmulnn  12100  bernneq3  12386  expmulnbnd  12390  facwordi  12460  faclbnd  12461  faclbnd2  12462  faclbnd3  12463  faclbnd5  12469  faclbnd6  12470  facubnd  12471  facavg  12472  bcp1nk  12488  hashf1  12604  swrds2  12988  isercolllem1  13695  isercoll  13698  o1fsum  13840  climcndslem1  13874  climcndslem2  13875  climcnds  13876  eftabs  14097  efcllem  14099  ege2le3  14111  efcj  14113  eftlub  14130  eflegeo  14142  eirrlem  14223  fzm1ndvds  14324  bitsfzolem  14371  bitsfzo  14372  bitsinv1lem  14378  sadcaddlem  14394  smueqlem  14427  bezoutlem3  14468  bezoutlem4  14469  sqgcd  14486  lcmgcdlem  14531  lcmf  14566  prmind2  14595  coprm  14617  prmfac1  14631  divdenle  14658  qnumgt0  14659  zsqrtelqelz  14667  hashdvds  14681  eulerthlem2  14688  odzdvds  14698  modprm1div  14700  vfermltl  14704  modprm0  14708  pythagtriplem11  14727  pythagtriplem13  14729  pythagtriplem19  14735  pclem  14740  pcpre1  14744  pcidlem  14773  pcadd  14786  pcmpt  14789  pcmpt2  14790  pcfaclem  14795  pcfac  14796  qexpz  14798  pockthlem  14801  pockthg  14802  prmreclem1  14812  prmreclem3  14814  prmreclem4  14815  prmreclem5  14816  1arithlem4  14822  1arith  14823  4sqlem5  14838  4sqlem6  14839  4sqlem10  14843  mul4sqlem  14849  4sqlem11  14851  4sqlem12  14852  4sqlem13OLD  14853  4sqlem14OLD  14854  4sqlem15OLD  14855  4sqlem16OLD  14856  4sqlem17OLD  14857  4sqlem13  14859  4sqlem14  14860  4sqlem15  14861  4sqlem16  14862  4sqlem17  14863  vdwlem1  14883  vdwlem3  14885  vdwlem6  14888  vdwlem9  14891  vdwlem10  14892  vdwlem12  14894  vdwnnlem3  14899  ramub1lem1  14936  prmolefac  14956  prmorlefacOLD  14970  prmgaplem4  14976  prmgaplem5  14977  prmgaplem6  14978  prmgaplem8  14980  2expltfac  15015  cshwshashnsame  15026  psgnunilem4  17082  mndodconglem  17125  oddvds  17131  sylow1lem1  17178  sylow1lem5  17182  fislw  17205  efgredlem  17325  gexexlem  17418  zringlpirlem3  18982  prmirredlem  18988  fvmptnn04if  19797  fvmptnn04ifb  19799  fvmptnn04ifc  19800  fvmptnn04ifd  19801  chfacfisf  19802  chfacfisfcpmat  19803  chfacfscmulgsum  19808  chfacfpmmulgsum  19812  lebnumii  21883  lmnn  22119  ovolunlem1a  22323  ovoliunlem1  22329  ovolicc2lem3  22346  ovolicc2lem4OLD  22347  ovolicc2lem4  22348  iundisj  22375  voliunlem1  22377  uniioombllem3  22417  dyadf  22423  dyadovol  22425  dyaddisjlem  22427  dyadmaxlem  22429  opnmbllem  22433  vitalilem4  22443  mbfi1fseqlem1  22547  mbfi1fseqlem3  22549  mbfi1fseqlem4  22550  mbfi1fseqlem5  22551  mbfi1fseqlem6  22552  itg2gt0  22592  itg2cnlem2  22594  dgreq0  23084  dgrco  23094  elqaalem2  23138  aaliou3lem2  23161  aaliou3lem8  23163  aaliou3lem9  23168  leibpi  23730  log2tlbnd  23733  birthdaylem3  23741  amgm  23778  emcllem2  23784  harmonicbnd4  23798  lgamgulmlem1  23816  lgamgulmlem2  23817  lgamgulmlem3  23818  lgamgulmlem4  23819  lgamgulmlem5  23820  lgamgulmlem6  23821  lgamucov  23825  lgamcvg2  23842  wilthlem1  23855  ftalem5  23863  basellem1  23867  basellem2  23868  basellem3  23869  basellem4  23870  basellem5  23871  basellem6  23872  basellem8  23874  chtge0  23899  chtwordi  23943  vma1  23953  dvdsdivcl  23970  dvdsflf1o  23976  dvdsflsumcom  23977  fsumfldivdiaglem  23978  sgmmul  23989  chtublem  23999  fsumvma2  24002  logfac2  24005  chpchtsum  24007  chpub  24008  logfaclbnd  24010  logexprlim  24013  mersenne  24015  perfectlem2  24018  dchrelbas4  24031  bposlem1  24072  bposlem2  24073  bposlem3  24074  bposlem4  24075  bposlem5  24076  bposlem6  24077  bposlem7  24078  bposlem9  24080  lgslem1  24084  lgslem4  24087  lgsval2lem  24094  lgsdirprm  24117  lgsdir  24118  lgsne0  24121  lgsqrlem2  24130  lgseisenlem1  24137  lgseisenlem2  24138  lgseisenlem3  24139  lgseisenlem4  24140  lgseisen  24141  lgsquadlem1  24142  lgsquadlem2  24143  lgsquadlem3  24144  m1lgs  24150  2sqlem3  24154  2sqlem8  24160  2sqblem  24165  chebbnd1lem1  24167  chebbnd1lem3  24169  chtppilimlem1  24171  rplogsumlem1  24182  rplogsumlem2  24183  dchrisum0lem1a  24184  rpvmasumlem  24185  dchrisumlema  24186  dchrisumlem1  24187  dchrisumlem2  24188  dchrisumlem3  24189  dchrvmasumiflem1  24199  dchrisum0flblem2  24207  dchrisum0re  24211  dchrisum0lem1b  24213  dchrisum0lem1  24214  dirith2  24226  selbergb  24247  selberg2lem  24248  logdivbnd  24254  selberg3lem2  24256  selberg4lem1  24258  pntrsumo1  24263  pntrsumbnd2  24265  pntrlog2bndlem1  24275  pntrlog2bndlem2  24276  pntrlog2bndlem3  24277  pntrlog2bndlem4  24278  pntrlog2bndlem5  24279  pntpbnd1a  24283  pntpbnd1  24284  pntibndlem2a  24288  pntibndlem2  24289  pntlemg  24296  pntlemh  24297  pntlemj  24301  pntlemf  24303  ostth2lem1  24316  padicabvf  24329  padicabvcxp  24330  ostth2lem2  24332  ostth2lem3  24333  ostth2lem4  24334  ostth2  24335  ostth3  24336  eupap1  25546  numclwwlk5  25682  numclwwlk7  25684  ubthlem2  26355  minvecolem4  26364  iundisjf  28035  ssnnssfz  28200  iundisjfi  28205  2sqmod  28244  pmtrto1cl  28448  psgnfzto1stlem  28449  fzto1st1  28451  fzto1st  28452  psgnfzto1st  28454  smatrcl  28458  smattr  28461  smatbl  28462  smatbr  28463  1smat1  28466  submateqlem1  28469  submateqlem2  28470  submateq  28471  esumcst  28720  fiunelros  28832  oddpwdc  29010  eulerpartlems  29016  eulerpartlemgc  29018  fiblem  29054  dstfrvunirn  29130  dstfrvclim1  29133  ballotlemimin  29161  subfaclim  29696  subfacval3  29697  erdszelem7  29705  erdszelem8  29706  erdsze2lem2  29712  cvmliftlem2  29794  cvmliftlem6  29798  cvmliftlem7  29799  cvmliftlem8  29800  cvmliftlem9  29801  cvmliftlem10  29802  cvmliftlem13  29804  bcprod  30158  bccolsum  30159  faclimlem2  30164  faclim2  30168  nn0prpwlem  30760  poimirlem3  31647  poimirlem6  31650  poimirlem7  31651  poimirlem8  31652  poimirlem9  31653  poimirlem10  31654  poimirlem11  31655  poimirlem12  31656  poimirlem13  31657  poimirlem15  31659  poimirlem16  31660  poimirlem17  31661  poimirlem19  31663  poimirlem20  31664  poimirlem21  31665  poimirlem22  31666  poimirlem23  31667  poimirlem26  31670  poimirlem28  31672  opnmbllem0  31680  mblfinlem2  31682  incsequz  31781  nninfnub  31784  irrapxlem3  35378  irrapxlem4  35379  irrapxlem5  35380  pellexlem2  35384  pellexlem6  35388  pell14qrgt0  35415  pell14qrgapw  35432  pellfundgt1  35441  rmspecsqrtnq  35464  ltrmxnn0  35509  jm3.1lem1  35582  jm3.1lem3  35584  dgraa0p  35718  hashnzfz2  36311  rfcnnnub  37001  nnxrd  37007  fzisoeu  37131  fsumnncl  37229  sumnnodd  37286  stoweidlem1  37434  stoweidlem3  37436  stoweidlem11  37444  stoweidlem17  37450  stoweidlem20  37453  stoweidlem25  37458  stoweidlem26  37459  stoweidlem34  37468  stoweidlem38  37472  stoweidlem42  37476  stoweidlem44  37478  stoweidlem51  37485  stoweidlem59  37493  stoweidlem60  37494  wallispi  37505  wallispi2  37508  stirlinglem3  37511  stirlinglem4  37512  stirlinglem8  37516  stirlinglem10  37518  stirlinglem12  37520  stirlinglem15  37523  dirkertrigeqlem2  37534  dirkertrigeqlem3  37535  dirkercncflem2  37539  fourierdlem11  37553  fourierdlem14  37556  fourierdlem15  37557  fourierdlem20  37562  fourierdlem31  37573  fourierdlem64  37606  fourierdlem93  37635  fourierdlem95  37637  fourierdlem103  37645  fourierdlem104  37646  fourierdlem112  37654  sqwvfourb  37665  etransclem3  37673  etransclem19  37689  etransclem23  37693  etransclem24  37694  etransclem25  37695  etransclem32  37702  etransclem35  37705  etransclem41  37711  etransclem48  37718  iccpartlt  38141  iccpartgt  38144  perfectALTVlem2  38247  gboge7  38267  proththdlem  38316  ztprmneprm  38901  pgrple2abl  38923  nno  39102  logbpw2m1  39152  nnpw2pmod  39168  nnolog2flm1  39175  blennngt2o2  39177
  Copyright terms: Public domain W3C validator