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

Theorem nnred 10438
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 10427 . 2  |-  NN  C_  RR
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3452 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   RRcr 9382   NNcn 10423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-i2m1 9451  ax-1ne0 9452  ax-rrecex 9455  ax-cnre 9456
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-reu 2802  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-tp 3980  df-op 3982  df-uni 4190  df-iun 4271  df-br 4391  df-opab 4449  df-mpt 4450  df-tr 4484  df-eprel 4730  df-id 4734  df-po 4739  df-so 4740  df-fr 4777  df-we 4779  df-ord 4820  df-on 4821  df-lim 4822  df-suc 4823  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-ov 6193  df-om 6577  df-recs 6932  df-rdg 6966  df-nn 10424
This theorem is referenced by:  uzwo3  11049  modmulnn  11826  bernneq3  12093  expmulnbnd  12097  facwordi  12166  faclbnd  12167  faclbnd2  12168  faclbnd3  12169  faclbnd5  12175  faclbnd6  12176  facubnd  12177  facavg  12178  bcp1nk  12194  hashf1  12312  swrds2  12647  isercolllem1  13244  isercoll  13247  o1fsum  13378  climcndslem1  13414  climcndslem2  13415  climcnds  13416  eftabs  13463  efcllem  13465  ege2le3  13477  efcj  13479  eftlub  13495  eflegeo  13507  eirrlem  13588  fzm1ndvds  13687  bitsfzolem  13732  bitsfzo  13733  bitsinv1lem  13739  sadcaddlem  13755  smueqlem  13788  bezoutlem3  13826  bezoutlem4  13827  sqgcd  13844  prmind2  13876  coprm  13888  prmfac1  13906  divdenle  13929  qnumgt0  13930  zsqrelqelz  13938  hashdvds  13952  eulerthlem2  13959  odzdvds  13969  modprm1div  13971  modprm0  13975  pythagtriplem11  13994  pythagtriplem13  13996  pythagtriplem19  14002  pclem  14007  pcpre1  14011  pcidlem  14040  pcadd  14053  pcmpt  14056  pcmpt2  14057  pcfaclem  14062  pcfac  14063  qexpz  14065  pockthlem  14068  pockthg  14069  prmreclem1  14079  prmreclem3  14081  prmreclem4  14082  prmreclem5  14083  1arithlem4  14089  1arith  14090  4sqlem5  14105  4sqlem6  14106  4sqlem10  14110  mul4sqlem  14116  4sqlem11  14118  4sqlem12  14119  4sqlem13  14120  4sqlem14  14121  4sqlem15  14122  4sqlem16  14123  4sqlem17  14124  vdwlem1  14144  vdwlem3  14146  vdwlem6  14149  vdwlem9  14152  vdwlem10  14153  vdwlem12  14155  vdwnnlem3  14160  ramub1lem1  14189  2expltfac  14221  cshwshashnsame  14232  psgnunilem4  16105  mndodconglem  16148  oddvds  16154  sylow1lem1  16201  sylow1lem5  16205  fislw  16228  efgredlem  16348  gexexlem  16438  zringlpirlem3  18014  zlpirlem3  18019  prmirredlem  18026  prmirredlemOLD  18029  lebnumii  20654  lmnn  20890  ovolunlem1a  21095  ovoliunlem1  21101  ovolicc2lem3  21118  ovolicc2lem4  21119  iundisj  21145  voliunlem1  21147  uniioombllem3  21181  dyadf  21187  dyadovol  21189  dyaddisjlem  21191  dyadmaxlem  21193  opnmbllem  21197  vitalilem4  21207  mbfi1fseqlem1  21309  mbfi1fseqlem3  21311  mbfi1fseqlem4  21312  mbfi1fseqlem5  21313  mbfi1fseqlem6  21314  itg2gt0  21354  itg2cnlem2  21356  dgreq0  21848  dgrco  21858  elqaalem2  21902  aaliou3lem2  21925  aaliou3lem8  21927  aaliou3lem9  21932  leibpi  22453  log2tlbnd  22456  birthdaylem3  22463  amgm  22500  emcllem2  22506  harmonicbnd4  22520  wilthlem1  22522  ftalem5  22530  basellem1  22534  basellem2  22535  basellem3  22536  basellem4  22537  basellem5  22538  basellem6  22539  basellem8  22541  chtge0  22566  chtwordi  22610  vma1  22620  dvdsdivcl  22637  dvdsflf1o  22643  dvdsflsumcom  22644  fsumfldivdiaglem  22645  sgmmul  22656  chtublem  22666  fsumvma2  22669  logfac2  22672  chpchtsum  22674  chpub  22675  logfaclbnd  22677  logexprlim  22680  mersenne  22682  perfectlem2  22685  dchrelbas4  22698  bposlem1  22739  bposlem2  22740  bposlem3  22741  bposlem4  22742  bposlem5  22743  bposlem6  22744  bposlem7  22745  bposlem9  22747  lgslem1  22751  lgslem4  22754  lgsval2lem  22761  lgsdirprm  22784  lgsdir  22785  lgsne0  22788  lgsqrlem2  22797  lgseisenlem1  22804  lgseisenlem2  22805  lgseisenlem3  22806  lgseisenlem4  22807  lgseisen  22808  lgsquadlem1  22809  lgsquadlem2  22810  lgsquadlem3  22811  m1lgs  22817  2sqlem3  22821  2sqlem8  22827  2sqblem  22832  chebbnd1lem1  22834  chebbnd1lem3  22836  chtppilimlem1  22838  rplogsumlem1  22849  rplogsumlem2  22850  dchrisum0lem1a  22851  rpvmasumlem  22852  dchrisumlema  22853  dchrisumlem1  22854  dchrisumlem2  22855  dchrisumlem3  22856  dchrvmasumiflem1  22866  dchrisum0flblem2  22874  dchrisum0re  22878  dchrisum0lem1b  22880  dchrisum0lem1  22881  dirith2  22893  selbergb  22914  selberg2lem  22915  logdivbnd  22921  selberg3lem2  22923  selberg4lem1  22925  pntrsumo1  22930  pntrsumbnd2  22932  pntrlog2bndlem1  22942  pntrlog2bndlem2  22943  pntrlog2bndlem3  22944  pntrlog2bndlem4  22945  pntrlog2bndlem5  22946  pntpbnd1a  22950  pntpbnd1  22951  pntibndlem2a  22955  pntibndlem2  22956  pntlemg  22963  pntlemh  22964  pntlemj  22968  pntlemf  22970  ostth2lem1  22983  padicabvf  22996  padicabvcxp  22997  ostth2lem2  22999  ostth2lem3  23000  ostth2lem4  23001  ostth2  23002  ostth3  23003  eupap1  23732  ubthlem2  24407  minvecolem4  24416  iundisjf  26065  ssnnssfz  26210  iundisjfi  26214  esumcst  26648  oddpwdc  26871  eulerpartlems  26877  eulerpartlemgc  26879  fiblem  26915  dstfrvunirn  26991  dstfrvclim1  26994  ballotlemimin  27022  lgamgulmlem1  27149  lgamgulmlem2  27150  lgamgulmlem3  27151  lgamgulmlem4  27152  lgamgulmlem5  27153  lgamgulmlem6  27154  lgamucov  27158  lgamcvg2  27175  subfaclim  27210  subfacval3  27211  erdszelem7  27219  erdszelem8  27220  erdsze2lem2  27226  cvmliftlem2  27309  cvmliftlem6  27313  cvmliftlem7  27314  cvmliftlem8  27315  cvmliftlem9  27316  cvmliftlem10  27317  cvmliftlem13  27319  faclimlem2  27684  faclim2  27688  opnmbllem0  28565  mblfinlem2  28567  nn0prpwlem  28655  incsequz  28782  nninfnub  28785  irrapxlem3  29303  irrapxlem4  29304  irrapxlem5  29305  pellexlem2  29309  pellexlem6  29313  pell14qrgt0  29338  pell14qrgapw  29355  pellfundgt1  29362  rmspecsqrnq  29385  ltrmxnn0  29430  jm3.1lem1  29504  jm3.1lem3  29506  dgraa0p  29644  rfcnnnub  29896  stoweidlem1  29934  stoweidlem3  29936  stoweidlem11  29944  stoweidlem17  29950  stoweidlem20  29953  stoweidlem25  29958  stoweidlem26  29959  stoweidlem34  29967  stoweidlem38  29971  stoweidlem42  29975  stoweidlem44  29977  stoweidlem51  29984  stoweidlem59  29992  stoweidlem60  29993  wallispi  30003  wallispi2  30006  stirlinglem3  30009  stirlinglem4  30010  stirlinglem8  30014  stirlinglem10  30016  stirlinglem12  30018  stirlinglem15  30021  numclwwlk5  30843  numclwwlk7  30845  ztprmneprm  30877  pgrple2abel  30908  fvmptnn04if  31303  fvmptnn04ifb  31305  fvmptnn04ifc  31306  fvmptnn04ifd  31307  chfacfisf  31308  chfacfisfcpmat  31309  chfacfscmulgsum  31314  chfacfpmmulgsum  31318
  Copyright terms: Public domain W3C validator