Theorem nn0red 9600

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

Syntax hints:   -> wi 4   e. wcel 2209   RRcr 8168   NN0cn0 9542

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4244  ax-cnex 8260  ax-resscn 8261  ax-1re 8263  ax-addrcl 8266  ax-rnegex 8278

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3711  df-int 3966  df-inn 9284  df-n0 9543

This theorem is referenced by:  nn0cnd  9601  nn0readdcl  9605  eluzmn  9907  nn01to3  9996  xnn0dcle  10183  flqmulnn0  10712  modifeq2int  10801  modaddmodup  10802  modaddmodlo  10803  modsumfzodifsn  10811  expnegap0  10962  nn0leexp2  11126  nn0le2msqd  11135  nn0opthlem2d  11137  nn0opthd  11138  faclbnd6  11160  bcval5  11179  filtinf  11208  sshashneg  11259  hashf1  11265  zfz1isolemiso  11269  wrdlenge2n0  11318  ccatsymb  11348  ccatrn  11355  ccatalpha  11359  ccat2s1fvwd  11393  swrdspsleq  11417  pfxsuffeqwrdeq  11448  swrdccat3blem  11489  mertenslemi1  12280  efcllemp  12403  eftlub  12435  oddge22np1  12626  nn0oddm1d2  12654  bitsfzolem  12699  bitsfzo  12700  bitsmod  12701  gcdaddm  12739  bezoutlemsup  12764  gcdzeq  12777  dvdssqlem  12785  nninfctlemfo  12795  nn0seqcvgd  12797  lcmneg  12830  mulgcddvds  12850  qredeu  12853  pw2dvdseulemle  12923  pw2dvdseu  12924  nn0sqrtelqelz  12962  nonsq  12963  pythagtriplem3  13024  pythagtriplem6  13027  pythagtriplem7  13028  pclemub  13044  pcprendvds  13047  pcpremul  13050  pcidlem  13080  pcgcd1  13085  pc2dvds  13087  pcz  13089  pcprmpw2  13090  fldivp1  13105  pcfaclem  13106  pcfac  13107  pcbc  13108  4sqexercise1  13155  4sqexercise2  13156  4sqlemsdc  13157  4sqlem11  13158  4sqlem12  13159  4sqlem14  13161  ennnfoneleminc  13280  ennnfonelemkh  13281  ennnfonelemex  13283  ennnfonelemim  13293  psrbaglesuppg  14980  psrbagcon  14985  mplsubgfilemcl  15013  plyaddlem1  15771  sgmppw  16020  gausslemma2dlem0h  16089  gausslemma2dlem4  16097  gausslemma2dlem6  16100  lgseisenlem1  16103  2lgsoddprmlem2  16139  2sqlem7  16154  2sqlem8  16156  vtxdgfifival  16446  vtxdgfif  16448  vtxd0nedgbfi  16454  eupth2lemsfi  16633