Theorem nnred 9296

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

Syntax hints:   -> wi 4   e. wcel 2209   RRcr 8168   NNcn 9283

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 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 4244  ax-cnex 8260  ax-resscn 8261  ax-1re 8263  ax-addrcl 8266

This theorem 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 3966  df-inn 9284

This theorem is referenced by:  exbtwnzlemstep  10660  qbtwnrelemcalc  10668  qbtwnre  10669  flqdiv  10736  modqmulnn  10757  modifeq2int  10801  modaddmodup  10802  modaddmodlo  10803  modsumfzodifsn  10811  addmodlteq  10813  bernneq3  11078  expnbnd  11079  facwordi  11156  faclbnd  11157  faclbnd2  11158  faclbnd3  11159  faclbnd6  11160  facubnd  11161  facavg  11162  bcp1nk  11178  bcval5  11179  hashf1  11265  caucvgrelemcau  11724  caucvgre  11725  cvg1nlemcxze  11726  cvg1nlemcau  11728  cvg1nlemres  11729  resqrexlemdecn  11756  resqrexlemga  11767  fsum3cvg3  12141  divcnv  12242  cvgratnnlembern  12268  cvgratnnlemseq  12271  cvgratnnlemabsle  12272  cvgratnnlemsumlt  12273  cvgratnnlemrate  12275  cvgratz  12277  eftabs  12401  efcllemp  12403  ege2le3  12416  efcj  12418  eftlub  12435  eflegeo  12446  eirraplem  12522  dvdslelemd  12588  nno  12651  nnoddm1d2  12655  divalglemnqt  12665  divalglemeunn  12666  bitsfzolem  12699  bitsfzo  12700  bitsinv1lem  12706  dvdsbnd  12711  sqgcd  12784  uzwodc  12792  lcmgcdlem  12833  ncoprmgcdne1b  12845  prmind2  12876  isprm5lem  12897  coprm  12900  prmfac1  12908  sqrt2irraplemnn  12935  divdenle  12953  qnumgt0  12954  nn0sqrtelqelz  12962  hashdvds  12977  eulerthlemrprm  12985  eulerthlema  12986  odzdvds  13002  pythagtriplem11  13031  pythagtriplem12  13032  pythagtriplem13  13033  pythagtriplem14  13034  pythagtriplem19  13039  pclemub  13044  pcpre1  13049  pcidlem  13080  dvdsprmpweqle  13094  pcadd  13097  pcmpt  13100  pcmpt2  13101  pcfaclem  13106  pcfac  13107  qexpz  13109  pockthlem  13113  pockthg  13114  1arith  13124  4sqlem5  13139  4sqlem6  13140  4sqlem10  13144  mul4sqlem  13150  4sqlem11  13158  4sqlem12  13159  4sqlem13m  13160  4sqlem14  13161  4sqlem15  13162  4sqlem16  13163  4sqlem17  13164  2expltfac  13196  ballotfilemonn  13199  ballotfilemimin  13227  znnen  13267  exmidunben  13295  nninfdclemp1  13319  nninfdclemlt  13320  nninfdclemf1  13321  strleund  13434  strext  13436  psrbaglesuppg  14980  logfac  15918  logbgcd1irraplemexp  15993  logbgcd1irraplemap  15994  pellexlem2  16006  wilthlem1  16008  mersenne  16025  perfectlem2  16028  lgslem1  16033  lgsval2lem  16043  lgsdirprm  16067  lgsdir  16068  gausslemma2dlem0h  16089  gausslemma2dlem1a  16091  gausslemma2dlem2  16095  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgseisen  16107  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  2sqlem3  16150  2sqlem8  16156  cvgcmp2nlemabs  16986