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

Theorem nnred 9971
Description: A natural number 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 9960 . 2  |-  NN  C_  RR
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3306 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   RRcr 8945   NNcn 9956
This theorem is referenced by:  uzwo3  10525  modmulnn  11220  bernneq3  11462  expmulnbnd  11466  facwordi  11535  faclbnd  11536  faclbnd2  11537  faclbnd3  11538  faclbnd5  11544  faclbnd6  11545  facubnd  11546  facavg  11547  bcp1nk  11563  hashf1  11661  swrds2  11835  isercolllem1  12413  isercoll  12416  o1fsum  12547  climcndslem1  12584  climcndslem2  12585  climcnds  12586  eftabs  12633  efcllem  12635  ege2le3  12647  efcj  12649  eftlub  12665  eflegeo  12677  eirrlem  12758  fzm1ndvds  12856  bitsfzolem  12901  bitsfzo  12902  bitsinv1lem  12908  sadcaddlem  12924  smueqlem  12957  bezoutlem3  12995  bezoutlem4  12996  sqgcd  13013  prmind2  13045  coprm  13055  prmfac1  13073  divdenle  13096  qnumgt0  13097  zsqrelqelz  13105  hashdvds  13119  eulerthlem2  13126  odzdvds  13136  pythagtriplem11  13154  pythagtriplem13  13156  pythagtriplem19  13162  pclem  13167  pcpre1  13171  pcidlem  13200  pcadd  13213  pcmpt  13216  pcmpt2  13217  pcfaclem  13222  pcfac  13223  qexpz  13225  pockthlem  13228  pockthg  13229  prmreclem1  13239  prmreclem3  13241  prmreclem4  13242  prmreclem5  13243  1arithlem4  13249  1arith  13250  4sqlem5  13265  4sqlem6  13266  4sqlem10  13270  mul4sqlem  13276  4sqlem11  13278  4sqlem12  13279  4sqlem13  13280  4sqlem14  13281  4sqlem15  13282  4sqlem16  13283  4sqlem17  13284  vdwlem1  13304  vdwlem3  13306  vdwlem6  13309  vdwlem9  13312  vdwlem10  13313  vdwlem12  13315  vdwnnlem3  13320  ramub1lem1  13349  2expltfac  13381  mndodconglem  15134  oddvds  15140  sylow1lem1  15187  sylow1lem5  15191  fislw  15214  efgredlem  15334  gexexlem  15422  zlpirlem3  16725  prmirredlem  16728  lebnumii  18944  lmnn  19169  ovolunlem1a  19345  ovoliunlem1  19351  ovolicc2lem3  19368  ovolicc2lem4  19369  iundisj  19395  voliunlem1  19397  uniioombllem3  19430  dyadf  19436  dyadovol  19438  dyaddisjlem  19440  dyadmaxlem  19442  opnmbllem  19446  vitalilem4  19456  mbfi1fseqlem1  19560  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfi1fseqlem6  19565  itg2gt0  19605  itg2cnlem2  19607  dgreq0  20136  dgrco  20146  elqaalem2  20190  aaliou3lem2  20213  aaliou3lem8  20215  aaliou3lem9  20220  leibpi  20735  log2tlbnd  20738  birthdaylem3  20745  amgm  20782  emcllem2  20788  harmonicbnd4  20802  wilthlem1  20804  ftalem5  20812  basellem1  20816  basellem2  20817  basellem3  20818  basellem4  20819  basellem5  20820  basellem6  20821  basellem8  20823  chtge0  20848  chtwordi  20892  vma1  20902  dvdsdivcl  20919  dvdsflf1o  20925  dvdsflsumcom  20926  fsumfldivdiaglem  20927  sgmmul  20938  chtublem  20948  fsumvma2  20951  logfac2  20954  chpchtsum  20956  chpub  20957  logfaclbnd  20959  logexprlim  20962  mersenne  20964  perfectlem2  20967  dchrelbas4  20980  bposlem1  21021  bposlem2  21022  bposlem3  21023  bposlem4  21024  bposlem5  21025  bposlem6  21026  bposlem7  21027  bposlem9  21029  lgslem1  21033  lgslem4  21036  lgsval2lem  21043  lgsdirprm  21066  lgsdir  21067  lgsne0  21070  lgsqrlem2  21079  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem3  21088  lgseisenlem4  21089  lgseisen  21090  lgsquadlem1  21091  lgsquadlem2  21092  lgsquadlem3  21093  m1lgs  21099  2sqlem3  21103  2sqlem8  21109  2sqblem  21114  chebbnd1lem1  21116  chebbnd1lem3  21118  chtppilimlem1  21120  rplogsumlem1  21131  rplogsumlem2  21132  dchrisum0lem1a  21133  rpvmasumlem  21134  dchrisumlema  21135  dchrisumlem1  21136  dchrisumlem2  21137  dchrisumlem3  21138  dchrvmasumiflem1  21148  dchrisum0flblem2  21156  dchrisum0re  21160  dchrisum0lem1b  21162  dchrisum0lem1  21163  dirith2  21175  selbergb  21196  selberg2lem  21197  logdivbnd  21203  selberg3lem2  21205  selberg4lem1  21207  pntrsumo1  21212  pntrsumbnd2  21214  pntrlog2bndlem1  21224  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntpbnd1a  21232  pntpbnd1  21233  pntibndlem2a  21237  pntibndlem2  21238  pntlemg  21245  pntlemh  21246  pntlemj  21250  pntlemf  21252  ostth2lem1  21265  padicabvf  21278  padicabvcxp  21279  ostth2lem2  21281  ostth2lem3  21282  ostth2lem4  21283  ostth2  21284  ostth3  21285  eupap1  21651  ubthlem2  22326  minvecolem4  22335  iundisjf  23982  ssnnssfz  24101  iundisjfi  24105  esumcst  24408  dstfrvunirn  24685  dstfrvclim1  24688  ballotlemimin  24716  lgamgulmlem1  24766  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamgulmlem4  24769  lgamgulmlem5  24770  lgamgulmlem6  24771  lgamucov  24775  lgamcvg2  24792  subfaclim  24827  subfacval3  24828  erdszelem7  24836  erdszelem8  24837  erdsze2lem2  24843  cvmliftlem2  24926  cvmliftlem6  24930  cvmliftlem7  24931  cvmliftlem8  24932  cvmliftlem9  24933  cvmliftlem10  24934  cvmliftlem13  24936  faclimlem2  25311  faclim2  25315  mblfinlem  26143  nn0prpwlem  26215  incsequz  26342  nninfnub  26345  irrapxlem3  26777  irrapxlem4  26778  irrapxlem5  26779  pellexlem2  26783  pellexlem6  26787  pell14qrgt0  26812  pell14qrgapw  26829  pellfundgt1  26836  rmspecsqrnq  26859  ltrmxnn0  26904  jm3.1lem1  26978  jm3.1lem3  26980  dgraa0p  27222  psgnunilem4  27288  rfcnnnub  27574  stoweidlem1  27617  stoweidlem3  27619  stoweidlem11  27627  stoweidlem17  27633  stoweidlem20  27636  stoweidlem25  27641  stoweidlem26  27642  stoweidlem34  27650  stoweidlem38  27654  stoweidlem42  27658  stoweidlem44  27660  stoweidlem51  27667  stoweidlem59  27675  stoweidlem60  27676  wallispi  27686  wallispi2  27689  stirlinglem3  27692  stirlinglem4  27693  stirlinglem8  27697  stirlinglem10  27699  stirlinglem12  27701  stirlinglem15  27704
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-i2m1 9014  ax-1ne0 9015  ax-rrecex 9018  ax-cnre 9019
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-recs 6592  df-rdg 6627  df-nn 9957
  Copyright terms: Public domain W3C validator