Theorem nnred 8895

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

Syntax hints:   -> wi 4   e. wcel 2142   RRcr 7777   NNcn 8882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153  ax-sep 4108  ax-cnex 7869  ax-resscn 7870  ax-1re 7872  ax-addrcl 7875

This theorem depends on definitions:  df-bi 116  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ral 2454  df-v 2733  df-in 3128  df-ss 3135  df-int 3833  df-inn 8883

This theorem is referenced by:  exbtwnzlemstep  10208  qbtwnrelemcalc  10216  qbtwnre  10217  flqdiv  10281  modqmulnn  10302  modifeq2int  10346  modaddmodup  10347  modaddmodlo  10348  modsumfzodifsn  10356  addmodlteq  10358  bernneq3  10602  expnbnd  10603  facwordi  10678  faclbnd  10679  faclbnd2  10680  faclbnd3  10681  faclbnd6  10682  facubnd  10683  facavg  10684  bcp1nk  10700  bcval5  10701  caucvgrelemcau  10948  caucvgre  10949  cvg1nlemcxze  10950  cvg1nlemcau  10952  cvg1nlemres  10953  resqrexlemdecn  10980  resqrexlemga  10991  fsum3cvg3  11363  divcnv  11464  cvgratnnlembern  11490  cvgratnnlemseq  11493  cvgratnnlemabsle  11494  cvgratnnlemsumlt  11495  cvgratnnlemrate  11497  cvgratz  11499  eftabs  11623  efcllemp  11625  ege2le3  11638  efcj  11640  eftlub  11657  eflegeo  11668  eirraplem  11743  dvdslelemd  11807  nno  11869  nnoddm1d2  11873  divalglemnqt  11883  divalglemeunn  11884  dvdsbnd  11915  sqgcd  11988  uzwodc  11996  lcmgcdlem  12035  ncoprmgcdne1b  12047  prmind2  12078  isprm5lem  12099  coprm  12102  prmfac1  12110  sqrt2irraplemnn  12137  divdenle  12155  qnumgt0  12156  nn0sqrtelqelz  12164  hashdvds  12179  eulerthlemrprm  12187  eulerthlema  12188  odzdvds  12203  pythagtriplem11  12232  pythagtriplem12  12233  pythagtriplem13  12234  pythagtriplem14  12235  pythagtriplem19  12240  pclemub  12245  pcpre1  12250  pcidlem  12280  dvdsprmpweqle  12294  pcadd  12297  pcmpt  12299  pcmpt2  12300  pcfaclem  12305  pcfac  12306  qexpz  12308  pockthlem  12312  pockthg  12313  1arith  12323  4sqlem5  12338  4sqlem6  12339  4sqlem10  12343  mul4sqlem  12349  znnen  12357  exmidunben  12385  nninfdclemp1  12409  nninfdclemlt  12410  nninfdclemf1  12411  strleund  12510  logbgcd1irraplemexp  13765  logbgcd1irraplemap  13766  lgslem1  13780  lgsval2lem  13790  lgsdirprm  13814  lgsdir  13815  2sqlem3  13832  2sqlem8  13838  cvgcmp2nlemabs  14149