Theorem nnred 9123

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

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 7998   NNcn 9110

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 4202  ax-cnex 8090  ax-resscn 8091  ax-1re 8093  ax-addrcl 8096

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 2801  df-in 3203  df-ss 3210  df-int 3924  df-inn 9111

This theorem is referenced by:  exbtwnzlemstep  10467  qbtwnrelemcalc  10475  qbtwnre  10476  flqdiv  10543  modqmulnn  10564  modifeq2int  10608  modaddmodup  10609  modaddmodlo  10610  modsumfzodifsn  10618  addmodlteq  10620  bernneq3  10884  expnbnd  10885  facwordi  10962  faclbnd  10963  faclbnd2  10964  faclbnd3  10965  faclbnd6  10966  facubnd  10967  facavg  10968  bcp1nk  10984  bcval5  10985  caucvgrelemcau  11491  caucvgre  11492  cvg1nlemcxze  11493  cvg1nlemcau  11495  cvg1nlemres  11496  resqrexlemdecn  11523  resqrexlemga  11534  fsum3cvg3  11907  divcnv  12008  cvgratnnlembern  12034  cvgratnnlemseq  12037  cvgratnnlemabsle  12038  cvgratnnlemsumlt  12039  cvgratnnlemrate  12041  cvgratz  12043  eftabs  12167  efcllemp  12169  ege2le3  12182  efcj  12184  eftlub  12201  eflegeo  12212  eirraplem  12288  dvdslelemd  12354  nno  12417  nnoddm1d2  12421  divalglemnqt  12431  divalglemeunn  12432  bitsfzolem  12465  bitsfzo  12466  bitsinv1lem  12472  dvdsbnd  12477  sqgcd  12550  uzwodc  12558  lcmgcdlem  12599  ncoprmgcdne1b  12611  prmind2  12642  isprm5lem  12663  coprm  12666  prmfac1  12674  sqrt2irraplemnn  12701  divdenle  12719  qnumgt0  12720  nn0sqrtelqelz  12728  hashdvds  12743  eulerthlemrprm  12751  eulerthlema  12752  odzdvds  12768  pythagtriplem11  12797  pythagtriplem12  12798  pythagtriplem13  12799  pythagtriplem14  12800  pythagtriplem19  12805  pclemub  12810  pcpre1  12815  pcidlem  12846  dvdsprmpweqle  12860  pcadd  12863  pcmpt  12866  pcmpt2  12867  pcfaclem  12872  pcfac  12873  qexpz  12875  pockthlem  12879  pockthg  12880  1arith  12890  4sqlem5  12905  4sqlem6  12906  4sqlem10  12910  mul4sqlem  12916  4sqlem11  12924  4sqlem12  12925  4sqlem13m  12926  4sqlem14  12927  4sqlem15  12928  4sqlem16  12929  4sqlem17  12930  2expltfac  12962  znnen  12969  exmidunben  12997  nninfdclemp1  13021  nninfdclemlt  13022  nninfdclemf1  13023  strleund  13136  strext  13138  psrbaglesuppg  14636  logbgcd1irraplemexp  15642  logbgcd1irraplemap  15643  wilthlem1  15654  mersenne  15671  perfectlem2  15674  lgslem1  15679  lgsval2lem  15689  lgsdirprm  15713  lgsdir  15714  gausslemma2dlem0h  15735  gausslemma2dlem1a  15737  gausslemma2dlem2  15741  lgseisenlem1  15749  lgseisenlem2  15750  lgseisenlem3  15751  lgseisen  15753  lgsquadlem1  15756  lgsquadlem2  15757  lgsquadlem3  15758  2sqlem3  15796  2sqlem8  15802  cvgcmp2nlemabs  16400