Theorem nnred 9084

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

Syntax hints:   -> wi 4   e. wcel 2178   RRcr 7959   NNcn 9071

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-sep 4178  ax-cnex 8051  ax-resscn 8052  ax-1re 8054  ax-addrcl 8057

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-v 2778  df-in 3180  df-ss 3187  df-int 3900  df-inn 9072

This theorem is referenced by:  exbtwnzlemstep  10427  qbtwnrelemcalc  10435  qbtwnre  10436  flqdiv  10503  modqmulnn  10524  modifeq2int  10568  modaddmodup  10569  modaddmodlo  10570  modsumfzodifsn  10578  addmodlteq  10580  bernneq3  10844  expnbnd  10845  facwordi  10922  faclbnd  10923  faclbnd2  10924  faclbnd3  10925  faclbnd6  10926  facubnd  10927  facavg  10928  bcp1nk  10944  bcval5  10945  caucvgrelemcau  11406  caucvgre  11407  cvg1nlemcxze  11408  cvg1nlemcau  11410  cvg1nlemres  11411  resqrexlemdecn  11438  resqrexlemga  11449  fsum3cvg3  11822  divcnv  11923  cvgratnnlembern  11949  cvgratnnlemseq  11952  cvgratnnlemabsle  11953  cvgratnnlemsumlt  11954  cvgratnnlemrate  11956  cvgratz  11958  eftabs  12082  efcllemp  12084  ege2le3  12097  efcj  12099  eftlub  12116  eflegeo  12127  eirraplem  12203  dvdslelemd  12269  nno  12332  nnoddm1d2  12336  divalglemnqt  12346  divalglemeunn  12347  bitsfzolem  12380  bitsfzo  12381  bitsinv1lem  12387  dvdsbnd  12392  sqgcd  12465  uzwodc  12473  lcmgcdlem  12514  ncoprmgcdne1b  12526  prmind2  12557  isprm5lem  12578  coprm  12581  prmfac1  12589  sqrt2irraplemnn  12616  divdenle  12634  qnumgt0  12635  nn0sqrtelqelz  12643  hashdvds  12658  eulerthlemrprm  12666  eulerthlema  12667  odzdvds  12683  pythagtriplem11  12712  pythagtriplem12  12713  pythagtriplem13  12714  pythagtriplem14  12715  pythagtriplem19  12720  pclemub  12725  pcpre1  12730  pcidlem  12761  dvdsprmpweqle  12775  pcadd  12778  pcmpt  12781  pcmpt2  12782  pcfaclem  12787  pcfac  12788  qexpz  12790  pockthlem  12794  pockthg  12795  1arith  12805  4sqlem5  12820  4sqlem6  12821  4sqlem10  12825  mul4sqlem  12831  4sqlem11  12839  4sqlem12  12840  4sqlem13m  12841  4sqlem14  12842  4sqlem15  12843  4sqlem16  12844  4sqlem17  12845  2expltfac  12877  znnen  12884  exmidunben  12912  nninfdclemp1  12936  nninfdclemlt  12937  nninfdclemf1  12938  strleund  13050  strext  13052  psrbaglesuppg  14549  logbgcd1irraplemexp  15555  logbgcd1irraplemap  15556  wilthlem1  15567  mersenne  15584  perfectlem2  15587  lgslem1  15592  lgsval2lem  15602  lgsdirprm  15626  lgsdir  15627  gausslemma2dlem0h  15648  gausslemma2dlem1a  15650  gausslemma2dlem2  15654  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem3  15664  lgseisen  15666  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671  2sqlem3  15709  2sqlem8  15715  cvgcmp2nlemabs  16173