Theorem nnred 9158

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

Syntax hints:   -> wi 4   e. wcel 2201   RRcr 8033   NNcn 9145

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 2212  ax-sep 4206  ax-cnex 8125  ax-resscn 8126  ax-1re 8128  ax-addrcl 8131

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-v 2803  df-in 3205  df-ss 3212  df-int 3928  df-inn 9146

This theorem is referenced by:  exbtwnzlemstep  10510  qbtwnrelemcalc  10518  qbtwnre  10519  flqdiv  10586  modqmulnn  10607  modifeq2int  10651  modaddmodup  10652  modaddmodlo  10653  modsumfzodifsn  10661  addmodlteq  10663  bernneq3  10927  expnbnd  10928  facwordi  11005  faclbnd  11006  faclbnd2  11007  faclbnd3  11008  faclbnd6  11009  facubnd  11010  facavg  11011  bcp1nk  11027  bcval5  11028  caucvgrelemcau  11560  caucvgre  11561  cvg1nlemcxze  11562  cvg1nlemcau  11564  cvg1nlemres  11565  resqrexlemdecn  11592  resqrexlemga  11603  fsum3cvg3  11977  divcnv  12078  cvgratnnlembern  12104  cvgratnnlemseq  12107  cvgratnnlemabsle  12108  cvgratnnlemsumlt  12109  cvgratnnlemrate  12111  cvgratz  12113  eftabs  12237  efcllemp  12239  ege2le3  12252  efcj  12254  eftlub  12271  eflegeo  12282  eirraplem  12358  dvdslelemd  12424  nno  12487  nnoddm1d2  12491  divalglemnqt  12501  divalglemeunn  12502  bitsfzolem  12535  bitsfzo  12536  bitsinv1lem  12542  dvdsbnd  12547  sqgcd  12620  uzwodc  12628  lcmgcdlem  12669  ncoprmgcdne1b  12681  prmind2  12712  isprm5lem  12733  coprm  12736  prmfac1  12744  sqrt2irraplemnn  12771  divdenle  12789  qnumgt0  12790  nn0sqrtelqelz  12798  hashdvds  12813  eulerthlemrprm  12821  eulerthlema  12822  odzdvds  12838  pythagtriplem11  12867  pythagtriplem12  12868  pythagtriplem13  12869  pythagtriplem14  12870  pythagtriplem19  12875  pclemub  12880  pcpre1  12885  pcidlem  12916  dvdsprmpweqle  12930  pcadd  12933  pcmpt  12936  pcmpt2  12937  pcfaclem  12942  pcfac  12943  qexpz  12945  pockthlem  12949  pockthg  12950  1arith  12960  4sqlem5  12975  4sqlem6  12976  4sqlem10  12980  mul4sqlem  12986  4sqlem11  12994  4sqlem12  12995  4sqlem13m  12996  4sqlem14  12997  4sqlem15  12998  4sqlem16  12999  4sqlem17  13000  2expltfac  13032  znnen  13039  exmidunben  13067  nninfdclemp1  13091  nninfdclemlt  13092  nninfdclemf1  13093  strleund  13206  strext  13208  psrbaglesuppg  14707  logbgcd1irraplemexp  15718  logbgcd1irraplemap  15719  wilthlem1  15730  mersenne  15747  perfectlem2  15750  lgslem1  15755  lgsval2lem  15765  lgsdirprm  15789  lgsdir  15790  gausslemma2dlem0h  15811  gausslemma2dlem1a  15813  gausslemma2dlem2  15817  lgseisenlem1  15825  lgseisenlem2  15826  lgseisenlem3  15827  lgseisen  15829  lgsquadlem1  15832  lgsquadlem2  15833  lgsquadlem3  15834  2sqlem3  15872  2sqlem8  15878  cvgcmp2nlemabs  16698