Theorem nnred 9326

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 9317	. 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 8184   NNcn 9313

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 4251  ax-cnex 8276  ax-resscn 8277  ax-1re 8279  ax-addrcl 8282

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 9314

This theorem is used by:  exbtwnzlemstep  10698  qbtwnrelemcalc  10706  qbtwnre  10707  flqdiv  10778  modqmulnn  10799  modifeq2int  10843  modaddmodup  10844  modaddmodlo  10845  modsumfzodifsn  10853  addmodlteq  10855  bernneq3  11120  expnbnd  11121  facwordi  11199  faclbnd  11200  faclbnd2  11201  faclbnd3  11202  faclbnd6  11203  facubnd  11204  facavg  11205  bcp1nk  11221  bcval5  11222  hashf1  11308  caucvgrelemcau  11767  caucvgre  11768  cvg1nlemcxze  11769  cvg1nlemcau  11771  cvg1nlemres  11772  resqrexlemdecn  11799  resqrexlemga  11810  fsum3cvg3  12187  divcnv  12288  cvgratnnlembern  12314  cvgratnnlemseq  12317  cvgratnnlemabsle  12318  cvgratnnlemsumlt  12319  cvgratnnlemrate  12321  cvgratz  12323  eftabs  12447  efcllemp  12449  ege2le3  12462  efcj  12464  eftlub  12481  eflegeo  12492  eirraplem  12568  dvdslelemd  12634  nno  12697  nnoddm1d2  12701  divalglemnqt  12711  divalglemeunn  12712  bitsfzolem  12745  bitsfzo  12746  bitsinv1lem  12752  dvdsbnd  12757  sqgcd  12830  uzwodc  12838  lcmgcdlem  12879  ncoprmgcdne1b  12891  prmind2  12922  isprm5lem  12944  coprm  12947  prmfac1  12955  sqrt2irraplemnn  12983  divdenle  13001  qnumgt0  13002  nn0sqrtelqelz  13010  hashdvds  13027  eulerthlemrprm  13035  eulerthlema  13036  odzdvds  13052  pythagtriplem11  13081  pythagtriplem12  13082  pythagtriplem13  13083  pythagtriplem14  13084  pythagtriplem19  13089  pclemub  13094  pcpre1  13099  pcidlem  13130  dvdsprmpweqle  13144  pcadd  13147  pcmpt  13150  pcmpt2  13151  pcfaclem  13156  pcfac  13157  qexpz  13159  pockthlem  13163  pockthg  13164  1arith  13174  4sqlem5  13189  4sqlem6  13190  4sqlem10  13194  mul4sqlem  13200  4sqlem11  13208  4sqlem12  13209  4sqlem13m  13210  4sqlem14  13211  4sqlem15  13212  4sqlem16  13213  4sqlem17  13214  2expltfac  13247  ballotfilemonn  13278  ballotfilemimin  13306  znnen  13346  exmidunben  13374  nninfdclemp1  13398  nninfdclemlt  13399  nninfdclemf1  13400  strleund  13515  strext  13517  psrbaglesuppg  15170  logfac  16143  logbgcd1irraplemexp  16221  logbgcd1irraplemap  16222  zprmlogbaplem1  16232  zprmlogbaplem2  16233  log2tlbndlog2  16237  birthdaylem3  16244  pellexlem2  16247  wilthlem1  16249  chtqge0  16264  chtqwordi  16280  ppiqltx  16298  chtublem  16312  mersenne  16314  perfectlem2  16317  prmefexple  16325  bposlem1  16328  bposlem2  16329  bposlem3  16330  bposlem4  16331  bposlem5  16332  bposlem6  16333  bposlem7  16334  bposlem9  16336  lgslem1  16341  lgsval2lem  16351  lgsdirprm  16375  lgsdir  16376  gausslemma2dlem0h  16397  gausslemma2dlem1a  16399  gausslemma2dlem2  16403  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgseisen  16415  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  2sqlem3  16458  2sqlem8  16464  cvgcmp2nlemabs  17304