Theorem nnred 9320

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 9311	. 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 8179   NNcn 9307

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 8271  ax-resscn 8272  ax-1re 8274  ax-addrcl 8277

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 9308

This theorem is used by:  exbtwnzlemstep  10693  qbtwnrelemcalc  10701  qbtwnre  10702  flqdiv  10773  modqmulnn  10794  modifeq2int  10838  modaddmodup  10839  modaddmodlo  10840  modsumfzodifsn  10848  addmodlteq  10850  bernneq3  11115  expnbnd  11116  facwordi  11194  faclbnd  11195  faclbnd2  11196  faclbnd3  11197  faclbnd6  11198  facubnd  11199  facavg  11200  bcp1nk  11216  bcval5  11217  hashf1  11303  caucvgrelemcau  11762  caucvgre  11763  cvg1nlemcxze  11764  cvg1nlemcau  11766  cvg1nlemres  11767  resqrexlemdecn  11794  resqrexlemga  11805  fsum3cvg3  12182  divcnv  12283  cvgratnnlembern  12309  cvgratnnlemseq  12312  cvgratnnlemabsle  12313  cvgratnnlemsumlt  12314  cvgratnnlemrate  12316  cvgratz  12318  eftabs  12442  efcllemp  12444  ege2le3  12457  efcj  12459  eftlub  12476  eflegeo  12487  eirraplem  12563  dvdslelemd  12629  nno  12692  nnoddm1d2  12696  divalglemnqt  12706  divalglemeunn  12707  bitsfzolem  12740  bitsfzo  12741  bitsinv1lem  12747  dvdsbnd  12752  sqgcd  12825  uzwodc  12833  lcmgcdlem  12874  ncoprmgcdne1b  12886  prmind2  12917  isprm5lem  12939  coprm  12942  prmfac1  12950  sqrt2irraplemnn  12978  divdenle  12996  qnumgt0  12997  nn0sqrtelqelz  13005  hashdvds  13022  eulerthlemrprm  13030  eulerthlema  13031  odzdvds  13047  pythagtriplem11  13076  pythagtriplem12  13077  pythagtriplem13  13078  pythagtriplem14  13079  pythagtriplem19  13084  pclemub  13089  pcpre1  13094  pcidlem  13125  dvdsprmpweqle  13139  pcadd  13142  pcmpt  13145  pcmpt2  13146  pcfaclem  13151  pcfac  13152  qexpz  13154  pockthlem  13158  pockthg  13159  1arith  13169  4sqlem5  13184  4sqlem6  13185  4sqlem10  13189  mul4sqlem  13195  4sqlem11  13203  4sqlem12  13204  4sqlem13m  13205  4sqlem14  13206  4sqlem15  13207  4sqlem16  13208  4sqlem17  13209  2expltfac  13242  ballotfilemonn  13273  ballotfilemimin  13301  znnen  13341  exmidunben  13369  nninfdclemp1  13393  nninfdclemlt  13394  nninfdclemf1  13395  strleund  13510  strext  13512  psrbaglesuppg  15141  logfac  16090  logbgcd1irraplemexp  16165  logbgcd1irraplemap  16166  zprmlogbaplem1  16176  zprmlogbaplem2  16177  log2tlbndlog2  16181  birthdaylem3  16188  pellexlem2  16191  wilthlem1  16193  chtqge0  16208  chtqwordi  16224  ppiqltx  16242  chtublem  16256  mersenne  16258  perfectlem2  16261  prmefexple  16269  bposlem1  16272  bposlem2  16273  bposlem3  16274  bposlem4  16275  bposlem5  16276  bposlem6  16277  bposlem7  16278  bposlem9  16280  lgslem1  16285  lgsval2lem  16295  lgsdirprm  16319  lgsdir  16320  gausslemma2dlem0h  16341  gausslemma2dlem1a  16343  gausslemma2dlem2  16347  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem3  16357  lgseisen  16359  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  2sqlem3  16402  2sqlem8  16408  cvgcmp2nlemabs  17247