Theorem nn0red 9351

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

Syntax hints:   -> wi 4   e. wcel 2176   RRcr 7926   NN0cn0 9297

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-sep 4163  ax-cnex 8018  ax-resscn 8019  ax-1re 8021  ax-addrcl 8024  ax-rnegex 8036

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-sn 3639  df-int 3886  df-inn 9039  df-n0 9298

This theorem is referenced by:  nn0cnd  9352  nn0readdcl  9356  nn01to3  9740  xnn0dcle  9926  flqmulnn0  10444  modifeq2int  10533  modaddmodup  10534  modaddmodlo  10535  modsumfzodifsn  10543  expnegap0  10694  nn0leexp2  10857  nn0le2msqd  10866  nn0opthlem2d  10868  nn0opthd  10869  faclbnd6  10891  bcval5  10910  filtinf  10938  zfz1isolemiso  10986  wrdlenge2n0  11031  ccatsymb  11061  ccatrn  11068  swrdspsleq  11123  pfxsuffeqwrdeq  11152  mertenslemi1  11879  efcllemp  12002  eftlub  12034  oddge22np1  12225  nn0oddm1d2  12253  bitsfzolem  12298  bitsfzo  12299  bitsmod  12300  gcdaddm  12338  bezoutlemsup  12363  gcdzeq  12376  dvdssqlem  12384  nninfctlemfo  12394  nn0seqcvgd  12396  lcmneg  12429  mulgcddvds  12449  qredeu  12452  pw2dvdseulemle  12522  pw2dvdseu  12523  nn0sqrtelqelz  12561  nonsq  12562  pythagtriplem3  12623  pythagtriplem6  12626  pythagtriplem7  12627  pclemub  12643  pcprendvds  12646  pcpremul  12649  pcidlem  12679  pcgcd1  12684  pc2dvds  12686  pcz  12688  pcprmpw2  12689  fldivp1  12704  pcfaclem  12705  pcfac  12706  pcbc  12707  4sqexercise1  12754  4sqexercise2  12755  4sqlemsdc  12756  4sqlem11  12757  4sqlem12  12758  4sqlem14  12760  ennnfoneleminc  12815  ennnfonelemkh  12816  ennnfonelemex  12818  ennnfonelemim  12828  psrbaglesuppg  14467  mplsubgfilemcl  14494  plyaddlem1  15252  sgmppw  15497  gausslemma2dlem0h  15566  gausslemma2dlem4  15574  gausslemma2dlem6  15577  lgseisenlem1  15580  2lgsoddprmlem2  15616  2sqlem7  15631  2sqlem8  15633