Theorem nn0red 9626

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   RRcr 8179   NN0cn0 9568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4249  ax-cnex 8271  ax-resscn 8272  ax-1re 8274  ax-addrcl 8277  ax-rnegex 8289

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-int 3971  df-inn 9308  df-n0 9569

This theorem is used by:  nn0cnd  9627  nn0readdcl  9631  eluzmn  9938  nn01to3  10027  xnn0dcle  10215  flqmulnn0  10749  modifeq2int  10838  modaddmodup  10839  modaddmodlo  10840  modsumfzodifsn  10848  expnegap0  10999  nn0leexp2  11164  nn0le2msqd  11173  nn0opthlem2d  11175  nn0opthd  11176  faclbnd6  11198  bcval5  11217  filtinf  11246  sshashneg  11297  hashf1  11303  zfz1isolemiso  11307  wrdlenge2n0  11356  ccatsymb  11386  ccatrn  11393  ccatalpha  11397  ccat2s1fvwd  11431  swrdspsleq  11455  pfxsuffeqwrdeq  11486  swrdccat3blem  11527  mertenslemi1  12321  efcllemp  12444  eftlub  12476  oddge22np1  12667  nn0oddm1d2  12695  bitsfzolem  12740  bitsfzo  12741  bitsmod  12742  gcdaddm  12780  bezoutlemsup  12805  gcdzeq  12818  dvdssqlem  12826  nninfctlemfo  12836  nn0seqcvgd  12838  lcmneg  12871  mulgcddvds  12891  qredeu  12894  pwbdvdseulemle  12965  pwbdvdseu  12966  nn0sqrtelqelz  13005  nonsq  13006  pythagtriplem3  13069  pythagtriplem6  13072  pythagtriplem7  13073  pclemub  13089  pcprendvds  13092  pcpremul  13095  pcidlem  13125  pcgcd1  13130  pc2dvds  13132  pcz  13134  pcprmpw2  13135  fldivp1  13150  pcfaclem  13151  pcfac  13152  pcbc  13153  4sqexercise1  13200  4sqexercise2  13201  4sqlemsdc  13202  4sqlem11  13203  4sqlem12  13204  4sqlem14  13206  ennnfoneleminc  13354  ennnfonelemkh  13355  ennnfonelemex  13357  ennnfonelemim  13367  psrbaglesuppg  15141  psrbagcon  15146  psrbaglefifi  15147  mplsubgfilemcl  15181  plyaddlem1  15939  log2tlbndlog2  16181  birthdaylem2  16187  birthdaylem3  16188  ppiqp1le  16228  ppiqltx  16242  sgmppw  16247  ppiqub  16254  chtublem  16256  bcmono  16265  bcmax  16266  bcp1ctr  16267  bclbnd  16268  bposlem5  16276  gausslemma2dlem0h  16341  gausslemma2dlem4  16349  gausslemma2dlem6  16352  lgseisenlem1  16355  2lgsoddprmlem2  16391  2sqlem7  16406  2sqlem8  16408  vtxdgfifival  16698  vtxdgfif  16700  vtxd0nedgbfi  16706  eupth2lemsfi  16885