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

Theorem nnrp 11793
Description: A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.)
Assertion
Ref Expression
nnrp (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)

Proof of Theorem nnrp
StepHypRef Expression
1 nnre 10978 . 2 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2 nngt0 11000 . 2 (𝐴 ∈ ℕ → 0 < 𝐴)
3 elrp 11785 . 2 (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
41, 2, 3sylanbrc 697 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987   class class class wbr 4618  cr 9886  0cc0 9887   < clt 10025  cn 10971  +crp 11783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-er 7694  df-en 7907  df-dom 7908  df-sdom 7909  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-nn 10972  df-rp 11784
This theorem is referenced by:  nnrpd  11821  nn0ledivnn  11892  adddivflid  12566  divfl0  12572  fldivnn0le  12580  zmodcl  12637  zmodfz  12639  zmodid2  12645  m1modnnsub1  12663  addmodid  12665  modifeq2int  12679  modaddmodup  12680  modaddmodlo  12681  modsumfzodifsn  12690  addmodlteq  12692  nnesq  12935  digit2  12944  digit1  12945  bcrpcl  13042  bcval5  13052  lswccatn0lsw  13319  cshw0  13484  cshwmodn  13485  cshwsublen  13486  cshwidxmod  13493  cshwidxmodr  13494  cshwidxm1  13497  cshwidxm  13498  repswcshw  13502  2cshw  13503  cshweqrep  13511  modfsummods  14459  divcnv  14517  supcvg  14520  harmonic  14523  expcnv  14528  rpnnen2lem11  14885  sqrt2irr  14910  dvdsval3  14918  moddvds  14922  mulmoddvds  14982  divalgmod  15060  divalgmodOLD  15061  flodddiv4  15068  modgcd  15184  divgcdcoprm0  15310  isprm5  15350  isprm6  15357  nnnn0modprm0  15442  pythagtriplem13  15463  fldivp1  15532  prmreclem5  15555  prmreclem6  15556  4sqlem12  15591  modxai  15703  modsubi  15707  mulgmodid  17509  odmodnn0  17887  gexdvds  17927  sylow1lem1  17941  gexexlem  18183  znf1o  19828  met1stc  22245  lmnn  22980  bcthlem5  23044  minveclem3  23119  vitalilem4  23299  vitali  23301  ismbf3d  23340  itg2seq  23428  plyeq0lem  23883  elqaalem3  23993  aalioulem6  24009  aaliou  24010  logtayllem  24318  atan1  24568  leibpi  24582  birthdaylem2  24592  dfef2  24610  divsqrtsumlem  24619  emcllem1  24635  emcllem2  24636  emcllem3  24637  emcllem4  24638  emcllem6  24640  zetacvg  24654  lgam1  24703  ppiub  24842  vmalelog  24843  logfacbnd3  24861  logexprlim  24863  bcmono  24915  bclbnd  24918  bposlem1  24922  bposlem7  24928  bposlem8  24929  bposlem9  24930  gausslemma2dlem1a  25003  gausslemma2dlem4  25007  gausslemma2dlem6  25010  m1lgs  25026  2lgslem1a1  25027  2lgslem3a1  25038  2lgslem3b1  25039  2lgslem3c1  25040  2lgslem3d1  25041  2lgslem4  25044  2lgsoddprmlem2  25047  rplogsumlem1  25086  dchrisumlema  25090  dchrisumlem2  25092  dchrisumlem3  25093  dchrvmasumlem2  25100  dchrvmasumiflem1  25103  dchrisum0lem1b  25117  dchrisum0lem2a  25119  rplogsum  25129  logdivsum  25135  mulog2sumlem2  25137  logsqvma  25144  logsqvma2  25145  log2sumbnd  25146  selberg2lem  25152  logdivbnd  25158  pntrsumo1  25167  pntrsumbnd  25168  pntibndlem1  25191  pntibndlem2  25193  pntibndlem3  25194  pntlemd  25196  pntlema  25198  pntlemb  25199  pntlemr  25204  pntlemj  25205  pntlemf  25207  pntlemo  25209  crctcshwlkn0lem5  26588  crctcshwlkn0lem6  26589  lnconi  28759  circum  31303  bccolsum  31360  faclimlem3  31366  faclim  31367  poimirlem29  33097  poimirlem30  33098  poimirlem31  33099  poimirlem32  33100  mblfinlem3  33107  itg2addnclem2  33121  itg2addnclem3  33122  itg2addnc  33123  pellexlem4  36903  pell1qrgaplem  36944  pellqrex  36950  congrep  37047  acongeq  37057  proot1ex  37287  hashnzfzclim  38030  xrralrecnnle  39089  nnrecrp  39092  xrralrecnnge  39100  iooiinicc  39203  iooiinioc  39217  fprodsubrecnncnvlem  39447  fprodaddrecnncnvlem  39449  wallispilem4  39613  wallispi  39615  wallispi2lem1  39616  wallispi2lem2  39617  stirlinglem1  39619  stirlinglem2  39620  stirlinglem3  39621  stirlinglem4  39622  stirlinglem6  39624  stirlinglem7  39625  stirlinglem10  39628  stirlinglem11  39629  stirlinglem13  39631  stirlinglem14  39632  stirlinglem15  39633  stirlingr  39635  dirkertrigeqlem1  39643  hoicvrrex  40098  ovnsubaddlem2  40113  hoiqssbllem3  40166  iinhoiicc  40216  iunhoiioo  40218  vonioolem1  40222  vonioolem2  40223  vonicclem1  40225  vonicclem2  40226  preimageiingt  40258  preimaleiinlt  40259  fsummmodsndifre  40663  mod42tp1mod8  40839  lighneallem2  40843  3exp4mod41  40853  41prothprmlem2  40855  perfectALTVlem2  40947  mod0mul  41623  modn0mul  41624  m1modmmod  41625  difmodm1lt  41626  nnlog2ge0lt1  41673  blennnelnn  41683  nnpw2blen  41687  blen1b  41695  blennnt2  41696  blennn0e2  41701  dignn0fr  41708  dignn0ldlem  41709  dignnld  41710  dig2nn1st  41712  dig0  41713
  Copyright terms: Public domain W3C validator