Theorem nnred 9156

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 9147	. 2 |- NN C_ RR
2		nnred.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sselid 3225	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8031   NNcn 9143

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8123  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804  df-in 3206  df-ss 3213  df-int 3929  df-inn 9144

This theorem is referenced by:  exbtwnzlemstep  10508  qbtwnrelemcalc  10516  qbtwnre  10517  flqdiv  10584  modqmulnn  10605  modifeq2int  10649  modaddmodup  10650  modaddmodlo  10651  modsumfzodifsn  10659  addmodlteq  10661  bernneq3  10925  expnbnd  10926  facwordi  11003  faclbnd  11004  faclbnd2  11005  faclbnd3  11006  faclbnd6  11007  facubnd  11008  facavg  11009  bcp1nk  11025  bcval5  11026  caucvgrelemcau  11558  caucvgre  11559  cvg1nlemcxze  11560  cvg1nlemcau  11562  cvg1nlemres  11563  resqrexlemdecn  11590  resqrexlemga  11601  fsum3cvg3  11975  divcnv  12076  cvgratnnlembern  12102  cvgratnnlemseq  12105  cvgratnnlemabsle  12106  cvgratnnlemsumlt  12107  cvgratnnlemrate  12109  cvgratz  12111  eftabs  12235  efcllemp  12237  ege2le3  12250  efcj  12252  eftlub  12269  eflegeo  12280  eirraplem  12356  dvdslelemd  12422  nno  12485  nnoddm1d2  12489  divalglemnqt  12499  divalglemeunn  12500  bitsfzolem  12533  bitsfzo  12534  bitsinv1lem  12540  dvdsbnd  12545  sqgcd  12618  uzwodc  12626  lcmgcdlem  12667  ncoprmgcdne1b  12679  prmind2  12710  isprm5lem  12731  coprm  12734  prmfac1  12742  sqrt2irraplemnn  12769  divdenle  12787  qnumgt0  12788  nn0sqrtelqelz  12796  hashdvds  12811  eulerthlemrprm  12819  eulerthlema  12820  odzdvds  12836  pythagtriplem11  12865  pythagtriplem12  12866  pythagtriplem13  12867  pythagtriplem14  12868  pythagtriplem19  12873  pclemub  12878  pcpre1  12883  pcidlem  12914  dvdsprmpweqle  12928  pcadd  12931  pcmpt  12934  pcmpt2  12935  pcfaclem  12940  pcfac  12941  qexpz  12943  pockthlem  12947  pockthg  12948  1arith  12958  4sqlem5  12973  4sqlem6  12974  4sqlem10  12978  mul4sqlem  12984  4sqlem11  12992  4sqlem12  12993  4sqlem13m  12994  4sqlem14  12995  4sqlem15  12996  4sqlem16  12997  4sqlem17  12998  2expltfac  13030  znnen  13037  exmidunben  13065  nninfdclemp1  13089  nninfdclemlt  13090  nninfdclemf1  13091  strleund  13204  strext  13206  psrbaglesuppg  14705  logbgcd1irraplemexp  15711  logbgcd1irraplemap  15712  wilthlem1  15723  mersenne  15740  perfectlem2  15743  lgslem1  15748  lgsval2lem  15758  lgsdirprm  15782  lgsdir  15783  gausslemma2dlem0h  15804  gausslemma2dlem1a  15806  gausslemma2dlem2  15810  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisen  15822  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  2sqlem3  15865  2sqlem8  15871  cvgcmp2nlemabs  16687