Theorem nnred 8733

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 8724	. 2 |- NN C_ RR
2		nnred.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sseldi 3095	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1480   RRcr 7619   NNcn 8720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-cnex 7711  ax-resscn 7712  ax-1re 7714  ax-addrcl 7717

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-v 2688  df-in 3077  df-ss 3084  df-int 3772  df-inn 8721

This theorem is referenced by:  exbtwnzlemstep  10025  qbtwnrelemcalc  10033  qbtwnre  10034  flqdiv  10094  modqmulnn  10115  modifeq2int  10159  modaddmodup  10160  modaddmodlo  10161  modsumfzodifsn  10169  addmodlteq  10171  bernneq3  10414  expnbnd  10415  facwordi  10486  faclbnd  10487  faclbnd2  10488  faclbnd3  10489  faclbnd6  10490  facubnd  10491  facavg  10492  bcp1nk  10508  bcval5  10509  caucvgrelemcau  10752  caucvgre  10753  cvg1nlemcxze  10754  cvg1nlemcau  10756  cvg1nlemres  10757  resqrexlemdecn  10784  resqrexlemga  10795  fsum3cvg3  11165  divcnv  11266  cvgratnnlembern  11292  cvgratnnlemseq  11295  cvgratnnlemabsle  11296  cvgratnnlemsumlt  11297  cvgratnnlemrate  11299  cvgratz  11301  eftabs  11362  efcllemp  11364  ege2le3  11377  efcj  11379  eftlub  11396  eflegeo  11408  eirraplem  11483  dvdslelemd  11541  nno  11603  nnoddm1d2  11607  divalglemnqt  11617  divalglemeunn  11618  dvdsbnd  11645  sqgcd  11717  lcmgcdlem  11758  ncoprmgcdne1b  11770  prmind2  11801  coprm  11822  prmfac1  11830  sqrt2irraplemnn  11857  divdenle  11875  qnumgt0  11876  nn0sqrtelqelz  11884  hashdvds  11897  znnen  11911  exmidunben  11939  strleund  12047  cvgcmp2nlemabs  13227