Theorem nn0red 9554

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 9500	. 2 |- NN0 C_ RR
2		nn0red.1	. 2 |- ( ph -> A e. NN0 )
3	1, 2	sselid 3236	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2203   RRcr 8126   NN0cn0 9496

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-sep 4228  ax-cnex 8218  ax-resscn 8219  ax-1re 8221  ax-addrcl 8224  ax-rnegex 8236

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-sn 3695  df-int 3950  df-inn 9238  df-n0 9497

This theorem is referenced by:  nn0cnd  9555  nn0readdcl  9559  eluzmn  9860  nn01to3  9949  xnn0dcle  10135  flqmulnn0  10659  modifeq2int  10748  modaddmodup  10749  modaddmodlo  10750  modsumfzodifsn  10758  expnegap0  10909  nn0leexp2  11072  nn0le2msqd  11081  nn0opthlem2d  11083  nn0opthd  11084  faclbnd6  11106  bcval5  11125  filtinf  11154  sshashneg  11205  zfz1isolemiso  11211  wrdlenge2n0  11260  ccatsymb  11290  ccatrn  11297  ccatalpha  11301  ccat2s1fvwd  11335  swrdspsleq  11359  pfxsuffeqwrdeq  11390  swrdccat3blem  11431  mertenslemi1  12221  efcllemp  12344  eftlub  12376  oddge22np1  12567  nn0oddm1d2  12595  bitsfzolem  12640  bitsfzo  12641  bitsmod  12642  gcdaddm  12680  bezoutlemsup  12705  gcdzeq  12718  dvdssqlem  12726  nninfctlemfo  12736  nn0seqcvgd  12738  lcmneg  12771  mulgcddvds  12791  qredeu  12794  pw2dvdseulemle  12864  pw2dvdseu  12865  nn0sqrtelqelz  12903  nonsq  12904  pythagtriplem3  12965  pythagtriplem6  12968  pythagtriplem7  12969  pclemub  12985  pcprendvds  12988  pcpremul  12991  pcidlem  13021  pcgcd1  13026  pc2dvds  13028  pcz  13030  pcprmpw2  13031  fldivp1  13046  pcfaclem  13047  pcfac  13048  pcbc  13049  4sqexercise1  13096  4sqexercise2  13097  4sqlemsdc  13098  4sqlem11  13099  4sqlem12  13100  4sqlem14  13102  ennnfoneleminc  13162  ennnfonelemkh  13163  ennnfonelemex  13165  ennnfonelemim  13175  psrbaglesuppg  14821  psrbagcon  14826  mplsubgfilemcl  14854  plyaddlem1  15612  sgmppw  15860  gausslemma2dlem0h  15929  gausslemma2dlem4  15937  gausslemma2dlem6  15940  lgseisenlem1  15943  2lgsoddprmlem2  15979  2sqlem7  15994  2sqlem8  15996  vtxdgfifival  16286  vtxdgfif  16288  vtxd0nedgbfi  16294  eupth2lemsfi  16473