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

Theorem nnrp 12394
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 11639 . 2 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2 nngt0 11662 . 2 (𝐴 ∈ ℕ → 0 < 𝐴)
3 elrp 12385 . 2 (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
41, 2, 3sylanbrc 585 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2110   class class class wbr 5059  cr 10530  0cc0 10531   < clt 10669  cn 11632  +crp 12383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-pred 6143  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-nn 11633  df-rp 12384
This theorem is referenced by:  nnrpd  12423  nn0ledivnn  12496  adddivflid  13182  divfl0  13188  fldivnn0le  13196  zmodcl  13253  zmodfz  13255  zmodid2  13261  m1modnnsub1  13279  addmodid  13281  modifeq2int  13295  modaddmodup  13296  modaddmodlo  13297  modsumfzodifsn  13306  addmodlteq  13308  nnesq  13582  digit2  13591  digit1  13592  bcrpcl  13662  bcval5  13672  lswccatn0lsw  13939  cshw0  14150  cshwmodn  14151  cshwsublen  14152  cshwidxmod  14159  cshwidxmodr  14160  cshwidxm1  14163  cshwidxm  14164  repswcshw  14168  2cshw  14169  cshweqrep  14177  modfsummods  15142  divcnv  15202  supcvg  15205  harmonic  15208  expcnv  15213  rpnnen2lem11  15571  sqrt2irr  15596  dvdsval3  15605  dvdsmodexp  15609  moddvds  15612  divalgmod  15751  flodddiv4  15758  modgcd  15874  divgcdcoprm0  16003  isprm5  16045  isprm6  16052  nnnn0modprm0  16137  pythagtriplem13  16158  fldivp1  16227  prmreclem5  16250  prmreclem6  16251  4sqlem12  16286  modxai  16398  modsubi  16402  smndex1iidm  18060  smndex1n0mnd  18071  mulgmodid  18260  odmodnn0  18662  gexdvds  18703  sylow1lem1  18717  gexexlem  18966  znf1o  20692  met1stc  23125  lmnn  23860  bcthlem5  23925  minveclem3  24026  vitali  24208  ismbf3d  24249  itg2seq  24337  plyeq0lem  24794  elqaalem3  24904  aalioulem6  24920  aaliou  24921  logtayllem  25236  sqrt2cxp2logb9e3  25371  atan1  25500  leibpi  25514  birthdaylem2  25524  dfef2  25542  divsqrtsumlem  25551  emcllem1  25567  emcllem2  25568  emcllem3  25569  emcllem4  25570  emcllem6  25572  zetacvg  25586  lgam1  25635  ppiub  25774  vmalelog  25775  logfacbnd3  25793  logexprlim  25795  bcmono  25847  bclbnd  25850  bposlem1  25854  bposlem7  25860  bposlem8  25861  bposlem9  25862  gausslemma2dlem1a  25935  gausslemma2dlem4  25939  gausslemma2dlem6  25942  m1lgs  25958  2lgslem1a1  25959  2lgslem3a1  25970  2lgslem3b1  25971  2lgslem3c1  25972  2lgslem3d1  25973  2lgslem4  25976  2lgsoddprmlem2  25979  2sqreultlem  26017  2sqreunnltlem  26020  rplogsumlem1  26054  dchrisumlema  26058  dchrisumlem2  26060  dchrisumlem3  26061  dchrvmasumlem2  26068  dchrvmasumiflem1  26071  dchrisum0lem1b  26085  dchrisum0lem2a  26087  rplogsum  26097  logdivsum  26103  mulog2sumlem2  26105  logsqvma  26112  logsqvma2  26113  log2sumbnd  26114  selberg2lem  26120  logdivbnd  26126  pntrsumo1  26135  pntrsumbnd  26136  pntibndlem1  26159  pntibndlem2  26161  pntibndlem3  26162  pntlemd  26164  pntlema  26166  pntlemb  26167  pntlemr  26172  pntlemj  26173  pntlemf  26175  pntlemo  26177  crctcshwlkn0lem5  27586  crctcshwlkn0lem6  27587  lnconi  29804  rpdp2cl  30553  rpdp2cl2  30554  hgt750lem  31917  hgt750lem2  31918  hgt750leme  31924  circum  32912  bccolsum  32966  faclimlem3  32972  faclim  32973  poimirlem29  34915  poimirlem30  34916  poimirlem31  34917  poimirlem32  34918  mblfinlem3  34925  itg2addnclem2  34938  itg2addnclem3  34939  itg2addnc  34940  pellexlem4  39422  pell1qrgaplem  39463  pellqrex  39469  congrep  39563  acongeq  39573  proot1ex  39794  hashnzfzclim  40647  xrralrecnnle  41645  nnrecrp  41648  xrralrecnnge  41654  iooiinicc  41810  iooiinioc  41824  fprodsubrecnncnvlem  42183  fprodaddrecnncnvlem  42185  wallispilem4  42346  wallispi  42348  wallispi2lem1  42349  wallispi2lem2  42350  stirlinglem1  42352  stirlinglem2  42353  stirlinglem3  42354  stirlinglem4  42355  stirlinglem6  42357  stirlinglem7  42358  stirlinglem10  42361  stirlinglem11  42362  stirlinglem13  42364  stirlinglem14  42365  stirlinglem15  42366  stirlingr  42368  dirkertrigeqlem1  42376  hoicvrrex  42831  ovnsubaddlem2  42846  hoiqssbllem3  42899  iinhoiicc  42949  iunhoiioo  42951  vonioolem1  42955  vonioolem2  42956  vonicclem1  42958  vonicclem2  42959  preimageiingt  42991  preimaleiinlt  42992  fsummmodsndifre  43527  mod42tp1mod8  43760  lighneallem2  43764  3exp4mod41  43774  41prothprmlem2  43776  perfectALTVlem2  43880  2exp340mod341  43891  8exp8mod9  43894  nfermltl8rev  43900  mod0mul  44572  modn0mul  44573  m1modmmod  44574  difmodm1lt  44575  nnlog2ge0lt1  44619  blennnelnn  44629  nnpw2blen  44633  blen1b  44641  blennnt2  44642  blennn0e2  44647  dignn0fr  44654  dignn0ldlem  44655  dignnld  44656  dig2nn1st  44658  dig0  44659
  Copyright terms: Public domain W3C validator