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

Theorem nnrp 12045
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 11229 . 2 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2 nngt0 11251 . 2 (𝐴 ∈ ℕ → 0 < 𝐴)
3 elrp 12037 . 2 (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
41, 2, 3sylanbrc 572 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145   class class class wbr 4786  cr 10137  0cc0 10138   < clt 10276  cn 11222  +crp 12035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-nn 11223  df-rp 12036
This theorem is referenced by:  nnrpd  12073  nn0ledivnn  12146  adddivflid  12827  divfl0  12833  fldivnn0le  12841  zmodcl  12898  zmodfz  12900  zmodid2  12906  m1modnnsub1  12924  addmodid  12926  modifeq2int  12940  modaddmodup  12941  modaddmodlo  12942  modsumfzodifsn  12951  addmodlteq  12953  nnesq  13195  digit2  13204  digit1  13205  bcrpcl  13299  bcval5  13309  lswccatn0lsw  13573  cshw0  13749  cshwmodn  13750  cshwsublen  13751  cshwidxmod  13758  cshwidxmodr  13759  cshwidxm1  13762  cshwidxm  13763  repswcshw  13767  2cshw  13768  cshweqrep  13776  modfsummods  14732  divcnv  14792  supcvg  14795  harmonic  14798  expcnv  14803  rpnnen2lem11  15159  sqrt2irr  15185  dvdsval3  15193  dvdsmodexp  15197  moddvds  15200  divalgmod  15337  divalgmodOLD  15338  flodddiv4  15345  modgcd  15461  divgcdcoprm0  15586  isprm5  15626  isprm6  15633  nnnn0modprm0  15718  pythagtriplem13  15739  fldivp1  15808  prmreclem5  15831  prmreclem6  15832  4sqlem12  15867  modxai  15979  modsubi  15983  mulgmodid  17789  odmodnn0  18166  gexdvds  18206  sylow1lem1  18220  gexexlem  18462  znf1o  20115  met1stc  22546  lmnn  23280  bcthlem5  23344  minveclem3  23419  vitalilem4  23599  vitali  23601  ismbf3d  23641  itg2seq  23729  plyeq0lem  24186  elqaalem3  24296  aalioulem6  24312  aaliou  24313  logtayllem  24626  atan1  24876  leibpi  24890  birthdaylem2  24900  dfef2  24918  divsqrtsumlem  24927  emcllem1  24943  emcllem2  24944  emcllem3  24945  emcllem4  24946  emcllem6  24948  zetacvg  24962  lgam1  25011  ppiub  25150  vmalelog  25151  logfacbnd3  25169  logexprlim  25171  bcmono  25223  bclbnd  25226  bposlem1  25230  bposlem7  25236  bposlem8  25237  bposlem9  25238  gausslemma2dlem1a  25311  gausslemma2dlem4  25315  gausslemma2dlem6  25318  m1lgs  25334  2lgslem1a1  25335  2lgslem3a1  25346  2lgslem3b1  25347  2lgslem3c1  25348  2lgslem3d1  25349  2lgslem4  25352  2lgsoddprmlem2  25355  rplogsumlem1  25394  dchrisumlema  25398  dchrisumlem2  25400  dchrisumlem3  25401  dchrvmasumlem2  25408  dchrvmasumiflem1  25411  dchrisum0lem1b  25425  dchrisum0lem2a  25427  rplogsum  25437  logdivsum  25443  mulog2sumlem2  25445  logsqvma  25452  logsqvma2  25453  log2sumbnd  25454  selberg2lem  25460  logdivbnd  25466  pntrsumo1  25475  pntrsumbnd  25476  pntibndlem1  25499  pntibndlem2  25501  pntibndlem3  25502  pntlemd  25504  pntlema  25506  pntlemb  25507  pntlemr  25512  pntlemj  25513  pntlemf  25515  pntlemo  25517  crctcshwlkn0lem5  26942  crctcshwlkn0lem6  26943  lnconi  29232  rpdp2cl  29929  rpdp2cl2  29930  hgt750lem  31069  hgt750lem2  31070  hgt750leme  31076  circum  31906  bccolsum  31963  faclimlem3  31969  faclim  31970  poimirlem29  33771  poimirlem30  33772  poimirlem31  33773  poimirlem32  33774  mblfinlem3  33781  itg2addnclem2  33794  itg2addnclem3  33795  itg2addnc  33796  pellexlem4  37922  pell1qrgaplem  37963  pellqrex  37969  congrep  38066  acongeq  38076  proot1ex  38305  hashnzfzclim  39047  xrralrecnnle  40118  nnrecrp  40121  xrralrecnnge  40129  iooiinicc  40287  iooiinioc  40301  fprodsubrecnncnvlem  40639  fprodaddrecnncnvlem  40641  wallispilem4  40802  wallispi  40804  wallispi2lem1  40805  wallispi2lem2  40806  stirlinglem1  40808  stirlinglem2  40809  stirlinglem3  40810  stirlinglem4  40811  stirlinglem6  40813  stirlinglem7  40814  stirlinglem10  40817  stirlinglem11  40818  stirlinglem13  40820  stirlinglem14  40821  stirlinglem15  40822  stirlingr  40824  dirkertrigeqlem1  40832  hoicvrrex  41290  ovnsubaddlem2  41305  hoiqssbllem3  41358  iinhoiicc  41408  iunhoiioo  41410  vonioolem1  41414  vonioolem2  41415  vonicclem1  41417  vonicclem2  41418  preimageiingt  41450  preimaleiinlt  41451  fsummmodsndifre  41872  mod42tp1mod8  42047  lighneallem2  42051  3exp4mod41  42061  41prothprmlem2  42063  perfectALTVlem2  42159  mod0mul  42842  modn0mul  42843  m1modmmod  42844  difmodm1lt  42845  nnlog2ge0lt1  42888  blennnelnn  42898  nnpw2blen  42902  blen1b  42910  blennnt2  42911  blennn0e2  42916  dignn0fr  42923  dignn0ldlem  42924  dignnld  42925  dig2nn1st  42927  dig0  42928
  Copyright terms: Public domain W3C validator