Theorem nnred 9155

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 9146	. 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 8030   NNcn 9142

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 8122  ax-resscn 8123  ax-1re 8125  ax-addrcl 8128

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 9143

This theorem is referenced by:  exbtwnzlemstep  10506  qbtwnrelemcalc  10514  qbtwnre  10515  flqdiv  10582  modqmulnn  10603  modifeq2int  10647  modaddmodup  10648  modaddmodlo  10649  modsumfzodifsn  10657  addmodlteq  10659  bernneq3  10923  expnbnd  10924  facwordi  11001  faclbnd  11002  faclbnd2  11003  faclbnd3  11004  faclbnd6  11005  facubnd  11006  facavg  11007  bcp1nk  11023  bcval5  11024  caucvgrelemcau  11540  caucvgre  11541  cvg1nlemcxze  11542  cvg1nlemcau  11544  cvg1nlemres  11545  resqrexlemdecn  11572  resqrexlemga  11583  fsum3cvg3  11956  divcnv  12057  cvgratnnlembern  12083  cvgratnnlemseq  12086  cvgratnnlemabsle  12087  cvgratnnlemsumlt  12088  cvgratnnlemrate  12090  cvgratz  12092  eftabs  12216  efcllemp  12218  ege2le3  12231  efcj  12233  eftlub  12250  eflegeo  12261  eirraplem  12337  dvdslelemd  12403  nno  12466  nnoddm1d2  12470  divalglemnqt  12480  divalglemeunn  12481  bitsfzolem  12514  bitsfzo  12515  bitsinv1lem  12521  dvdsbnd  12526  sqgcd  12599  uzwodc  12607  lcmgcdlem  12648  ncoprmgcdne1b  12660  prmind2  12691  isprm5lem  12712  coprm  12715  prmfac1  12723  sqrt2irraplemnn  12750  divdenle  12768  qnumgt0  12769  nn0sqrtelqelz  12777  hashdvds  12792  eulerthlemrprm  12800  eulerthlema  12801  odzdvds  12817  pythagtriplem11  12846  pythagtriplem12  12847  pythagtriplem13  12848  pythagtriplem14  12849  pythagtriplem19  12854  pclemub  12859  pcpre1  12864  pcidlem  12895  dvdsprmpweqle  12909  pcadd  12912  pcmpt  12915  pcmpt2  12916  pcfaclem  12921  pcfac  12922  qexpz  12924  pockthlem  12928  pockthg  12929  1arith  12939  4sqlem5  12954  4sqlem6  12955  4sqlem10  12959  mul4sqlem  12965  4sqlem11  12973  4sqlem12  12974  4sqlem13m  12975  4sqlem14  12976  4sqlem15  12977  4sqlem16  12978  4sqlem17  12979  2expltfac  13011  znnen  13018  exmidunben  13046  nninfdclemp1  13070  nninfdclemlt  13071  nninfdclemf1  13072  strleund  13185  strext  13187  psrbaglesuppg  14685  logbgcd1irraplemexp  15691  logbgcd1irraplemap  15692  wilthlem1  15703  mersenne  15720  perfectlem2  15723  lgslem1  15728  lgsval2lem  15738  lgsdirprm  15762  lgsdir  15763  gausslemma2dlem0h  15784  gausslemma2dlem1a  15786  gausslemma2dlem2  15790  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgseisen  15802  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  2sqlem3  15845  2sqlem8  15851  cvgcmp2nlemabs  16636