Theorem nn0red 9446

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

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 8021   NN0cn0 9392

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4205  ax-cnex 8113  ax-resscn 8114  ax-1re 8116  ax-addrcl 8119  ax-rnegex 8131

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-sn 3673  df-int 3927  df-inn 9134  df-n0 9393

This theorem is referenced by:  nn0cnd  9447  nn0readdcl  9451  eluzmn  9752  nn01to3  9841  xnn0dcle  10027  flqmulnn0  10549  modifeq2int  10638  modaddmodup  10639  modaddmodlo  10640  modsumfzodifsn  10648  expnegap0  10799  nn0leexp2  10962  nn0le2msqd  10971  nn0opthlem2d  10973  nn0opthd  10974  faclbnd6  10996  bcval5  11015  filtinf  11043  zfz1isolemiso  11093  wrdlenge2n0  11139  ccatsymb  11169  ccatrn  11176  ccatalpha  11180  ccat2s1fvwd  11214  swrdspsleq  11238  pfxsuffeqwrdeq  11269  swrdccat3blem  11310  mertenslemi1  12086  efcllemp  12209  eftlub  12241  oddge22np1  12432  nn0oddm1d2  12460  bitsfzolem  12505  bitsfzo  12506  bitsmod  12507  gcdaddm  12545  bezoutlemsup  12570  gcdzeq  12583  dvdssqlem  12591  nninfctlemfo  12601  nn0seqcvgd  12603  lcmneg  12636  mulgcddvds  12656  qredeu  12659  pw2dvdseulemle  12729  pw2dvdseu  12730  nn0sqrtelqelz  12768  nonsq  12769  pythagtriplem3  12830  pythagtriplem6  12833  pythagtriplem7  12834  pclemub  12850  pcprendvds  12853  pcpremul  12856  pcidlem  12886  pcgcd1  12891  pc2dvds  12893  pcz  12895  pcprmpw2  12896  fldivp1  12911  pcfaclem  12912  pcfac  12913  pcbc  12914  4sqexercise1  12961  4sqexercise2  12962  4sqlemsdc  12963  4sqlem11  12964  4sqlem12  12965  4sqlem14  12967  ennnfoneleminc  13022  ennnfonelemkh  13023  ennnfonelemex  13025  ennnfonelemim  13035  psrbaglesuppg  14676  mplsubgfilemcl  14703  plyaddlem1  15461  sgmppw  15706  gausslemma2dlem0h  15775  gausslemma2dlem4  15783  gausslemma2dlem6  15786  lgseisenlem1  15789  2lgsoddprmlem2  15825  2sqlem7  15840  2sqlem8  15842  vtxdgfifival  16097  vtxdgfif  16099  vtxd0nedgbfi  16105