Theorem nnrp 11842

Description: A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.)

Assertion

Ref	Expression
nnrp	|- ( A e. NN -> A e. RR+ )

Proof of Theorem nnrp

Step	Hyp	Ref	Expression
1		nnre 11027	. 2 |- ( A e. NN -> A e. RR )
2		nngt0 11049	. 2 |- ( A e. NN -> 0 < A )
3		elrp 11834	. 2 |- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
4	1, 2, 3	sylanbrc 698	1 |- ( A e. NN -> A e. RR+ )

Syntax hints:   -> wi 4   e. wcel 1990   class class class wbr 4653   RRcr 9935   0cc0 9936   < clt 10074   NNcn 11020   RR+crp 11832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-rp 11833

This theorem is referenced by:  nnrpd  11870  nn0ledivnn  11941  adddivflid  12619  divfl0  12625  fldivnn0le  12633  zmodcl  12690  zmodfz  12692  zmodid2  12698  m1modnnsub1  12716  addmodid  12718  modifeq2int  12732  modaddmodup  12733  modaddmodlo  12734  modsumfzodifsn  12743  addmodlteq  12745  nnesq  12988  digit2  12997  digit1  12998  bcrpcl  13095  bcval5  13105  lswccatn0lsw  13373  cshw0  13540  cshwmodn  13541  cshwsublen  13542  cshwidxmod  13549  cshwidxmodr  13550  cshwidxm1  13553  cshwidxm  13554  repswcshw  13558  2cshw  13559  cshweqrep  13567  modfsummods  14525  divcnv  14585  supcvg  14588  harmonic  14591  expcnv  14596  rpnnen2lem11  14953  sqrt2irr  14979  dvdsval3  14987  moddvds  14991  mulmoddvds  15051  divalgmod  15129  divalgmodOLD  15130  flodddiv4  15137  modgcd  15253  divgcdcoprm0  15379  isprm5  15419  isprm6  15426  nnnn0modprm0  15511  pythagtriplem13  15532  fldivp1  15601  prmreclem5  15624  prmreclem6  15625  4sqlem12  15660  modxai  15772  modsubi  15776  mulgmodid  17581  odmodnn0  17959  gexdvds  17999  sylow1lem1  18013  gexexlem  18255  znf1o  19900  met1stc  22326  lmnn  23061  bcthlem5  23125  minveclem3  23200  vitalilem4  23380  vitali  23382  ismbf3d  23421  itg2seq  23509  plyeq0lem  23966  elqaalem3  24076  aalioulem6  24092  aaliou  24093  logtayllem  24405  atan1  24655  leibpi  24669  birthdaylem2  24679  dfef2  24697  divsqrtsumlem  24706  emcllem1  24722  emcllem2  24723  emcllem3  24724  emcllem4  24725  emcllem6  24727  zetacvg  24741  lgam1  24790  ppiub  24929  vmalelog  24930  logfacbnd3  24948  logexprlim  24950  bcmono  25002  bclbnd  25005  bposlem1  25009  bposlem7  25015  bposlem8  25016  bposlem9  25017  gausslemma2dlem1a  25090  gausslemma2dlem4  25094  gausslemma2dlem6  25097  m1lgs  25113  2lgslem1a1  25114  2lgslem3a1  25125  2lgslem3b1  25126  2lgslem3c1  25127  2lgslem3d1  25128  2lgslem4  25131  2lgsoddprmlem2  25134  rplogsumlem1  25173  dchrisumlema  25177  dchrisumlem2  25179  dchrisumlem3  25180  dchrvmasumlem2  25187  dchrvmasumiflem1  25190  dchrisum0lem1b  25204  dchrisum0lem2a  25206  rplogsum  25216  logdivsum  25222  mulog2sumlem2  25224  logsqvma  25231  logsqvma2  25232  log2sumbnd  25233  selberg2lem  25239  logdivbnd  25245  pntrsumo1  25254  pntrsumbnd  25255  pntibndlem1  25278  pntibndlem2  25280  pntibndlem3  25281  pntlemd  25283  pntlema  25285  pntlemb  25286  pntlemr  25291  pntlemj  25292  pntlemf  25294  pntlemo  25296  crctcshwlkn0lem5  26706  crctcshwlkn0lem6  26707  lnconi  28892  rpdp2cl  29589  rpdp2cl2  29590  hgt750lem  30729  hgt750lem2  30730  hgt750leme  30736  circum  31568  bccolsum  31625  faclimlem3  31631  faclim  31632  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  mblfinlem3  33448  itg2addnclem2  33462  itg2addnclem3  33463  itg2addnc  33464  pellexlem4  37396  pell1qrgaplem  37437  pellqrex  37443  congrep  37540  acongeq  37550  proot1ex  37779  hashnzfzclim  38521  xrralrecnnle  39602  nnrecrp  39605  xrralrecnnge  39613  iooiinicc  39769  iooiinioc  39783  fprodsubrecnncnvlem  40121  fprodaddrecnncnvlem  40123  wallispilem4  40285  wallispi  40287  wallispi2lem1  40288  wallispi2lem2  40289  stirlinglem1  40291  stirlinglem2  40292  stirlinglem3  40293  stirlinglem4  40294  stirlinglem6  40296  stirlinglem7  40297  stirlinglem10  40300  stirlinglem11  40301  stirlinglem13  40303  stirlinglem14  40304  stirlinglem15  40305  stirlingr  40307  dirkertrigeqlem1  40315  hoicvrrex  40770  ovnsubaddlem2  40785  hoiqssbllem3  40838  iinhoiicc  40888  iunhoiioo  40890  vonioolem1  40894  vonioolem2  40895  vonicclem1  40897  vonicclem2  40898  preimageiingt  40930  preimaleiinlt  40931  fsummmodsndifre  41344  mod42tp1mod8  41519  lighneallem2  41523  3exp4mod41  41533  41prothprmlem2  41535  perfectALTVlem2  41631  mod0mul  42314  modn0mul  42315  m1modmmod  42316  difmodm1lt  42317  nnlog2ge0lt1  42360  blennnelnn  42370  nnpw2blen  42374  blen1b  42382  blennnt2  42383  blennn0e2  42388  dignn0fr  42395  dignn0ldlem  42396  dignnld  42397  dig2nn1st  42399  dig0  42400