Theorem nnred 8108

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

Syntax hints:   -> wi 4   e. wcel 1434   RRcr 7031   NNcn 8095

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-sep 3898  ax-cnex 7118  ax-resscn 7119  ax-1re 7121  ax-addrcl 7124

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ral 2354  df-v 2604  df-in 2980  df-ss 2987  df-int 3639  df-inn 8096

This theorem is referenced by:  exbtwnzlemstep  9323  qbtwnrelemcalc  9331  qbtwnre  9332  flqdiv  9392  modqmulnn  9413  modifeq2int  9457  modaddmodup  9458  modaddmodlo  9459  modsumfzodifsn  9467  addmodlteq  9469  bernneq3  9681  expnbnd  9682  facwordi  9753  faclbnd  9754  faclbnd2  9755  faclbnd3  9756  faclbnd6  9757  facubnd  9758  facavg  9759  bcp1nk  9775  ibcval5  9776  caucvgrelemcau  9993  caucvgre  9994  cvg1nlemcxze  9995  cvg1nlemcau  9997  cvg1nlemres  9998  resqrexlemdecn  10025  resqrexlemga  10036  dvdslelemd  10377  nno  10439  nnoddm1d2  10443  divalglemnqt  10453  divalglemeunn  10454  dvdsbnd  10481  sqgcd  10551  lcmgcdlem  10592  ncoprmgcdne1b  10604  prmind2  10635  coprm  10656  prmfac1  10664  sqrt2irraplemnn  10690