Theorem nn0red 9456

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 9406	. 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 8031   NN0cn0 9402

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 8123  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129  ax-rnegex 8141

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 9144  df-n0 9403

This theorem is referenced by:  nn0cnd  9457  nn0readdcl  9461  eluzmn  9762  nn01to3  9851  xnn0dcle  10037  flqmulnn0  10560  modifeq2int  10649  modaddmodup  10650  modaddmodlo  10651  modsumfzodifsn  10659  expnegap0  10810  nn0leexp2  10973  nn0le2msqd  10982  nn0opthlem2d  10984  nn0opthd  10985  faclbnd6  11007  bcval5  11026  filtinf  11054  zfz1isolemiso  11104  wrdlenge2n0  11153  ccatsymb  11183  ccatrn  11190  ccatalpha  11194  ccat2s1fvwd  11228  swrdspsleq  11252  pfxsuffeqwrdeq  11283  swrdccat3blem  11324  mertenslemi1  12114  efcllemp  12237  eftlub  12269  oddge22np1  12460  nn0oddm1d2  12488  bitsfzolem  12533  bitsfzo  12534  bitsmod  12535  gcdaddm  12573  bezoutlemsup  12598  gcdzeq  12611  dvdssqlem  12619  nninfctlemfo  12629  nn0seqcvgd  12631  lcmneg  12664  mulgcddvds  12684  qredeu  12687  pw2dvdseulemle  12757  pw2dvdseu  12758  nn0sqrtelqelz  12796  nonsq  12797  pythagtriplem3  12858  pythagtriplem6  12861  pythagtriplem7  12862  pclemub  12878  pcprendvds  12881  pcpremul  12884  pcidlem  12914  pcgcd1  12919  pc2dvds  12921  pcz  12923  pcprmpw2  12924  fldivp1  12939  pcfaclem  12940  pcfac  12941  pcbc  12942  4sqexercise1  12989  4sqexercise2  12990  4sqlemsdc  12991  4sqlem11  12992  4sqlem12  12993  4sqlem14  12995  ennnfoneleminc  13050  ennnfonelemkh  13051  ennnfonelemex  13053  ennnfonelemim  13063  psrbaglesuppg  14705  mplsubgfilemcl  14732  plyaddlem1  15490  sgmppw  15735  gausslemma2dlem0h  15804  gausslemma2dlem4  15812  gausslemma2dlem6  15815  lgseisenlem1  15818  2lgsoddprmlem2  15854  2sqlem7  15869  2sqlem8  15871  vtxdgfifival  16161  vtxdgfif  16163  vtxd0nedgbfi  16169  eupth2lemsfi  16348