Theorem nnred 9250

Description: A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnred.1	|- ( ph -> A e. NN )

Assertion

Ref	Expression
nnred	|- ( ph -> A e. RR )

Proof of Theorem nnred

Step	Hyp	Ref	Expression
1		nnssre 9241	. 2 |- NN C_ RR
2		nnred.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sselid 3236	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2203   RRcr 8126   NNcn 9237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-sep 4228  ax-cnex 8218  ax-resscn 8219  ax-1re 8221  ax-addrcl 8224

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-v 2815  df-in 3217  df-ss 3224  df-int 3950  df-inn 9238

This theorem is referenced by:  exbtwnzlemstep  10607  qbtwnrelemcalc  10615  qbtwnre  10616  flqdiv  10683  modqmulnn  10704  modifeq2int  10748  modaddmodup  10749  modaddmodlo  10750  modsumfzodifsn  10758  addmodlteq  10760  bernneq3  11024  expnbnd  11025  facwordi  11102  faclbnd  11103  faclbnd2  11104  faclbnd3  11105  faclbnd6  11106  facubnd  11107  facavg  11108  bcp1nk  11124  bcval5  11125  caucvgrelemcau  11665  caucvgre  11666  cvg1nlemcxze  11667  cvg1nlemcau  11669  cvg1nlemres  11670  resqrexlemdecn  11697  resqrexlemga  11708  fsum3cvg3  12082  divcnv  12183  cvgratnnlembern  12209  cvgratnnlemseq  12212  cvgratnnlemabsle  12213  cvgratnnlemsumlt  12214  cvgratnnlemrate  12216  cvgratz  12218  eftabs  12342  efcllemp  12344  ege2le3  12357  efcj  12359  eftlub  12376  eflegeo  12387  eirraplem  12463  dvdslelemd  12529  nno  12592  nnoddm1d2  12596  divalglemnqt  12606  divalglemeunn  12607  bitsfzolem  12640  bitsfzo  12641  bitsinv1lem  12647  dvdsbnd  12652  sqgcd  12725  uzwodc  12733  lcmgcdlem  12774  ncoprmgcdne1b  12786  prmind2  12817  isprm5lem  12838  coprm  12841  prmfac1  12849  sqrt2irraplemnn  12876  divdenle  12894  qnumgt0  12895  nn0sqrtelqelz  12903  hashdvds  12918  eulerthlemrprm  12926  eulerthlema  12927  odzdvds  12943  pythagtriplem11  12972  pythagtriplem12  12973  pythagtriplem13  12974  pythagtriplem14  12975  pythagtriplem19  12980  pclemub  12985  pcpre1  12990  pcidlem  13021  dvdsprmpweqle  13035  pcadd  13038  pcmpt  13041  pcmpt2  13042  pcfaclem  13047  pcfac  13048  qexpz  13050  pockthlem  13054  pockthg  13055  1arith  13065  4sqlem5  13080  4sqlem6  13081  4sqlem10  13085  mul4sqlem  13091  4sqlem11  13099  4sqlem12  13100  4sqlem13m  13101  4sqlem14  13102  4sqlem15  13103  4sqlem16  13104  4sqlem17  13105  2expltfac  13137  ballotfilemonn  13140  znnen  13149  exmidunben  13177  nninfdclemp1  13201  nninfdclemlt  13202  nninfdclemf1  13203  strleund  13316  strext  13318  psrbaglesuppg  14821  logbgcd1irraplemexp  15833  logbgcd1irraplemap  15834  pellexlem2  15846  wilthlem1  15848  mersenne  15865  perfectlem2  15868  lgslem1  15873  lgsval2lem  15883  lgsdirprm  15907  lgsdir  15908  gausslemma2dlem0h  15929  gausslemma2dlem1a  15931  gausslemma2dlem2  15935  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisen  15947  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  2sqlem3  15990  2sqlem8  15996  cvgcmp2nlemabs  16816