Theorem nnred 8052

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

Syntax hints:   -> wi 4   e. wcel 1433   RRcr 6980   NNcn 8039

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 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896  ax-cnex 7067  ax-resscn 7068  ax-1re 7070  ax-addrcl 7073

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-v 2603  df-in 2979  df-ss 2986  df-int 3637  df-inn 8040

This theorem is referenced by:  qbtwnzlemstep  9257  qbtwnrelemcalc  9264  qbtwnre  9265  flqdiv  9323  modqmulnn  9344  modifeq2int  9388  modaddmodup  9389  modaddmodlo  9390  modsumfzodifsn  9398  addmodlteq  9400  bernneq3  9595  expnbnd  9596  facwordi  9667  faclbnd  9668  faclbnd2  9669  faclbnd3  9670  faclbnd6  9671  facubnd  9672  facavg  9673  bcp1nk  9689  ibcval5  9690  caucvgrelemcau  9866  caucvgre  9867  cvg1nlemcxze  9868  cvg1nlemcau  9870  cvg1nlemres  9871  resqrexlemdecn  9898  resqrexlemga  9909  dvdslelemd  10243  nno  10306  nnoddm1d2  10310  divalglemnqt  10320  divalglemeunn  10321  dvdsbnd  10348  sqgcd  10418  lcmgcdlem  10459  ncoprmgcdne1b  10471  prmind2  10502  coprm  10523  prmfac1  10531  sqrt2irraplemnn  10557