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

Theorem nnred 10329
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 10318 . 2  |-  NN  C_  RR
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3349 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   RRcr 9273   NNcn 10314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-i2m1 9342  ax-1ne0 9343  ax-rrecex 9346  ax-cnre 9347
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6089  df-om 6472  df-recs 6824  df-rdg 6858  df-nn 10315
This theorem is referenced by:  uzwo3  10940  modmulnn  11717  bernneq3  11984  expmulnbnd  11988  facwordi  12057  faclbnd  12058  faclbnd2  12059  faclbnd3  12060  faclbnd5  12066  faclbnd6  12067  facubnd  12068  facavg  12069  bcp1nk  12085  hashf1  12202  swrds2  12537  isercolllem1  13134  isercoll  13137  o1fsum  13268  climcndslem1  13304  climcndslem2  13305  climcnds  13306  eftabs  13353  efcllem  13355  ege2le3  13367  efcj  13369  eftlub  13385  eflegeo  13397  eirrlem  13478  fzm1ndvds  13577  bitsfzolem  13622  bitsfzo  13623  bitsinv1lem  13629  sadcaddlem  13645  smueqlem  13678  bezoutlem3  13716  bezoutlem4  13717  sqgcd  13734  prmind2  13766  coprm  13778  prmfac1  13796  divdenle  13819  qnumgt0  13820  zsqrelqelz  13828  hashdvds  13842  eulerthlem2  13849  odzdvds  13859  modprm1div  13861  modprm0  13865  pythagtriplem11  13884  pythagtriplem13  13886  pythagtriplem19  13892  pclem  13897  pcpre1  13901  pcidlem  13930  pcadd  13943  pcmpt  13946  pcmpt2  13947  pcfaclem  13952  pcfac  13953  qexpz  13955  pockthlem  13958  pockthg  13959  prmreclem1  13969  prmreclem3  13971  prmreclem4  13972  prmreclem5  13973  1arithlem4  13979  1arith  13980  4sqlem5  13995  4sqlem6  13996  4sqlem10  14000  mul4sqlem  14006  4sqlem11  14008  4sqlem12  14009  4sqlem13  14010  4sqlem14  14011  4sqlem15  14012  4sqlem16  14013  4sqlem17  14014  vdwlem1  14034  vdwlem3  14036  vdwlem6  14039  vdwlem9  14042  vdwlem10  14043  vdwlem12  14045  vdwnnlem3  14050  ramub1lem1  14079  2expltfac  14111  cshwshashnsame  14122  psgnunilem4  15994  mndodconglem  16035  oddvds  16041  sylow1lem1  16088  sylow1lem5  16092  fislw  16115  efgredlem  16235  gexexlem  16325  zringlpirlem3  17885  zlpirlem3  17890  prmirredlem  17897  prmirredlemOLD  17900  lebnumii  20518  lmnn  20754  ovolunlem1a  20959  ovoliunlem1  20965  ovolicc2lem3  20982  ovolicc2lem4  20983  iundisj  21009  voliunlem1  21011  uniioombllem3  21045  dyadf  21051  dyadovol  21053  dyaddisjlem  21055  dyadmaxlem  21057  opnmbllem  21061  vitalilem4  21071  mbfi1fseqlem1  21173  mbfi1fseqlem3  21175  mbfi1fseqlem4  21176  mbfi1fseqlem5  21177  mbfi1fseqlem6  21178  itg2gt0  21218  itg2cnlem2  21220  dgreq0  21712  dgrco  21722  elqaalem2  21766  aaliou3lem2  21789  aaliou3lem8  21791  aaliou3lem9  21796  leibpi  22317  log2tlbnd  22320  birthdaylem3  22327  amgm  22364  emcllem2  22370  harmonicbnd4  22384  wilthlem1  22386  ftalem5  22394  basellem1  22398  basellem2  22399  basellem3  22400  basellem4  22401  basellem5  22402  basellem6  22403  basellem8  22405  chtge0  22430  chtwordi  22474  vma1  22484  dvdsdivcl  22501  dvdsflf1o  22507  dvdsflsumcom  22508  fsumfldivdiaglem  22509  sgmmul  22520  chtublem  22530  fsumvma2  22533  logfac2  22536  chpchtsum  22538  chpub  22539  logfaclbnd  22541  logexprlim  22544  mersenne  22546  perfectlem2  22549  dchrelbas4  22562  bposlem1  22603  bposlem2  22604  bposlem3  22605  bposlem4  22606  bposlem5  22607  bposlem6  22608  bposlem7  22609  bposlem9  22611  lgslem1  22615  lgslem4  22618  lgsval2lem  22625  lgsdirprm  22648  lgsdir  22649  lgsne0  22652  lgsqrlem2  22661  lgseisenlem1  22668  lgseisenlem2  22669  lgseisenlem3  22670  lgseisenlem4  22671  lgseisen  22672  lgsquadlem1  22673  lgsquadlem2  22674  lgsquadlem3  22675  m1lgs  22681  2sqlem3  22685  2sqlem8  22691  2sqblem  22696  chebbnd1lem1  22698  chebbnd1lem3  22700  chtppilimlem1  22702  rplogsumlem1  22713  rplogsumlem2  22714  dchrisum0lem1a  22715  rpvmasumlem  22716  dchrisumlema  22717  dchrisumlem1  22718  dchrisumlem2  22719  dchrisumlem3  22720  dchrvmasumiflem1  22730  dchrisum0flblem2  22738  dchrisum0re  22742  dchrisum0lem1b  22744  dchrisum0lem1  22745  dirith2  22757  selbergb  22778  selberg2lem  22779  logdivbnd  22785  selberg3lem2  22787  selberg4lem1  22789  pntrsumo1  22794  pntrsumbnd2  22796  pntrlog2bndlem1  22806  pntrlog2bndlem2  22807  pntrlog2bndlem3  22808  pntrlog2bndlem4  22809  pntrlog2bndlem5  22810  pntpbnd1a  22814  pntpbnd1  22815  pntibndlem2a  22819  pntibndlem2  22820  pntlemg  22827  pntlemh  22828  pntlemj  22832  pntlemf  22834  ostth2lem1  22847  padicabvf  22860  padicabvcxp  22861  ostth2lem2  22863  ostth2lem3  22864  ostth2lem4  22865  ostth2  22866  ostth3  22867  eupap1  23565  ubthlem2  24240  minvecolem4  24249  iundisjf  25899  ssnnssfz  26044  iundisjfi  26048  esumcst  26483  oddpwdc  26706  eulerpartlems  26712  eulerpartlemgc  26714  fiblem  26750  dstfrvunirn  26826  dstfrvclim1  26829  ballotlemimin  26857  lgamgulmlem1  26984  lgamgulmlem2  26985  lgamgulmlem3  26986  lgamgulmlem4  26987  lgamgulmlem5  26988  lgamgulmlem6  26989  lgamucov  26993  lgamcvg2  27010  subfaclim  27045  subfacval3  27046  erdszelem7  27054  erdszelem8  27055  erdsze2lem2  27061  cvmliftlem2  27144  cvmliftlem6  27148  cvmliftlem7  27149  cvmliftlem8  27150  cvmliftlem9  27151  cvmliftlem10  27152  cvmliftlem13  27154  faclimlem2  27519  faclim2  27523  opnmbllem0  28398  mblfinlem2  28400  nn0prpwlem  28488  incsequz  28615  nninfnub  28618  irrapxlem3  29136  irrapxlem4  29137  irrapxlem5  29138  pellexlem2  29142  pellexlem6  29146  pell14qrgt0  29171  pell14qrgapw  29188  pellfundgt1  29195  rmspecsqrnq  29218  ltrmxnn0  29263  jm3.1lem1  29337  jm3.1lem3  29339  dgraa0p  29477  rfcnnnub  29729  stoweidlem1  29767  stoweidlem3  29769  stoweidlem11  29777  stoweidlem17  29783  stoweidlem20  29786  stoweidlem25  29791  stoweidlem26  29792  stoweidlem34  29800  stoweidlem38  29804  stoweidlem42  29808  stoweidlem44  29810  stoweidlem51  29817  stoweidlem59  29825  stoweidlem60  29826  wallispi  29836  wallispi2  29839  stirlinglem3  29842  stirlinglem4  29843  stirlinglem8  29847  stirlinglem10  29849  stirlinglem12  29851  stirlinglem15  29854  numclwwlk5  30676  numclwwlk7  30678  ztprmneprm  30709  pgrple2abel  30737
  Copyright terms: Public domain W3C validator