Theorem nnred 9134

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

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 8009   NNcn 9121

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4202  ax-cnex 8101  ax-resscn 8102  ax-1re 8104  ax-addrcl 8107

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801  df-in 3203  df-ss 3210  df-int 3924  df-inn 9122

This theorem is referenced by:  exbtwnzlemstep  10479  qbtwnrelemcalc  10487  qbtwnre  10488  flqdiv  10555  modqmulnn  10576  modifeq2int  10620  modaddmodup  10621  modaddmodlo  10622  modsumfzodifsn  10630  addmodlteq  10632  bernneq3  10896  expnbnd  10897  facwordi  10974  faclbnd  10975  faclbnd2  10976  faclbnd3  10977  faclbnd6  10978  facubnd  10979  facavg  10980  bcp1nk  10996  bcval5  10997  caucvgrelemcau  11507  caucvgre  11508  cvg1nlemcxze  11509  cvg1nlemcau  11511  cvg1nlemres  11512  resqrexlemdecn  11539  resqrexlemga  11550  fsum3cvg3  11923  divcnv  12024  cvgratnnlembern  12050  cvgratnnlemseq  12053  cvgratnnlemabsle  12054  cvgratnnlemsumlt  12055  cvgratnnlemrate  12057  cvgratz  12059  eftabs  12183  efcllemp  12185  ege2le3  12198  efcj  12200  eftlub  12217  eflegeo  12228  eirraplem  12304  dvdslelemd  12370  nno  12433  nnoddm1d2  12437  divalglemnqt  12447  divalglemeunn  12448  bitsfzolem  12481  bitsfzo  12482  bitsinv1lem  12488  dvdsbnd  12493  sqgcd  12566  uzwodc  12574  lcmgcdlem  12615  ncoprmgcdne1b  12627  prmind2  12658  isprm5lem  12679  coprm  12682  prmfac1  12690  sqrt2irraplemnn  12717  divdenle  12735  qnumgt0  12736  nn0sqrtelqelz  12744  hashdvds  12759  eulerthlemrprm  12767  eulerthlema  12768  odzdvds  12784  pythagtriplem11  12813  pythagtriplem12  12814  pythagtriplem13  12815  pythagtriplem14  12816  pythagtriplem19  12821  pclemub  12826  pcpre1  12831  pcidlem  12862  dvdsprmpweqle  12876  pcadd  12879  pcmpt  12882  pcmpt2  12883  pcfaclem  12888  pcfac  12889  qexpz  12891  pockthlem  12895  pockthg  12896  1arith  12906  4sqlem5  12921  4sqlem6  12922  4sqlem10  12926  mul4sqlem  12932  4sqlem11  12940  4sqlem12  12941  4sqlem13m  12942  4sqlem14  12943  4sqlem15  12944  4sqlem16  12945  4sqlem17  12946  2expltfac  12978  znnen  12985  exmidunben  13013  nninfdclemp1  13037  nninfdclemlt  13038  nninfdclemf1  13039  strleund  13152  strext  13154  psrbaglesuppg  14652  logbgcd1irraplemexp  15658  logbgcd1irraplemap  15659  wilthlem1  15670  mersenne  15687  perfectlem2  15690  lgslem1  15695  lgsval2lem  15705  lgsdirprm  15729  lgsdir  15730  gausslemma2dlem0h  15751  gausslemma2dlem1a  15753  gausslemma2dlem2  15757  lgseisenlem1  15765  lgseisenlem2  15766  lgseisenlem3  15767  lgseisen  15769  lgsquadlem1  15772  lgsquadlem2  15773  lgsquadlem3  15774  2sqlem3  15812  2sqlem8  15818  cvgcmp2nlemabs  16488