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

Theorem nnred 10016
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 10005 . 2  |-  NN  C_  RR
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3347 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   RRcr 8990   NNcn 10001
This theorem is referenced by:  uzwo3  10570  modmulnn  11266  bernneq3  11508  expmulnbnd  11512  facwordi  11581  faclbnd  11582  faclbnd2  11583  faclbnd3  11584  faclbnd5  11590  faclbnd6  11591  facubnd  11592  facavg  11593  bcp1nk  11609  hashf1  11707  swrds2  11881  isercolllem1  12459  isercoll  12462  o1fsum  12593  climcndslem1  12630  climcndslem2  12631  climcnds  12632  eftabs  12679  efcllem  12681  ege2le3  12693  efcj  12695  eftlub  12711  eflegeo  12723  eirrlem  12804  fzm1ndvds  12902  bitsfzolem  12947  bitsfzo  12948  bitsinv1lem  12954  sadcaddlem  12970  smueqlem  13003  bezoutlem3  13041  bezoutlem4  13042  sqgcd  13059  prmind2  13091  coprm  13101  prmfac1  13119  divdenle  13142  qnumgt0  13143  zsqrelqelz  13151  hashdvds  13165  eulerthlem2  13172  odzdvds  13182  pythagtriplem11  13200  pythagtriplem13  13202  pythagtriplem19  13208  pclem  13213  pcpre1  13217  pcidlem  13246  pcadd  13259  pcmpt  13262  pcmpt2  13263  pcfaclem  13268  pcfac  13269  qexpz  13271  pockthlem  13274  pockthg  13275  prmreclem1  13285  prmreclem3  13287  prmreclem4  13288  prmreclem5  13289  1arithlem4  13295  1arith  13296  4sqlem5  13311  4sqlem6  13312  4sqlem10  13316  mul4sqlem  13322  4sqlem11  13324  4sqlem12  13325  4sqlem13  13326  4sqlem14  13327  4sqlem15  13328  4sqlem16  13329  4sqlem17  13330  vdwlem1  13350  vdwlem3  13352  vdwlem6  13355  vdwlem9  13358  vdwlem10  13359  vdwlem12  13361  vdwnnlem3  13366  ramub1lem1  13395  2expltfac  13427  mndodconglem  15180  oddvds  15186  sylow1lem1  15233  sylow1lem5  15237  fislw  15260  efgredlem  15380  gexexlem  15468  zlpirlem3  16771  prmirredlem  16774  lebnumii  18992  lmnn  19217  ovolunlem1a  19393  ovoliunlem1  19399  ovolicc2lem3  19416  ovolicc2lem4  19417  iundisj  19443  voliunlem1  19445  uniioombllem3  19478  dyadf  19484  dyadovol  19486  dyaddisjlem  19488  dyadmaxlem  19490  opnmbllem  19494  vitalilem4  19504  mbfi1fseqlem1  19608  mbfi1fseqlem3  19610  mbfi1fseqlem4  19611  mbfi1fseqlem5  19612  mbfi1fseqlem6  19613  itg2gt0  19653  itg2cnlem2  19655  dgreq0  20184  dgrco  20194  elqaalem2  20238  aaliou3lem2  20261  aaliou3lem8  20263  aaliou3lem9  20268  leibpi  20783  log2tlbnd  20786  birthdaylem3  20793  amgm  20830  emcllem2  20836  harmonicbnd4  20850  wilthlem1  20852  ftalem5  20860  basellem1  20864  basellem2  20865  basellem3  20866  basellem4  20867  basellem5  20868  basellem6  20869  basellem8  20871  chtge0  20896  chtwordi  20940  vma1  20950  dvdsdivcl  20967  dvdsflf1o  20973  dvdsflsumcom  20974  fsumfldivdiaglem  20975  sgmmul  20986  chtublem  20996  fsumvma2  20999  logfac2  21002  chpchtsum  21004  chpub  21005  logfaclbnd  21007  logexprlim  21010  mersenne  21012  perfectlem2  21015  dchrelbas4  21028  bposlem1  21069  bposlem2  21070  bposlem3  21071  bposlem4  21072  bposlem5  21073  bposlem6  21074  bposlem7  21075  bposlem9  21077  lgslem1  21081  lgslem4  21084  lgsval2lem  21091  lgsdirprm  21114  lgsdir  21115  lgsne0  21118  lgsqrlem2  21127  lgseisenlem1  21134  lgseisenlem2  21135  lgseisenlem3  21136  lgseisenlem4  21137  lgseisen  21138  lgsquadlem1  21139  lgsquadlem2  21140  lgsquadlem3  21141  m1lgs  21147  2sqlem3  21151  2sqlem8  21157  2sqblem  21162  chebbnd1lem1  21164  chebbnd1lem3  21166  chtppilimlem1  21168  rplogsumlem1  21179  rplogsumlem2  21180  dchrisum0lem1a  21181  rpvmasumlem  21182  dchrisumlema  21183  dchrisumlem1  21184  dchrisumlem2  21185  dchrisumlem3  21186  dchrvmasumiflem1  21196  dchrisum0flblem2  21204  dchrisum0re  21208  dchrisum0lem1b  21210  dchrisum0lem1  21211  dirith2  21223  selbergb  21244  selberg2lem  21245  logdivbnd  21251  selberg3lem2  21253  selberg4lem1  21255  pntrsumo1  21260  pntrsumbnd2  21262  pntrlog2bndlem1  21272  pntrlog2bndlem2  21273  pntrlog2bndlem3  21274  pntrlog2bndlem4  21275  pntrlog2bndlem5  21276  pntpbnd1a  21280  pntpbnd1  21281  pntibndlem2a  21285  pntibndlem2  21286  pntlemg  21293  pntlemh  21294  pntlemj  21298  pntlemf  21300  ostth2lem1  21313  padicabvf  21326  padicabvcxp  21327  ostth2lem2  21329  ostth2lem3  21330  ostth2lem4  21331  ostth2  21332  ostth3  21333  eupap1  21699  ubthlem2  22374  minvecolem4  22383  iundisjf  24030  ssnnssfz  24149  iundisjfi  24153  esumcst  24456  dstfrvunirn  24733  dstfrvclim1  24736  ballotlemimin  24764  lgamgulmlem1  24814  lgamgulmlem2  24815  lgamgulmlem3  24816  lgamgulmlem4  24817  lgamgulmlem5  24818  lgamgulmlem6  24819  lgamucov  24823  lgamcvg2  24840  subfaclim  24875  subfacval3  24876  erdszelem7  24884  erdszelem8  24885  erdsze2lem2  24891  cvmliftlem2  24974  cvmliftlem6  24978  cvmliftlem7  24979  cvmliftlem8  24980  cvmliftlem9  24981  cvmliftlem10  24982  cvmliftlem13  24984  faclimlem2  25364  faclim2  25368  opnmbllem0  26243  mblfinlem2  26245  nn0prpwlem  26326  incsequz  26453  nninfnub  26456  irrapxlem3  26888  irrapxlem4  26889  irrapxlem5  26890  pellexlem2  26894  pellexlem6  26898  pell14qrgt0  26923  pell14qrgapw  26940  pellfundgt1  26947  rmspecsqrnq  26970  ltrmxnn0  27015  jm3.1lem1  27089  jm3.1lem3  27091  dgraa0p  27332  psgnunilem4  27398  rfcnnnub  27684  stoweidlem1  27727  stoweidlem3  27729  stoweidlem11  27737  stoweidlem17  27743  stoweidlem20  27746  stoweidlem25  27751  stoweidlem26  27752  stoweidlem34  27760  stoweidlem38  27764  stoweidlem42  27768  stoweidlem44  27770  stoweidlem51  27777  stoweidlem59  27785  stoweidlem60  27786  wallispi  27796  wallispi2  27799  stirlinglem3  27802  stirlinglem4  27803  stirlinglem8  27807  stirlinglem10  27809  stirlinglem12  27811  stirlinglem15  27814  modprm1div  28225  modprm0  28229  cshwssizensame  28290
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702  ax-1cn 9049  ax-icn 9050  ax-addcl 9051  ax-addrcl 9052  ax-mulcl 9053  ax-mulrcl 9054  ax-i2m1 9059  ax-1ne0 9060  ax-rrecex 9063  ax-cnre 9064
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2711  df-rex 2712  df-reu 2713  df-rab 2715  df-v 2959  df-sbc 3163  df-csb 3253  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-tp 3823  df-op 3824  df-uni 4017  df-iun 4096  df-br 4214  df-opab 4268  df-mpt 4269  df-tr 4304  df-eprel 4495  df-id 4499  df-po 4504  df-so 4505  df-fr 4542  df-we 4544  df-ord 4585  df-on 4586  df-lim 4587  df-suc 4588  df-om 4847  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-ov 6085  df-recs 6634  df-rdg 6669  df-nn 10002
  Copyright terms: Public domain W3C validator