Theorem nn0red 9517

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

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8091   NN0cn0 9461

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-sep 4212  ax-cnex 8183  ax-resscn 8184  ax-1re 8186  ax-addrcl 8189  ax-rnegex 8201

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-int 3934  df-inn 9203  df-n0 9462

This theorem is referenced by:  nn0cnd  9518  nn0readdcl  9522  eluzmn  9823  nn01to3  9912  xnn0dcle  10098  flqmulnn0  10622  modifeq2int  10711  modaddmodup  10712  modaddmodlo  10713  modsumfzodifsn  10721  expnegap0  10872  nn0leexp2  11035  nn0le2msqd  11044  nn0opthlem2d  11046  nn0opthd  11047  faclbnd6  11069  bcval5  11088  filtinf  11116  zfz1isolemiso  11166  wrdlenge2n0  11215  ccatsymb  11245  ccatrn  11252  ccatalpha  11256  ccat2s1fvwd  11290  swrdspsleq  11314  pfxsuffeqwrdeq  11345  swrdccat3blem  11386  mertenslemi1  12176  efcllemp  12299  eftlub  12331  oddge22np1  12522  nn0oddm1d2  12550  bitsfzolem  12595  bitsfzo  12596  bitsmod  12597  gcdaddm  12635  bezoutlemsup  12660  gcdzeq  12673  dvdssqlem  12681  nninfctlemfo  12691  nn0seqcvgd  12693  lcmneg  12726  mulgcddvds  12746  qredeu  12749  pw2dvdseulemle  12819  pw2dvdseu  12820  nn0sqrtelqelz  12858  nonsq  12859  pythagtriplem3  12920  pythagtriplem6  12923  pythagtriplem7  12924  pclemub  12940  pcprendvds  12943  pcpremul  12946  pcidlem  12976  pcgcd1  12981  pc2dvds  12983  pcz  12985  pcprmpw2  12986  fldivp1  13001  pcfaclem  13002  pcfac  13003  pcbc  13004  4sqexercise1  13051  4sqexercise2  13052  4sqlemsdc  13053  4sqlem11  13054  4sqlem12  13055  4sqlem14  13057  ennnfoneleminc  13112  ennnfonelemkh  13113  ennnfonelemex  13115  ennnfonelemim  13125  psrbaglesuppg  14768  psrbagcon  14772  mplsubgfilemcl  14800  plyaddlem1  15558  sgmppw  15806  gausslemma2dlem0h  15875  gausslemma2dlem4  15883  gausslemma2dlem6  15886  lgseisenlem1  15889  2lgsoddprmlem2  15925  2sqlem7  15940  2sqlem8  15942  vtxdgfifival  16232  vtxdgfif  16234  vtxd0nedgbfi  16240  eupth2lemsfi  16419