Theorem nn0red 9384

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

Syntax hints:   -> wi 4   e. wcel 2178   RRcr 7959   NN0cn0 9330

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-sep 4178  ax-cnex 8051  ax-resscn 8052  ax-1re 8054  ax-addrcl 8057  ax-rnegex 8069

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-sn 3649  df-int 3900  df-inn 9072  df-n0 9331

This theorem is referenced by:  nn0cnd  9385  nn0readdcl  9389  nn01to3  9773  xnn0dcle  9959  flqmulnn0  10479  modifeq2int  10568  modaddmodup  10569  modaddmodlo  10570  modsumfzodifsn  10578  expnegap0  10729  nn0leexp2  10892  nn0le2msqd  10901  nn0opthlem2d  10903  nn0opthd  10904  faclbnd6  10926  bcval5  10945  filtinf  10973  zfz1isolemiso  11021  wrdlenge2n0  11066  ccatsymb  11096  ccatrn  11103  swrdspsleq  11158  pfxsuffeqwrdeq  11189  swrdccat3blem  11230  mertenslemi1  11961  efcllemp  12084  eftlub  12116  oddge22np1  12307  nn0oddm1d2  12335  bitsfzolem  12380  bitsfzo  12381  bitsmod  12382  gcdaddm  12420  bezoutlemsup  12445  gcdzeq  12458  dvdssqlem  12466  nninfctlemfo  12476  nn0seqcvgd  12478  lcmneg  12511  mulgcddvds  12531  qredeu  12534  pw2dvdseulemle  12604  pw2dvdseu  12605  nn0sqrtelqelz  12643  nonsq  12644  pythagtriplem3  12705  pythagtriplem6  12708  pythagtriplem7  12709  pclemub  12725  pcprendvds  12728  pcpremul  12731  pcidlem  12761  pcgcd1  12766  pc2dvds  12768  pcz  12770  pcprmpw2  12771  fldivp1  12786  pcfaclem  12787  pcfac  12788  pcbc  12789  4sqexercise1  12836  4sqexercise2  12837  4sqlemsdc  12838  4sqlem11  12839  4sqlem12  12840  4sqlem14  12842  ennnfoneleminc  12897  ennnfonelemkh  12898  ennnfonelemex  12900  ennnfonelemim  12910  psrbaglesuppg  14549  mplsubgfilemcl  14576  plyaddlem1  15334  sgmppw  15579  gausslemma2dlem0h  15648  gausslemma2dlem4  15656  gausslemma2dlem6  15659  lgseisenlem1  15662  2lgsoddprmlem2  15698  2sqlem7  15713  2sqlem8  15715