Theorem nn0red 9621

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 9567	. 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 9563

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 9305  df-n0 9564

This theorem is used by:  nn0cnd  9622  nn0readdcl  9626  eluzmn  9928  nn01to3  10017  xnn0dcle  10204  flqmulnn0  10734  modifeq2int  10823  modaddmodup  10824  modaddmodlo  10825  modsumfzodifsn  10833  expnegap0  10984  nn0leexp2  11148  nn0le2msqd  11157  nn0opthlem2d  11159  nn0opthd  11160  faclbnd6  11182  bcval5  11201  filtinf  11230  sshashneg  11281  hashf1  11287  zfz1isolemiso  11291  wrdlenge2n0  11340  ccatsymb  11370  ccatrn  11377  ccatalpha  11381  ccat2s1fvwd  11415  swrdspsleq  11439  pfxsuffeqwrdeq  11470  swrdccat3blem  11511  mertenslemi1  12302  efcllemp  12425  eftlub  12457  oddge22np1  12648  nn0oddm1d2  12676  bitsfzolem  12721  bitsfzo  12722  bitsmod  12723  gcdaddm  12761  bezoutlemsup  12786  gcdzeq  12799  dvdssqlem  12807  nninfctlemfo  12817  nn0seqcvgd  12819  lcmneg  12852  mulgcddvds  12872  qredeu  12875  pw2dvdseulemle  12945  pw2dvdseu  12946  nn0sqrtelqelz  12984  nonsq  12985  pythagtriplem3  13046  pythagtriplem6  13049  pythagtriplem7  13050  pclemub  13066  pcprendvds  13069  pcpremul  13072  pcidlem  13102  pcgcd1  13107  pc2dvds  13109  pcz  13111  pcprmpw2  13112  fldivp1  13127  pcfaclem  13128  pcfac  13129  pcbc  13130  4sqexercise1  13177  4sqexercise2  13178  4sqlemsdc  13179  4sqlem11  13180  4sqlem12  13181  4sqlem14  13183  ennnfoneleminc  13302  ennnfonelemkh  13303  ennnfonelemex  13305  ennnfonelemim  13315  psrbaglesuppg  15057  psrbagcon  15062  mplsubgfilemcl  15090  plyaddlem1  15848  log2tlbndlog2  16082  birthdaylem2  16088  birthdaylem3  16089  sgmppw  16106  gausslemma2dlem0h  16175  gausslemma2dlem4  16183  gausslemma2dlem6  16186  lgseisenlem1  16189  2lgsoddprmlem2  16225  2sqlem7  16240  2sqlem8  16242  vtxdgfifival  16532  vtxdgfif  16534  vtxd0nedgbfi  16540  eupth2lemsfi  16719