Theorem nnred 9319

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   RRcr 8178   NNcn 9306

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4249  ax-cnex 8270  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823  df-in 3226  df-ss 3233  df-int 3971  df-inn 9307

This theorem is used by:  exbtwnzlemstep  10692  qbtwnrelemcalc  10700  qbtwnre  10701  flqdiv  10771  modqmulnn  10792  modifeq2int  10836  modaddmodup  10837  modaddmodlo  10838  modsumfzodifsn  10846  addmodlteq  10848  bernneq3  11113  expnbnd  11114  facwordi  11192  faclbnd  11193  faclbnd2  11194  faclbnd3  11195  faclbnd6  11196  facubnd  11197  facavg  11198  bcp1nk  11214  bcval5  11215  hashf1  11301  caucvgrelemcau  11760  caucvgre  11761  cvg1nlemcxze  11762  cvg1nlemcau  11764  cvg1nlemres  11765  resqrexlemdecn  11792  resqrexlemga  11803  fsum3cvg3  12179  divcnv  12280  cvgratnnlembern  12306  cvgratnnlemseq  12309  cvgratnnlemabsle  12310  cvgratnnlemsumlt  12311  cvgratnnlemrate  12313  cvgratz  12315  eftabs  12439  efcllemp  12441  ege2le3  12454  efcj  12456  eftlub  12473  eflegeo  12484  eirraplem  12560  dvdslelemd  12626  nno  12689  nnoddm1d2  12693  divalglemnqt  12703  divalglemeunn  12704  bitsfzolem  12737  bitsfzo  12738  bitsinv1lem  12744  dvdsbnd  12749  sqgcd  12822  uzwodc  12830  lcmgcdlem  12871  ncoprmgcdne1b  12883  prmind2  12914  isprm5lem  12936  coprm  12939  prmfac1  12947  sqrt2irraplemnn  12975  divdenle  12993  qnumgt0  12994  nn0sqrtelqelz  13002  hashdvds  13019  eulerthlemrprm  13027  eulerthlema  13028  odzdvds  13044  pythagtriplem11  13073  pythagtriplem12  13074  pythagtriplem13  13075  pythagtriplem14  13076  pythagtriplem19  13081  pclemub  13086  pcpre1  13091  pcidlem  13122  dvdsprmpweqle  13136  pcadd  13139  pcmpt  13142  pcmpt2  13143  pcfaclem  13148  pcfac  13149  qexpz  13151  pockthlem  13155  pockthg  13156  1arith  13166  4sqlem5  13181  4sqlem6  13182  4sqlem10  13186  mul4sqlem  13192  4sqlem11  13200  4sqlem12  13201  4sqlem13m  13202  4sqlem14  13203  4sqlem15  13204  4sqlem16  13205  4sqlem17  13206  2expltfac  13239  ballotfilemonn  13270  ballotfilemimin  13298  znnen  13338  exmidunben  13366  nninfdclemp1  13390  nninfdclemlt  13391  nninfdclemf1  13392  strleund  13506  strext  13508  psrbaglesuppg  15106  logfac  16048  logbgcd1irraplemexp  16123  logbgcd1irraplemap  16124  zprmlogbaplem1  16134  zprmlogbaplem2  16135  log2tlbndlog2  16139  birthdaylem3  16146  pellexlem2  16149  wilthlem1  16151  ppiqltx  16183  mersenne  16195  perfectlem2  16198  prmefexple  16206  bposlem1  16209  bposlem2  16210  bposlem3  16211  bposlem4  16212  bposlem5  16213  lgslem1  16217  lgsval2lem  16227  lgsdirprm  16251  lgsdir  16252  gausslemma2dlem0h  16273  gausslemma2dlem1a  16275  gausslemma2dlem2  16279  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgseisen  16291  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  2sqlem3  16334  2sqlem8  16340  cvgcmp2nlemabs  17179