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

Theorem nnrp 12062
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 11250 . 2 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2 nngt0 11272 . 2 (𝐴 ∈ ℕ → 0 < 𝐴)
3 elrp 12054 . 2 (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
41, 2, 3sylanbrc 573 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2148   class class class wbr 4797  cr 10158  0cc0 10159   < clt 10297  cn 11243  +crp 12052
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117  ax-resscn 10216  ax-1cn 10217  ax-icn 10218  ax-addcl 10219  ax-addrcl 10220  ax-mulcl 10221  ax-mulrcl 10222  ax-mulcom 10223  ax-addass 10224  ax-mulass 10225  ax-distr 10226  ax-i2m1 10227  ax-1ne0 10228  ax-1rid 10229  ax-rnegex 10230  ax-rrecex 10231  ax-cnre 10232  ax-pre-lttri 10233  ax-pre-lttrn 10234  ax-pre-ltadd 10235  ax-pre-mulgt0 10236
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-pss 3745  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-tp 4331  df-op 4333  df-uni 4586  df-iun 4667  df-br 4798  df-opab 4860  df-mpt 4877  df-tr 4900  df-id 5171  df-eprel 5176  df-po 5184  df-so 5185  df-fr 5222  df-we 5224  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-pred 5834  df-ord 5880  df-on 5881  df-lim 5882  df-suc 5883  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-riota 6773  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-om 7234  df-wrecs 7580  df-recs 7642  df-rdg 7680  df-er 7917  df-en 8131  df-dom 8132  df-sdom 8133  df-pnf 10299  df-mnf 10300  df-xr 10301  df-ltxr 10302  df-le 10303  df-sub 10491  df-neg 10492  df-nn 11244  df-rp 12053
This theorem is referenced by:  nnrpd  12090  nn0ledivnn  12163  adddivflid  12849  divfl0  12855  fldivnn0le  12863  zmodcl  12920  zmodfz  12922  zmodid2  12928  m1modnnsub1  12946  addmodid  12948  modifeq2int  12962  modaddmodup  12963  modaddmodlo  12964  modsumfzodifsn  12973  addmodlteq  12975  nnesq  13217  digit2  13226  digit1  13227  bcrpcl  13321  bcval5  13331  lswccatn0lsw  13595  cshw0  13771  cshwmodn  13772  cshwsublen  13773  cshwidxmod  13780  cshwidxmodr  13781  cshwidxm1  13784  cshwidxm  13785  repswcshw  13789  2cshw  13790  cshweqrep  13798  modfsummods  14754  divcnv  14814  supcvg  14817  harmonic  14820  expcnv  14825  rpnnen2lem11  15181  sqrt2irr  15207  dvdsval3  15215  dvdsmodexp  15219  moddvds  15222  divalgmod  15359  flodddiv4  15366  modgcd  15482  divgcdcoprm0  15607  isprm5  15646  isprm6  15653  nnnn0modprm0  15738  pythagtriplem13  15759  fldivp1  15828  prmreclem5  15851  prmreclem6  15852  4sqlem12  15887  modxai  15999  modsubi  16003  mulgmodid  17809  odmodnn0  18186  gexdvds  18226  sylow1lem1  18240  gexexlem  18482  znf1o  20135  met1stc  22566  lmnn  23300  bcthlem5  23364  minveclem3  23439  vitalilem4  23619  vitali  23621  ismbf3d  23662  itg2seq  23750  plyeq0lem  24207  elqaalem3  24317  aalioulem6  24333  aaliou  24334  logtayllem  24647  atan1  24897  leibpi  24911  birthdaylem2  24921  dfef2  24939  divsqrtsumlem  24948  emcllem1  24964  emcllem2  24965  emcllem3  24966  emcllem4  24967  emcllem6  24969  zetacvg  24983  lgam1  25032  ppiub  25171  vmalelog  25172  logfacbnd3  25190  logexprlim  25192  bcmono  25244  bclbnd  25247  bposlem1  25251  bposlem7  25257  bposlem8  25258  bposlem9  25259  gausslemma2dlem1a  25332  gausslemma2dlem4  25336  gausslemma2dlem6  25339  m1lgs  25355  2lgslem1a1  25356  2lgslem3a1  25367  2lgslem3b1  25368  2lgslem3c1  25369  2lgslem3d1  25370  2lgslem4  25373  2lgsoddprmlem2  25376  rplogsumlem1  25415  dchrisumlema  25419  dchrisumlem2  25421  dchrisumlem3  25422  dchrvmasumlem2  25429  dchrvmasumiflem1  25432  dchrisum0lem1b  25446  dchrisum0lem2a  25448  rplogsum  25458  logdivsum  25464  mulog2sumlem2  25466  logsqvma  25473  logsqvma2  25474  log2sumbnd  25475  selberg2lem  25481  logdivbnd  25487  pntrsumo1  25496  pntrsumbnd  25497  pntibndlem1  25520  pntibndlem2  25522  pntibndlem3  25523  pntlemd  25525  pntlema  25527  pntlemb  25528  pntlemr  25533  pntlemj  25534  pntlemf  25536  pntlemo  25538  crctcshwlkn0lem5  26963  crctcshwlkn0lem6  26964  lnconi  29249  rpdp2cl  29946  rpdp2cl2  29947  hgt750lem  31086  hgt750lem2  31087  hgt750leme  31093  circum  31923  bccolsum  31980  faclimlem3  31986  faclim  31987  poimirlem29  33788  poimirlem30  33789  poimirlem31  33790  poimirlem32  33791  mblfinlem3  33798  itg2addnclem2  33811  itg2addnclem3  33812  itg2addnc  33813  pellexlem4  37937  pell1qrgaplem  37978  pellqrex  37984  congrep  38081  acongeq  38091  proot1ex  38320  hashnzfzclim  39061  xrralrecnnle  40126  nnrecrp  40129  xrralrecnnge  40136  iooiinicc  40293  iooiinioc  40307  fprodsubrecnncnvlem  40645  fprodaddrecnncnvlem  40647  wallispilem4  40808  wallispi  40810  wallispi2lem1  40811  wallispi2lem2  40812  stirlinglem1  40814  stirlinglem2  40815  stirlinglem3  40816  stirlinglem4  40817  stirlinglem6  40819  stirlinglem7  40820  stirlinglem10  40823  stirlinglem11  40824  stirlinglem13  40826  stirlinglem14  40827  stirlinglem15  40828  stirlingr  40830  dirkertrigeqlem1  40838  hoicvrrex  41296  ovnsubaddlem2  41311  hoiqssbllem3  41364  iinhoiicc  41414  iunhoiioo  41416  vonioolem1  41420  vonioolem2  41421  vonicclem1  41423  vonicclem2  41424  preimageiingt  41456  preimaleiinlt  41457  fsummmodsndifre  41896  mod42tp1mod8  42071  lighneallem2  42075  3exp4mod41  42085  41prothprmlem2  42087  perfectALTVlem2  42183  mod0mul  42866  modn0mul  42867  m1modmmod  42868  difmodm1lt  42869  nnlog2ge0lt1  42912  blennnelnn  42922  nnpw2blen  42926  blen1b  42934  blennnt2  42935  blennn0e2  42940  dignn0fr  42947  dignn0ldlem  42948  dignnld  42949  dig2nn1st  42951  dig0  42952
  Copyright terms: Public domain W3C validator