Theorem nn0red 9455

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

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8030   NN0cn0 9401

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8122  ax-resscn 8123  ax-1re 8125  ax-addrcl 8128  ax-rnegex 8140

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-int 3929  df-inn 9143  df-n0 9402

This theorem is referenced by:  nn0cnd  9456  nn0readdcl  9460  eluzmn  9761  nn01to3  9850  xnn0dcle  10036  flqmulnn0  10558  modifeq2int  10647  modaddmodup  10648  modaddmodlo  10649  modsumfzodifsn  10657  expnegap0  10808  nn0leexp2  10971  nn0le2msqd  10980  nn0opthlem2d  10982  nn0opthd  10983  faclbnd6  11005  bcval5  11024  filtinf  11052  zfz1isolemiso  11102  wrdlenge2n0  11148  ccatsymb  11178  ccatrn  11185  ccatalpha  11189  ccat2s1fvwd  11223  swrdspsleq  11247  pfxsuffeqwrdeq  11278  swrdccat3blem  11319  mertenslemi1  12095  efcllemp  12218  eftlub  12250  oddge22np1  12441  nn0oddm1d2  12469  bitsfzolem  12514  bitsfzo  12515  bitsmod  12516  gcdaddm  12554  bezoutlemsup  12579  gcdzeq  12592  dvdssqlem  12600  nninfctlemfo  12610  nn0seqcvgd  12612  lcmneg  12645  mulgcddvds  12665  qredeu  12668  pw2dvdseulemle  12738  pw2dvdseu  12739  nn0sqrtelqelz  12777  nonsq  12778  pythagtriplem3  12839  pythagtriplem6  12842  pythagtriplem7  12843  pclemub  12859  pcprendvds  12862  pcpremul  12865  pcidlem  12895  pcgcd1  12900  pc2dvds  12902  pcz  12904  pcprmpw2  12905  fldivp1  12920  pcfaclem  12921  pcfac  12922  pcbc  12923  4sqexercise1  12970  4sqexercise2  12971  4sqlemsdc  12972  4sqlem11  12973  4sqlem12  12974  4sqlem14  12976  ennnfoneleminc  13031  ennnfonelemkh  13032  ennnfonelemex  13034  ennnfonelemim  13044  psrbaglesuppg  14685  mplsubgfilemcl  14712  plyaddlem1  15470  sgmppw  15715  gausslemma2dlem0h  15784  gausslemma2dlem4  15792  gausslemma2dlem6  15795  lgseisenlem1  15798  2lgsoddprmlem2  15834  2sqlem7  15849  2sqlem8  15851  vtxdgfifival  16141  vtxdgfif  16143  vtxd0nedgbfi  16149