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

Theorem nnred 11644
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 11633 . 2 ℕ ⊆ ℝ
2 nnred.1 . 2 (𝜑𝐴 ∈ ℕ)
31, 2sseldi 3916 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  cr 10529  cn 11629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-i2m1 10598  ax-1ne0 10599  ax-rrecex 10602  ax-cnre 10603
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-nn 11630
This theorem is referenced by:  nnne0  11663  uzwo3  12335  modmulnn  13256  bernneq3  13592  expmulnbnd  13596  expnngt1b  13603  facwordi  13649  faclbnd  13650  faclbnd2  13651  faclbnd3  13652  faclbnd5  13658  faclbnd6  13659  facubnd  13660  facavg  13661  bcp1nk  13677  hashf1  13815  swrds2  14297  isercolllem1  15016  isercoll  15019  o1fsum  15163  climcndslem1  15199  climcndslem2  15200  climcnds  15201  eftabs  15424  efcllem  15426  ege2le3  15438  efcj  15440  eftlub  15457  eflegeo  15469  eirrlem  15552  fzm1ndvds  15667  nno  15726  nnoddm1d2  15730  bitsfzolem  15776  bitsfzo  15777  bitsinv1lem  15783  sadcaddlem  15799  smueqlem  15832  bezoutlem3  15882  bezoutlem4  15883  sqgcd  15902  lcmgcdlem  15943  lcmf  15970  prmind2  16022  coprm  16048  prmfac1  16056  prmndvdsfaclt  16060  divdenle  16082  qnumgt0  16083  zsqrtelqelz  16091  hashdvds  16105  eulerthlem2  16112  odzdvds  16125  vfermltl  16131  modprm0  16135  pythagtriplem11  16155  pythagtriplem13  16157  pythagtriplem19  16163  pclem  16168  pcpre1  16172  pcidlem  16201  dvdsprmpweqle  16215  pcadd  16218  pcmpt  16221  pcmpt2  16222  pcfaclem  16227  pcfac  16228  qexpz  16230  pockthlem  16234  pockthg  16235  prmreclem1  16245  prmreclem3  16247  prmreclem4  16248  prmreclem5  16249  1arithlem4  16255  1arith  16256  4sqlem5  16271  4sqlem6  16272  4sqlem10  16276  mul4sqlem  16282  4sqlem11  16284  4sqlem12  16285  4sqlem13  16286  4sqlem14  16287  4sqlem15  16288  4sqlem16  16289  4sqlem17  16290  vdwlem1  16310  vdwlem3  16312  vdwlem6  16315  vdwlem9  16318  vdwlem10  16319  vdwlem12  16321  vdwnnlem3  16326  ramub1lem1  16355  prmolefac  16375  prmgaplem4  16383  prmgaplem5  16384  prmgaplem6  16385  prmgaplem8  16387  2expltfac  16421  cshwshashnsame  16432  setsstruct2  16516  psgnunilem4  18620  mndodconglem  18664  oddvds  18670  sylow1lem1  18718  sylow1lem5  18722  fislw  18745  efgredlem  18868  gexexlem  18968  zringlpirlem3  20182  prmirredlem  20189  fvmptnn04if  21457  fvmptnn04ifb  21459  fvmptnn04ifc  21460  fvmptnn04ifd  21461  chfacfisf  21462  chfacfisfcpmat  21463  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  lebnumii  23574  lmnn  23870  ovolunlem1a  24103  ovoliunlem1  24109  ovolicc2lem3  24126  ovolicc2lem4  24127  iundisj  24155  voliunlem1  24157  uniioombllem3  24192  dyadf  24198  dyadovol  24200  dyaddisjlem  24202  dyadmaxlem  24204  opnmbllem  24208  vitalilem4  24218  mbfi1fseqlem1  24322  mbfi1fseqlem3  24324  mbfi1fseqlem4  24325  mbfi1fseqlem5  24326  mbfi1fseqlem6  24327  itg2gt0  24367  itg2cnlem2  24369  dgreq0  24865  dgrco  24875  elqaalem2  24919  aaliou3lem2  24942  aaliou3lem8  24944  aaliou3lem9  24949  leibpi  25531  log2tlbnd  25534  birthdaylem3  25542  amgm  25579  emcllem2  25585  harmonicbnd4  25599  lgamgulmlem1  25617  lgamgulmlem2  25618  lgamgulmlem3  25619  lgamgulmlem4  25620  lgamgulmlem5  25621  lgamgulmlem6  25622  lgamucov  25626  lgamcvg2  25643  wilthlem1  25656  ftalem5  25665  basellem1  25669  basellem2  25670  basellem3  25671  basellem4  25672  basellem5  25673  basellem6  25674  basellem8  25676  chtge0  25700  chtwordi  25744  vma1  25754  dvdsflf1o  25775  dvdsflsumcom  25776  fsumfldivdiaglem  25777  sgmmul  25788  chtublem  25798  fsumvma2  25801  logfac2  25804  chpchtsum  25806  chpub  25807  logfaclbnd  25809  logexprlim  25812  mersenne  25814  perfectlem2  25817  dchrelbas4  25830  bposlem1  25871  bposlem2  25872  bposlem3  25873  bposlem4  25874  bposlem5  25875  bposlem6  25876  bposlem7  25877  bposlem9  25879  lgslem1  25884  lgsval2lem  25894  lgsdirprm  25918  lgsdir  25919  lgsne0  25922  lgsqrlem2  25934  gausslemma2dlem0h  25950  gausslemma2dlem0i  25951  gausslemma2dlem1a  25952  gausslemma2dlem2  25954  gausslemma2dlem7  25960  gausslemma2d  25961  lgseisenlem1  25962  lgseisenlem2  25963  lgseisenlem3  25964  lgseisenlem4  25965  lgseisen  25966  lgsquadlem1  25967  lgsquadlem2  25968  lgsquadlem3  25969  2sqlem3  26007  2sqlem8  26013  2sqblem  26018  2sqmod  26023  chebbnd1lem1  26056  chebbnd1lem3  26058  chtppilimlem1  26060  rplogsumlem1  26071  rplogsumlem2  26072  dchrisum0lem1a  26073  rpvmasumlem  26074  dchrisumlema  26075  dchrisumlem1  26076  dchrisumlem2  26077  dchrisumlem3  26078  dchrvmasumiflem1  26088  dchrisum0flblem2  26096  dchrisum0re  26100  dchrisum0lem1b  26102  dchrisum0lem1  26103  dirith2  26115  selbergb  26136  selberg2lem  26137  logdivbnd  26143  selberg3lem2  26145  selberg4lem1  26147  pntrsumo1  26152  pntrsumbnd2  26154  pntrlog2bndlem1  26164  pntrlog2bndlem2  26165  pntrlog2bndlem3  26166  pntrlog2bndlem4  26167  pntrlog2bndlem5  26168  pntpbnd1a  26172  pntpbnd1  26173  pntibndlem2a  26177  pntibndlem2  26178  pntlemg  26185  pntlemh  26186  pntlemj  26190  pntlemf  26192  ostth2lem1  26205  padicabvf  26218  padicabvcxp  26219  ostth2lem2  26221  ostth2lem3  26222  ostth2lem4  26223  ostth2  26224  ostth3  26225  numclwwlk5  28176  numclwwlk7  28179  ubthlem2  28657  minvecolem4  28666  iundisjf  30355  ssnnssfz  30539  iundisjfi  30548  pfxlsw2ccat  30655  pmtrto1cl  30794  psgnfzto1stlem  30795  fzto1st1  30797  fzto1st  30798  psgnfzto1st  30800  cycpmco2lem6  30826  cycpmco2lem7  30827  smatrcl  31149  smattr  31152  smatbl  31153  smatbr  31154  1smat1  31157  submateqlem1  31160  submateqlem2  31161  submateq  31162  esumcst  31430  fiunelros  31541  oddpwdc  31720  eulerpartlems  31726  eulerpartlemgc  31728  fiblem  31764  dstfrvunirn  31840  dstfrvclim1  31843  ballotlemimin  31871  fsum2dsub  31986  reprinfz1  32001  hgt750lemd  32027  hgt750lemb  32035  hgt750leme  32037  tgoldbachgtde  32039  tgoldbachgt  32042  subfaclim  32543  subfacval3  32544  erdszelem7  32552  erdszelem8  32553  erdsze2lem2  32559  cvmliftlem2  32641  cvmliftlem6  32645  cvmliftlem7  32646  cvmliftlem8  32647  cvmliftlem9  32648  cvmliftlem10  32649  cvmliftlem13  32651  bcprod  33078  bccolsum  33079  faclimlem2  33084  faclim2  33088  nn0prpwlem  33778  knoppndvlem15  33973  knoppndvlem17  33975  knoppndvlem18  33976  knoppndvlem19  33977  knoppndvlem20  33978  knoppndvlem21  33979  poimirlem3  35053  poimirlem6  35056  poimirlem7  35057  poimirlem8  35058  poimirlem9  35059  poimirlem10  35060  poimirlem11  35061  poimirlem12  35062  poimirlem13  35063  poimirlem15  35065  poimirlem16  35066  poimirlem17  35067  poimirlem19  35069  poimirlem20  35070  poimirlem21  35071  poimirlem22  35072  poimirlem23  35073  poimirlem26  35076  poimirlem28  35078  opnmbllem0  35086  mblfinlem2  35088  incsequz  35179  nninfnub  35182  lcmineqlem4  39313  lcmineqlem10  39319  lcmineqlem11  39320  lcmineqlem15  39324  lcmineqlem18  39327  lcmineqlem19  39328  lcmineqlem20  39329  lcmineqlem21  39330  lcmineqlem22  39331  lcmineqlem23  39332  lcmineqlem  39333  2ap1caineq  39340  metakunt1  39341  metakunt2  39342  metakunt6  39346  metakunt7  39347  metakunt9  39349  metakunt10  39350  metakunt11  39351  metakunt12  39352  metakunt16  39356  metakunt18  39358  metakunt20  39360  metakunt22  39362  metakunt24  39364  metakunt27  39367  metakunt28  39368  metakunt29  39369  metakunt30  39370  nnadddir  39458  oexpreposd  39474  nn0expgcd  39479  rtprmirr  39489  fltltc  39604  fltnltalem  39605  fltnlta  39606  3cubeslem3r  39615  irrapxlem3  39752  irrapxlem4  39753  irrapxlem5  39754  pellexlem2  39758  pellexlem6  39762  pell14qrgt0  39787  pell14qrgapw  39804  pellfundgt1  39811  rmspecsqrtnq  39834  ltrmxnn0  39877  jm3.1lem1  39945  jm3.1lem3  39947  dgraa0p  40080  hashnzfz2  41012  rfcnnnub  41652  nnxrd  41658  fzisoeu  41919  fsumnncl  42200  sumnnodd  42259  limsup10exlem  42401  stoweidlem1  42630  stoweidlem3  42632  stoweidlem11  42640  stoweidlem17  42646  stoweidlem20  42649  stoweidlem25  42654  stoweidlem26  42655  stoweidlem34  42663  stoweidlem38  42667  stoweidlem42  42671  stoweidlem44  42673  stoweidlem51  42680  stoweidlem59  42688  stoweidlem60  42689  wallispi  42699  wallispi2  42702  stirlinglem3  42705  stirlinglem4  42706  stirlinglem8  42710  stirlinglem10  42712  stirlinglem12  42714  stirlinglem15  42717  dirkertrigeqlem2  42728  dirkertrigeqlem3  42729  dirkercncflem2  42733  fourierdlem11  42747  fourierdlem14  42750  fourierdlem15  42751  fourierdlem20  42756  fourierdlem31  42767  fourierdlem64  42799  fourierdlem93  42828  fourierdlem95  42830  fourierdlem103  42838  fourierdlem104  42839  fourierdlem112  42847  sqwvfourb  42858  etransclem3  42866  etransclem19  42882  etransclem23  42886  etransclem24  42887  etransclem25  42888  etransclem32  42895  etransclem35  42898  etransclem41  42904  etransclem48  42911  qndenserrnbllem  42923  hoiqssbllem1  43248  hoiqssbllem2  43249  ovolval5lem1  43278  ovolval5lem2  43279  iccpartlt  43928  iccpartgt  43931  odz2prm2pw  44067  fmtnoprmfac1lem  44068  2pwp1prm  44093  sfprmdvdsmersenne  44108  lighneallem2  44111  proththdlem  44118  perfectALTVlem2  44227  gbowge7  44268  ztprmneprm  44736  pgrple2abl  44754  logbpw2m1  44968  nnpw2pmod  44984  nnolog2flm1  44991  blennngt2o2  44993  itcovalt2lem2lem1  45074
  Copyright terms: Public domain W3C validator