Theorem nn0red 9297

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

Syntax hints:   -> wi 4   e. wcel 2164   RRcr 7873   NN0cn0 9243

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4148  ax-cnex 7965  ax-resscn 7966  ax-1re 7968  ax-addrcl 7971  ax-rnegex 7983

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3158  df-in 3160  df-ss 3167  df-sn 3625  df-int 3872  df-inn 8985  df-n0 9244

This theorem is referenced by:  nn0cnd  9298  nn0readdcl  9302  nn01to3  9685  xnn0dcle  9871  flqmulnn0  10371  modifeq2int  10460  modaddmodup  10461  modaddmodlo  10462  modsumfzodifsn  10470  expnegap0  10621  nn0leexp2  10784  nn0le2msqd  10793  nn0opthlem2d  10795  nn0opthd  10796  faclbnd6  10818  bcval5  10837  filtinf  10865  zfz1isolemiso  10913  wrdlenge2n0  10952  mertenslemi1  11681  efcllemp  11804  eftlub  11836  oddge22np1  12025  nn0oddm1d2  12053  gcdaddm  12124  bezoutlemsup  12149  gcdzeq  12162  dvdssqlem  12170  nninfctlemfo  12180  nn0seqcvgd  12182  lcmneg  12215  mulgcddvds  12235  qredeu  12238  pw2dvdseulemle  12308  pw2dvdseu  12309  nn0sqrtelqelz  12347  nonsq  12348  pythagtriplem3  12408  pythagtriplem6  12411  pythagtriplem7  12412  pclemub  12428  pcprendvds  12431  pcpremul  12434  pcidlem  12464  pcgcd1  12469  pc2dvds  12471  pcz  12473  pcprmpw2  12474  fldivp1  12489  pcfaclem  12490  pcfac  12491  pcbc  12492  4sqexercise1  12539  4sqexercise2  12540  4sqlemsdc  12541  4sqlem11  12542  4sqlem12  12543  4sqlem14  12545  ennnfoneleminc  12571  ennnfonelemkh  12572  ennnfonelemex  12574  ennnfonelemim  12584  psrbaglesuppg  14169  plyaddlem1  14926  gausslemma2dlem0h  15213  gausslemma2dlem4  15221  gausslemma2dlem6  15224  lgseisenlem1  15227  2lgsoddprmlem2  15263  2sqlem7  15278  2sqlem8  15280