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

Theorem nnred 10912
Description: A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nnred.1 (𝜑𝐴 ∈ ℕ)
Assertion
Ref Expression
nnred (𝜑𝐴 ∈ ℝ)

Proof of Theorem nnred
StepHypRef Expression
1 nnssre 10901 . 2 ℕ ⊆ ℝ
2 nnred.1 . 2 (𝜑𝐴 ∈ ℕ)
31, 2sseldi 3566 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  cr 9814  cn 10897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rrecex 9887  ax-cnre 9888
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-nn 10898
This theorem is referenced by:  uzwo3  11659  modmulnn  12550  bernneq3  12854  expmulnbnd  12858  facwordi  12938  faclbnd  12939  faclbnd2  12940  faclbnd3  12941  faclbnd5  12947  faclbnd6  12948  facubnd  12949  facavg  12950  bcp1nk  12966  hashf1  13098  swrds2  13533  isercolllem1  14243  isercoll  14246  o1fsum  14386  climcndslem1  14420  climcndslem2  14421  climcnds  14422  eftabs  14645  efcllem  14647  ege2le3  14659  efcj  14661  eftlub  14678  eflegeo  14690  eirrlem  14771  fzm1ndvds  14882  nno  14936  nnoddm1d2  14940  bitsfzolem  14994  bitsfzo  14995  bitsinv1lem  15001  sadcaddlem  15017  smueqlem  15050  bezoutlem3  15096  bezoutlem4  15097  sqgcd  15116  lcmgcdlem  15157  lcmf  15184  prmind2  15236  coprm  15261  prmfac1  15269  prmndvdsfaclt  15273  divdenle  15295  qnumgt0  15296  zsqrtelqelz  15304  hashdvds  15318  eulerthlem2  15325  odzdvds  15338  modprm1div  15340  vfermltl  15344  modprm0  15348  pythagtriplem11  15368  pythagtriplem13  15370  pythagtriplem19  15376  pclem  15381  pcpre1  15385  pcidlem  15414  dvdsprmpweqle  15428  pcadd  15431  pcmpt  15434  pcmpt2  15435  pcfaclem  15440  pcfac  15441  qexpz  15443  pockthlem  15447  pockthg  15448  prmreclem1  15458  prmreclem3  15460  prmreclem4  15461  prmreclem5  15462  1arithlem4  15468  1arith  15469  4sqlem5  15484  4sqlem6  15485  4sqlem10  15489  mul4sqlem  15495  4sqlem11  15497  4sqlem12  15498  4sqlem13  15499  4sqlem14  15500  4sqlem15  15501  4sqlem16  15502  4sqlem17  15503  vdwlem1  15523  vdwlem3  15525  vdwlem6  15528  vdwlem9  15531  vdwlem10  15532  vdwlem12  15534  vdwnnlem3  15539  ramub1lem1  15568  prmolefac  15588  prmgaplem4  15596  prmgaplem5  15597  prmgaplem6  15598  prmgaplem8  15600  2expltfac  15637  cshwshashnsame  15648  psgnunilem4  17740  mndodconglem  17783  oddvds  17789  sylow1lem1  17836  sylow1lem5  17840  fislw  17863  efgredlem  17983  gexexlem  18078  zringlpirlem3  19653  prmirredlem  19660  fvmptnn04if  20473  fvmptnn04ifb  20475  fvmptnn04ifc  20476  fvmptnn04ifd  20477  chfacfisf  20478  chfacfisfcpmat  20479  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  lebnumii  22573  lmnn  22869  ovolunlem1a  23071  ovoliunlem1  23077  ovolicc2lem3  23094  ovolicc2lem4  23095  iundisj  23123  voliunlem1  23125  uniioombllem3  23159  dyadf  23165  dyadovol  23167  dyaddisjlem  23169  dyadmaxlem  23171  opnmbllem  23175  vitalilem4  23186  mbfi1fseqlem1  23288  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  mbfi1fseqlem6  23293  itg2gt0  23333  itg2cnlem2  23335  dgreq0  23825  dgrco  23835  elqaalem2  23879  aaliou3lem2  23902  aaliou3lem8  23904  aaliou3lem9  23909  leibpi  24469  log2tlbnd  24472  birthdaylem3  24480  amgm  24517  emcllem2  24523  harmonicbnd4  24537  lgamgulmlem1  24555  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem4  24558  lgamgulmlem5  24559  lgamgulmlem6  24560  lgamucov  24564  lgamcvg2  24581  wilthlem1  24594  ftalem5  24603  basellem1  24607  basellem2  24608  basellem3  24609  basellem4  24610  basellem5  24611  basellem6  24612  basellem8  24614  chtge0  24638  chtwordi  24682  vma1  24692  dvdsflf1o  24713  dvdsflsumcom  24714  fsumfldivdiaglem  24715  sgmmul  24726  chtublem  24736  fsumvma2  24739  logfac2  24742  chpchtsum  24744  chpub  24745  logfaclbnd  24747  logexprlim  24750  mersenne  24752  perfectlem2  24755  dchrelbas4  24768  bposlem1  24809  bposlem2  24810  bposlem3  24811  bposlem4  24812  bposlem5  24813  bposlem6  24814  bposlem7  24815  bposlem9  24817  lgslem1  24822  lgslem4  24825  lgsval2lem  24832  lgsdirprm  24856  lgsdir  24857  lgsne0  24860  lgsqrlem2  24872  gausslemma2dlem0h  24888  gausslemma2dlem0i  24889  gausslemma2dlem1a  24890  gausslemma2dlem2  24892  gausslemma2dlem7  24898  gausslemma2d  24899  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem3  24902  lgseisenlem4  24903  lgseisen  24904  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  m1lgs  24913  2sqlem3  24945  2sqlem8  24951  2sqblem  24956  chebbnd1lem1  24958  chebbnd1lem3  24960  chtppilimlem1  24962  rplogsumlem1  24973  rplogsumlem2  24974  dchrisum0lem1a  24975  rpvmasumlem  24976  dchrisumlema  24977  dchrisumlem1  24978  dchrisumlem2  24979  dchrisumlem3  24980  dchrvmasumiflem1  24990  dchrisum0flblem2  24998  dchrisum0re  25002  dchrisum0lem1b  25004  dchrisum0lem1  25005  dirith2  25017  selbergb  25038  selberg2lem  25039  logdivbnd  25045  selberg3lem2  25047  selberg4lem1  25049  pntrsumo1  25054  pntrsumbnd2  25056  pntrlog2bndlem1  25066  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntpbnd1a  25074  pntpbnd1  25075  pntibndlem2a  25079  pntibndlem2  25080  pntlemg  25087  pntlemh  25088  pntlemj  25092  pntlemf  25094  ostth2lem1  25107  padicabvf  25120  padicabvcxp  25121  ostth2lem2  25123  ostth2lem3  25124  ostth2lem4  25125  ostth2  25126  ostth3  25127  eupap1  26503  numclwwlk5  26639  numclwwlk7  26641  ubthlem2  27111  minvecolem4  27120  iundisjf  28784  ssnnssfz  28937  iundisjfi  28942  2sqmod  28979  pmtrto1cl  29180  psgnfzto1stlem  29181  fzto1st1  29183  fzto1st  29184  psgnfzto1st  29186  smatrcl  29190  smattr  29193  smatbl  29194  smatbr  29195  1smat1  29198  submateqlem1  29201  submateqlem2  29202  submateq  29203  esumcst  29452  fiunelros  29564  oddpwdc  29743  eulerpartlems  29749  eulerpartlemgc  29751  fiblem  29787  dstfrvunirn  29863  dstfrvclim1  29866  ballotlemimin  29894  subfaclim  30424  subfacval3  30425  erdszelem7  30433  erdszelem8  30434  erdsze2lem2  30440  cvmliftlem2  30522  cvmliftlem6  30526  cvmliftlem7  30527  cvmliftlem8  30528  cvmliftlem9  30529  cvmliftlem10  30530  cvmliftlem13  30532  bcprod  30877  bccolsum  30878  faclimlem2  30883  faclim2  30887  nn0prpwlem  31487  knoppndvlem15  31687  knoppndvlem17  31689  knoppndvlem18  31690  knoppndvlem19  31691  knoppndvlem20  31692  knoppndvlem21  31693  poimirlem3  32582  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem9  32588  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem13  32592  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem23  32602  poimirlem26  32605  poimirlem28  32607  opnmbllem0  32615  mblfinlem2  32617  incsequz  32714  nninfnub  32717  irrapxlem3  36406  irrapxlem4  36407  irrapxlem5  36408  pellexlem2  36412  pellexlem6  36416  pell14qrgt0  36441  pell14qrgapw  36458  pellfundgt1  36465  rmspecsqrtnq  36488  rmspecsqrtnqOLD  36489  ltrmxnn0  36534  jm3.1lem1  36602  jm3.1lem3  36604  dgraa0p  36738  hashnzfz2  37542  rfcnnnub  38218  nnxrd  38224  fzisoeu  38455  fsumnncl  38638  sumnnodd  38697  stoweidlem1  38894  stoweidlem3  38896  stoweidlem11  38904  stoweidlem17  38910  stoweidlem20  38913  stoweidlem25  38918  stoweidlem26  38919  stoweidlem34  38927  stoweidlem38  38931  stoweidlem42  38935  stoweidlem44  38937  stoweidlem51  38944  stoweidlem59  38952  stoweidlem60  38953  wallispi  38963  wallispi2  38966  stirlinglem3  38969  stirlinglem4  38970  stirlinglem8  38974  stirlinglem10  38976  stirlinglem12  38978  stirlinglem15  38981  dirkertrigeqlem2  38992  dirkertrigeqlem3  38993  dirkercncflem2  38997  fourierdlem11  39011  fourierdlem14  39014  fourierdlem15  39015  fourierdlem20  39020  fourierdlem31  39031  fourierdlem64  39063  fourierdlem93  39092  fourierdlem95  39094  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  sqwvfourb  39122  etransclem3  39130  etransclem19  39146  etransclem23  39150  etransclem24  39151  etransclem25  39152  etransclem32  39159  etransclem35  39162  etransclem41  39168  etransclem48  39175  qndenserrnbllem  39190  hoiqssbllem1  39512  hoiqssbllem2  39513  ovolval5lem1  39542  ovolval5lem2  39543  iccpartlt  39962  iccpartgt  39965  odz2prm2pw  40013  fmtnoprmfac1lem  40014  2pwp1prm  40041  sfprmdvdsmersenne  40058  lighneallem2  40061  proththdlem  40068  perfectALTVlem2  40165  gboge7  40185  clwlksfclwwlk  41269  av-numclwwlk5  41542  av-numclwwlk7  41545  ztprmneprm  41918  pgrple2abl  41940  logbpw2m1  42159  nnpw2pmod  42175  nnolog2flm1  42182  blennngt2o2  42184
  Copyright terms: Public domain W3C validator