Theorem nnred 9003

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

Syntax hints:   -> wi 4   e. wcel 2167   RRcr 7878   NNcn 8990

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4151  ax-cnex 7970  ax-resscn 7971  ax-1re 7973  ax-addrcl 7976

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765  df-in 3163  df-ss 3170  df-int 3875  df-inn 8991

This theorem is referenced by:  exbtwnzlemstep  10337  qbtwnrelemcalc  10345  qbtwnre  10346  flqdiv  10413  modqmulnn  10434  modifeq2int  10478  modaddmodup  10479  modaddmodlo  10480  modsumfzodifsn  10488  addmodlteq  10490  bernneq3  10754  expnbnd  10755  facwordi  10832  faclbnd  10833  faclbnd2  10834  faclbnd3  10835  faclbnd6  10836  facubnd  10837  facavg  10838  bcp1nk  10854  bcval5  10855  caucvgrelemcau  11145  caucvgre  11146  cvg1nlemcxze  11147  cvg1nlemcau  11149  cvg1nlemres  11150  resqrexlemdecn  11177  resqrexlemga  11188  fsum3cvg3  11561  divcnv  11662  cvgratnnlembern  11688  cvgratnnlemseq  11691  cvgratnnlemabsle  11692  cvgratnnlemsumlt  11693  cvgratnnlemrate  11695  cvgratz  11697  eftabs  11821  efcllemp  11823  ege2le3  11836  efcj  11838  eftlub  11855  eflegeo  11866  eirraplem  11942  dvdslelemd  12008  nno  12071  nnoddm1d2  12075  divalglemnqt  12085  divalglemeunn  12086  bitsfzolem  12118  bitsfzo  12119  dvdsbnd  12123  sqgcd  12196  uzwodc  12204  lcmgcdlem  12245  ncoprmgcdne1b  12257  prmind2  12288  isprm5lem  12309  coprm  12312  prmfac1  12320  sqrt2irraplemnn  12347  divdenle  12365  qnumgt0  12366  nn0sqrtelqelz  12374  hashdvds  12389  eulerthlemrprm  12397  eulerthlema  12398  odzdvds  12414  pythagtriplem11  12443  pythagtriplem12  12444  pythagtriplem13  12445  pythagtriplem14  12446  pythagtriplem19  12451  pclemub  12456  pcpre1  12461  pcidlem  12492  dvdsprmpweqle  12506  pcadd  12509  pcmpt  12512  pcmpt2  12513  pcfaclem  12518  pcfac  12519  qexpz  12521  pockthlem  12525  pockthg  12526  1arith  12536  4sqlem5  12551  4sqlem6  12552  4sqlem10  12556  mul4sqlem  12562  4sqlem11  12570  4sqlem12  12571  4sqlem13m  12572  4sqlem14  12573  4sqlem15  12574  4sqlem16  12575  4sqlem17  12576  2expltfac  12608  znnen  12615  exmidunben  12643  nninfdclemp1  12667  nninfdclemlt  12668  nninfdclemf1  12669  strleund  12781  strext  12783  psrbaglesuppg  14226  logbgcd1irraplemexp  15204  logbgcd1irraplemap  15205  wilthlem1  15216  mersenne  15233  perfectlem2  15236  lgslem1  15241  lgsval2lem  15251  lgsdirprm  15275  lgsdir  15276  gausslemma2dlem0h  15297  gausslemma2dlem1a  15299  gausslemma2dlem2  15303  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisen  15315  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  2sqlem3  15358  2sqlem8  15364  cvgcmp2nlemabs  15676