Theorem nnred 9051

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

Syntax hints:   -> wi 4   e. wcel 2176   RRcr 7926   NNcn 9038

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-sep 4163  ax-cnex 8018  ax-resscn 8019  ax-1re 8021  ax-addrcl 8024

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-v 2774  df-in 3172  df-ss 3179  df-int 3886  df-inn 9039

This theorem is referenced by:  exbtwnzlemstep  10392  qbtwnrelemcalc  10400  qbtwnre  10401  flqdiv  10468  modqmulnn  10489  modifeq2int  10533  modaddmodup  10534  modaddmodlo  10535  modsumfzodifsn  10543  addmodlteq  10545  bernneq3  10809  expnbnd  10810  facwordi  10887  faclbnd  10888  faclbnd2  10889  faclbnd3  10890  faclbnd6  10891  facubnd  10892  facavg  10893  bcp1nk  10909  bcval5  10910  caucvgrelemcau  11324  caucvgre  11325  cvg1nlemcxze  11326  cvg1nlemcau  11328  cvg1nlemres  11329  resqrexlemdecn  11356  resqrexlemga  11367  fsum3cvg3  11740  divcnv  11841  cvgratnnlembern  11867  cvgratnnlemseq  11870  cvgratnnlemabsle  11871  cvgratnnlemsumlt  11872  cvgratnnlemrate  11874  cvgratz  11876  eftabs  12000  efcllemp  12002  ege2le3  12015  efcj  12017  eftlub  12034  eflegeo  12045  eirraplem  12121  dvdslelemd  12187  nno  12250  nnoddm1d2  12254  divalglemnqt  12264  divalglemeunn  12265  bitsfzolem  12298  bitsfzo  12299  bitsinv1lem  12305  dvdsbnd  12310  sqgcd  12383  uzwodc  12391  lcmgcdlem  12432  ncoprmgcdne1b  12444  prmind2  12475  isprm5lem  12496  coprm  12499  prmfac1  12507  sqrt2irraplemnn  12534  divdenle  12552  qnumgt0  12553  nn0sqrtelqelz  12561  hashdvds  12576  eulerthlemrprm  12584  eulerthlema  12585  odzdvds  12601  pythagtriplem11  12630  pythagtriplem12  12631  pythagtriplem13  12632  pythagtriplem14  12633  pythagtriplem19  12638  pclemub  12643  pcpre1  12648  pcidlem  12679  dvdsprmpweqle  12693  pcadd  12696  pcmpt  12699  pcmpt2  12700  pcfaclem  12705  pcfac  12706  qexpz  12708  pockthlem  12712  pockthg  12713  1arith  12723  4sqlem5  12738  4sqlem6  12739  4sqlem10  12743  mul4sqlem  12749  4sqlem11  12757  4sqlem12  12758  4sqlem13m  12759  4sqlem14  12760  4sqlem15  12761  4sqlem16  12762  4sqlem17  12763  2expltfac  12795  znnen  12802  exmidunben  12830  nninfdclemp1  12854  nninfdclemlt  12855  nninfdclemf1  12856  strleund  12968  strext  12970  psrbaglesuppg  14467  logbgcd1irraplemexp  15473  logbgcd1irraplemap  15474  wilthlem1  15485  mersenne  15502  perfectlem2  15505  lgslem1  15510  lgsval2lem  15520  lgsdirprm  15544  lgsdir  15545  gausslemma2dlem0h  15566  gausslemma2dlem1a  15568  gausslemma2dlem2  15572  lgseisenlem1  15580  lgseisenlem2  15581  lgseisenlem3  15582  lgseisen  15584  lgsquadlem1  15587  lgsquadlem2  15588  lgsquadlem3  15589  2sqlem3  15627  2sqlem8  15633  cvgcmp2nlemabs  16008