Theorem nn0red 9456

Description: A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nn0red.1	|- ( ph -> A e. NN0 )

Assertion

Ref	Expression
nn0red	|- ( ph -> A e. RR )

Proof of Theorem nn0red

Step	Hyp	Ref	Expression
1		nn0ssre 9406	. 2 |- NN0 C_ RR
2		nn0red.1	. 2 |- ( ph -> A e. NN0 )
3	1, 2	sselid 3225	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8031   NN0cn0 9402

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8123  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129  ax-rnegex 8141

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-int 3929  df-inn 9144  df-n0 9403

This theorem is referenced by:  nn0cnd  9457  nn0readdcl  9461  eluzmn  9762  nn01to3  9851  xnn0dcle  10037  flqmulnn0  10559  modifeq2int  10648  modaddmodup  10649  modaddmodlo  10650  modsumfzodifsn  10658  expnegap0  10809  nn0leexp2  10972  nn0le2msqd  10981  nn0opthlem2d  10983  nn0opthd  10984  faclbnd6  11006  bcval5  11025  filtinf  11053  zfz1isolemiso  11103  wrdlenge2n0  11149  ccatsymb  11179  ccatrn  11186  ccatalpha  11190  ccat2s1fvwd  11224  swrdspsleq  11248  pfxsuffeqwrdeq  11279  swrdccat3blem  11320  mertenslemi1  12097  efcllemp  12220  eftlub  12252  oddge22np1  12443  nn0oddm1d2  12471  bitsfzolem  12516  bitsfzo  12517  bitsmod  12518  gcdaddm  12556  bezoutlemsup  12581  gcdzeq  12594  dvdssqlem  12602  nninfctlemfo  12612  nn0seqcvgd  12614  lcmneg  12647  mulgcddvds  12667  qredeu  12670  pw2dvdseulemle  12740  pw2dvdseu  12741  nn0sqrtelqelz  12779  nonsq  12780  pythagtriplem3  12841  pythagtriplem6  12844  pythagtriplem7  12845  pclemub  12861  pcprendvds  12864  pcpremul  12867  pcidlem  12897  pcgcd1  12902  pc2dvds  12904  pcz  12906  pcprmpw2  12907  fldivp1  12922  pcfaclem  12923  pcfac  12924  pcbc  12925  4sqexercise1  12972  4sqexercise2  12973  4sqlemsdc  12974  4sqlem11  12975  4sqlem12  12976  4sqlem14  12978  ennnfoneleminc  13033  ennnfonelemkh  13034  ennnfonelemex  13036  ennnfonelemim  13046  psrbaglesuppg  14688  mplsubgfilemcl  14715  plyaddlem1  15473  sgmppw  15718  gausslemma2dlem0h  15787  gausslemma2dlem4  15795  gausslemma2dlem6  15798  lgseisenlem1  15801  2lgsoddprmlem2  15837  2sqlem7  15852  2sqlem8  15854  vtxdgfifival  16144  vtxdgfif  16146  vtxd0nedgbfi  16152