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

Theorem nnred 11316
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 11305 . 2 ℕ ⊆ ℝ
2 nnred.1 . 2 (𝜑𝐴 ∈ ℕ)
31, 2sseldi 3796 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  cr 10216  cn 11301
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-i2m1 10285  ax-1ne0 10286  ax-rrecex 10289  ax-cnre 10290
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-ov 6873  df-om 7292  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-nn 11302
This theorem is referenced by:  uzwo3  11998  modmulnn  12908  bernneq3  13211  expmulnbnd  13215  facwordi  13292  faclbnd  13293  faclbnd2  13294  faclbnd3  13295  faclbnd5  13301  faclbnd6  13302  facubnd  13303  facavg  13304  bcp1nk  13320  hashf1  13454  swrds2  13905  isercolllem1  14614  isercoll  14617  o1fsum  14763  climcndslem1  14799  climcndslem2  14800  climcnds  14801  eftabs  15022  efcllem  15024  ege2le3  15036  efcj  15038  eftlub  15055  eflegeo  15067  eirrlem  15148  fzm1ndvds  15263  nno  15314  nnoddm1d2  15318  bitsfzolem  15371  bitsfzo  15372  bitsinv1lem  15378  sadcaddlem  15394  smueqlem  15427  bezoutlem3  15473  bezoutlem4  15474  sqgcd  15493  lcmgcdlem  15534  lcmf  15561  prmind2  15612  coprm  15636  prmfac1  15644  prmndvdsfaclt  15648  divdenle  15670  qnumgt0  15671  zsqrtelqelz  15679  hashdvds  15693  eulerthlem2  15700  odzdvds  15713  modprm1div  15715  vfermltl  15719  modprm0  15723  pythagtriplem11  15743  pythagtriplem13  15745  pythagtriplem19  15751  pclem  15756  pcpre1  15760  pcidlem  15789  dvdsprmpweqle  15803  pcadd  15806  pcmpt  15809  pcmpt2  15810  pcfaclem  15815  pcfac  15816  qexpz  15818  pockthlem  15822  pockthg  15823  prmreclem1  15833  prmreclem3  15835  prmreclem4  15836  prmreclem5  15837  1arithlem4  15843  1arith  15844  4sqlem5  15859  4sqlem6  15860  4sqlem10  15864  mul4sqlem  15870  4sqlem11  15872  4sqlem12  15873  4sqlem13  15874  4sqlem14  15875  4sqlem15  15876  4sqlem16  15877  4sqlem17  15878  vdwlem1  15898  vdwlem3  15900  vdwlem6  15903  vdwlem9  15906  vdwlem10  15907  vdwlem12  15909  vdwnnlem3  15914  ramub1lem1  15943  prmolefac  15963  prmgaplem4  15971  prmgaplem5  15972  prmgaplem6  15973  prmgaplem8  15975  2expltfac  16007  cshwshashnsame  16018  setsstruct2  16103  psgnunilem4  18114  mndodconglem  18157  oddvds  18163  sylow1lem1  18210  sylow1lem5  18214  fislw  18237  efgredlem  18357  gexexlem  18452  zringlpirlem3  20038  prmirredlem  20045  fvmptnn04if  20864  fvmptnn04ifb  20866  fvmptnn04ifc  20867  fvmptnn04ifd  20868  chfacfisf  20869  chfacfisfcpmat  20870  chfacfscmulgsum  20875  chfacfpmmulgsum  20879  lebnumii  22975  lmnn  23271  ovolunlem1a  23476  ovoliunlem1  23482  ovolicc2lem3  23499  ovolicc2lem4  23500  iundisj  23528  voliunlem1  23530  uniioombllem3  23565  dyadf  23571  dyadovol  23573  dyaddisjlem  23575  dyadmaxlem  23577  opnmbllem  23581  vitalilem4  23591  mbfi1fseqlem1  23695  mbfi1fseqlem3  23697  mbfi1fseqlem4  23698  mbfi1fseqlem5  23699  mbfi1fseqlem6  23700  itg2gt0  23740  itg2cnlem2  23742  dgreq0  24234  dgrco  24244  elqaalem2  24288  aaliou3lem2  24311  aaliou3lem8  24313  aaliou3lem9  24318  leibpi  24882  log2tlbnd  24885  birthdaylem3  24893  amgm  24930  emcllem2  24936  harmonicbnd4  24950  lgamgulmlem1  24968  lgamgulmlem2  24969  lgamgulmlem3  24970  lgamgulmlem4  24971  lgamgulmlem5  24972  lgamgulmlem6  24973  lgamucov  24977  lgamcvg2  24994  wilthlem1  25007  ftalem5  25016  basellem1  25020  basellem2  25021  basellem3  25022  basellem4  25023  basellem5  25024  basellem6  25025  basellem8  25027  chtge0  25051  chtwordi  25095  vma1  25105  dvdsflf1o  25126  dvdsflsumcom  25127  fsumfldivdiaglem  25128  sgmmul  25139  chtublem  25149  fsumvma2  25152  logfac2  25155  chpchtsum  25157  chpub  25158  logfaclbnd  25160  logexprlim  25163  mersenne  25165  perfectlem2  25168  dchrelbas4  25181  bposlem1  25222  bposlem2  25223  bposlem3  25224  bposlem4  25225  bposlem5  25226  bposlem6  25227  bposlem7  25228  bposlem9  25230  lgslem1  25235  lgsval2lem  25245  lgsdirprm  25269  lgsdir  25270  lgsne0  25273  lgsqrlem2  25285  gausslemma2dlem0h  25301  gausslemma2dlem0i  25302  gausslemma2dlem1a  25303  gausslemma2dlem2  25305  gausslemma2dlem7  25311  gausslemma2d  25312  lgseisenlem1  25313  lgseisenlem2  25314  lgseisenlem3  25315  lgseisenlem4  25316  lgseisen  25317  lgsquadlem1  25318  lgsquadlem2  25319  lgsquadlem3  25320  m1lgs  25326  2sqlem3  25358  2sqlem8  25364  2sqblem  25369  chebbnd1lem1  25371  chebbnd1lem3  25373  chtppilimlem1  25375  rplogsumlem1  25386  rplogsumlem2  25387  dchrisum0lem1a  25388  rpvmasumlem  25389  dchrisumlema  25390  dchrisumlem1  25391  dchrisumlem2  25392  dchrisumlem3  25393  dchrvmasumiflem1  25403  dchrisum0flblem2  25411  dchrisum0re  25415  dchrisum0lem1b  25417  dchrisum0lem1  25418  dirith2  25430  selbergb  25451  selberg2lem  25452  logdivbnd  25458  selberg3lem2  25460  selberg4lem1  25462  pntrsumo1  25467  pntrsumbnd2  25469  pntrlog2bndlem1  25479  pntrlog2bndlem2  25480  pntrlog2bndlem3  25481  pntrlog2bndlem4  25482  pntrlog2bndlem5  25483  pntpbnd1a  25487  pntpbnd1  25488  pntibndlem2a  25492  pntibndlem2  25493  pntlemg  25500  pntlemh  25501  pntlemj  25505  pntlemf  25507  ostth2lem1  25520  padicabvf  25533  padicabvcxp  25534  ostth2lem2  25536  ostth2lem3  25537  ostth2lem4  25538  ostth2  25539  ostth3  25540  clwlksfclwwlkOLD  27235  numclwwlk5  27575  numclwwlk7  27578  ubthlem2  28054  minvecolem4  28063  iundisjf  29726  ssnnssfz  29875  iundisjfi  29881  2sqmod  29972  pmtrto1cl  30173  psgnfzto1stlem  30174  fzto1st1  30176  fzto1st  30177  psgnfzto1st  30179  smatrcl  30186  smattr  30189  smatbl  30190  smatbr  30191  1smat1  30194  submateqlem1  30197  submateqlem2  30198  submateq  30199  esumcst  30449  fiunelros  30561  oddpwdc  30740  eulerpartlems  30746  eulerpartlemgc  30748  fiblem  30784  dstfrvunirn  30860  dstfrvclim1  30863  ballotlemimin  30891  fsum2dsub  31009  reprinfz1  31024  hgt750lemd  31050  hgt750lemb  31058  hgt750leme  31060  tgoldbachgtde  31062  tgoldbachgt  31065  subfaclim  31491  subfacval3  31492  erdszelem7  31500  erdszelem8  31501  erdsze2lem2  31507  cvmliftlem2  31589  cvmliftlem6  31593  cvmliftlem7  31594  cvmliftlem8  31595  cvmliftlem9  31596  cvmliftlem10  31597  cvmliftlem13  31599  bcprod  31944  bccolsum  31945  faclimlem2  31950  faclim2  31954  nn0prpwlem  32636  knoppndvlem15  32832  knoppndvlem17  32834  knoppndvlem18  32835  knoppndvlem19  32836  knoppndvlem20  32837  knoppndvlem21  32838  poimirlem3  33723  poimirlem6  33726  poimirlem7  33727  poimirlem8  33728  poimirlem9  33729  poimirlem10  33730  poimirlem11  33731  poimirlem12  33732  poimirlem13  33733  poimirlem15  33735  poimirlem16  33736  poimirlem17  33737  poimirlem19  33739  poimirlem20  33740  poimirlem21  33741  poimirlem22  33742  poimirlem23  33743  poimirlem26  33746  poimirlem28  33748  opnmbllem0  33756  mblfinlem2  33758  incsequz  33853  nninfnub  33856  irrapxlem3  37887  irrapxlem4  37888  irrapxlem5  37889  pellexlem2  37893  pellexlem6  37897  pell14qrgt0  37922  pell14qrgapw  37939  pellfundgt1  37946  rmspecsqrtnq  37969  ltrmxnn0  38014  jm3.1lem1  38082  jm3.1lem3  38084  dgraa0p  38217  hashnzfz2  39017  rfcnnnub  39686  nnxrd  39692  fzisoeu  39992  fsumnncl  40280  sumnnodd  40339  limsup10exlem  40481  stoweidlem1  40694  stoweidlem3  40696  stoweidlem11  40704  stoweidlem17  40710  stoweidlem20  40713  stoweidlem25  40718  stoweidlem26  40719  stoweidlem34  40727  stoweidlem38  40731  stoweidlem42  40735  stoweidlem44  40737  stoweidlem51  40744  stoweidlem59  40752  stoweidlem60  40753  wallispi  40763  wallispi2  40766  stirlinglem3  40769  stirlinglem4  40770  stirlinglem8  40774  stirlinglem10  40776  stirlinglem12  40778  stirlinglem15  40781  dirkertrigeqlem2  40792  dirkertrigeqlem3  40793  dirkercncflem2  40797  fourierdlem11  40811  fourierdlem14  40814  fourierdlem15  40815  fourierdlem20  40820  fourierdlem31  40831  fourierdlem64  40863  fourierdlem93  40892  fourierdlem95  40894  fourierdlem103  40902  fourierdlem104  40903  fourierdlem112  40911  sqwvfourb  40922  etransclem3  40930  etransclem19  40946  etransclem23  40950  etransclem24  40951  etransclem25  40952  etransclem32  40959  etransclem35  40962  etransclem41  40968  etransclem48  40975  qndenserrnbllem  40990  hoiqssbllem1  41315  hoiqssbllem2  41316  ovolval5lem1  41345  ovolval5lem2  41346  iccpartlt  41932  iccpartgt  41935  odz2prm2pw  42047  fmtnoprmfac1lem  42048  2pwp1prm  42075  sfprmdvdsmersenne  42092  lighneallem2  42095  proththdlem  42102  perfectALTVlem2  42203  gbowge7  42223  ztprmneprm  42690  pgrple2abl  42711  logbpw2m1  42926  nnpw2pmod  42942  nnolog2flm1  42949  blennngt2o2  42951
  Copyright terms: Public domain W3C validator