Theorem nn0red 9625

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 9571	. 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 8178   NN0cn0 9567

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 8270  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276  ax-rnegex 8288

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 9307  df-n0 9568

This theorem is used by:  nn0cnd  9626  nn0readdcl  9630  eluzmn  9937  nn01to3  10026  xnn0dcle  10214  flqmulnn0  10747  modifeq2int  10836  modaddmodup  10837  modaddmodlo  10838  modsumfzodifsn  10846  expnegap0  10997  nn0leexp2  11162  nn0le2msqd  11171  nn0opthlem2d  11173  nn0opthd  11174  faclbnd6  11196  bcval5  11215  filtinf  11244  sshashneg  11295  hashf1  11301  zfz1isolemiso  11305  wrdlenge2n0  11354  ccatsymb  11384  ccatrn  11391  ccatalpha  11395  ccat2s1fvwd  11429  swrdspsleq  11453  pfxsuffeqwrdeq  11484  swrdccat3blem  11525  mertenslemi1  12318  efcllemp  12441  eftlub  12473  oddge22np1  12664  nn0oddm1d2  12692  bitsfzolem  12737  bitsfzo  12738  bitsmod  12739  gcdaddm  12777  bezoutlemsup  12802  gcdzeq  12815  dvdssqlem  12823  nninfctlemfo  12833  nn0seqcvgd  12835  lcmneg  12868  mulgcddvds  12888  qredeu  12891  pwbdvdseulemle  12962  pwbdvdseu  12963  nn0sqrtelqelz  13002  nonsq  13003  pythagtriplem3  13066  pythagtriplem6  13069  pythagtriplem7  13070  pclemub  13086  pcprendvds  13089  pcpremul  13092  pcidlem  13122  pcgcd1  13127  pc2dvds  13129  pcz  13131  pcprmpw2  13132  fldivp1  13147  pcfaclem  13148  pcfac  13149  pcbc  13150  4sqexercise1  13197  4sqexercise2  13198  4sqlemsdc  13199  4sqlem11  13200  4sqlem12  13201  4sqlem14  13203  ennnfoneleminc  13351  ennnfonelemkh  13352  ennnfonelemex  13354  ennnfonelemim  13364  psrbaglesuppg  15106  psrbagcon  15111  mplsubgfilemcl  15139  plyaddlem1  15897  log2tlbndlog2  16139  birthdaylem2  16145  birthdaylem3  16146  ppiqp1le  16173  ppiqltx  16183  sgmppw  16187  ppiqub  16194  bcmono  16202  bcmax  16203  bcp1ctr  16204  bclbnd  16205  bposlem5  16213  gausslemma2dlem0h  16273  gausslemma2dlem4  16281  gausslemma2dlem6  16284  lgseisenlem1  16287  2lgsoddprmlem2  16323  2sqlem7  16338  2sqlem8  16340  vtxdgfifival  16630  vtxdgfif  16632  vtxd0nedgbfi  16638  eupth2lemsfi  16817