Theorem nnred 9146

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

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 8021   NNcn 9133

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4205  ax-cnex 8113  ax-resscn 8114  ax-1re 8116  ax-addrcl 8119

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2802  df-in 3204  df-ss 3211  df-int 3927  df-inn 9134

This theorem is referenced by:  exbtwnzlemstep  10497  qbtwnrelemcalc  10505  qbtwnre  10506  flqdiv  10573  modqmulnn  10594  modifeq2int  10638  modaddmodup  10639  modaddmodlo  10640  modsumfzodifsn  10648  addmodlteq  10650  bernneq3  10914  expnbnd  10915  facwordi  10992  faclbnd  10993  faclbnd2  10994  faclbnd3  10995  faclbnd6  10996  facubnd  10997  facavg  10998  bcp1nk  11014  bcval5  11015  caucvgrelemcau  11531  caucvgre  11532  cvg1nlemcxze  11533  cvg1nlemcau  11535  cvg1nlemres  11536  resqrexlemdecn  11563  resqrexlemga  11574  fsum3cvg3  11947  divcnv  12048  cvgratnnlembern  12074  cvgratnnlemseq  12077  cvgratnnlemabsle  12078  cvgratnnlemsumlt  12079  cvgratnnlemrate  12081  cvgratz  12083  eftabs  12207  efcllemp  12209  ege2le3  12222  efcj  12224  eftlub  12241  eflegeo  12252  eirraplem  12328  dvdslelemd  12394  nno  12457  nnoddm1d2  12461  divalglemnqt  12471  divalglemeunn  12472  bitsfzolem  12505  bitsfzo  12506  bitsinv1lem  12512  dvdsbnd  12517  sqgcd  12590  uzwodc  12598  lcmgcdlem  12639  ncoprmgcdne1b  12651  prmind2  12682  isprm5lem  12703  coprm  12706  prmfac1  12714  sqrt2irraplemnn  12741  divdenle  12759  qnumgt0  12760  nn0sqrtelqelz  12768  hashdvds  12783  eulerthlemrprm  12791  eulerthlema  12792  odzdvds  12808  pythagtriplem11  12837  pythagtriplem12  12838  pythagtriplem13  12839  pythagtriplem14  12840  pythagtriplem19  12845  pclemub  12850  pcpre1  12855  pcidlem  12886  dvdsprmpweqle  12900  pcadd  12903  pcmpt  12906  pcmpt2  12907  pcfaclem  12912  pcfac  12913  qexpz  12915  pockthlem  12919  pockthg  12920  1arith  12930  4sqlem5  12945  4sqlem6  12946  4sqlem10  12950  mul4sqlem  12956  4sqlem11  12964  4sqlem12  12965  4sqlem13m  12966  4sqlem14  12967  4sqlem15  12968  4sqlem16  12969  4sqlem17  12970  2expltfac  13002  znnen  13009  exmidunben  13037  nninfdclemp1  13061  nninfdclemlt  13062  nninfdclemf1  13063  strleund  13176  strext  13178  psrbaglesuppg  14676  logbgcd1irraplemexp  15682  logbgcd1irraplemap  15683  wilthlem1  15694  mersenne  15711  perfectlem2  15714  lgslem1  15719  lgsval2lem  15729  lgsdirprm  15753  lgsdir  15754  gausslemma2dlem0h  15775  gausslemma2dlem1a  15777  gausslemma2dlem2  15781  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisen  15793  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  2sqlem3  15836  2sqlem8  15842  cvgcmp2nlemabs  16572