Theorem nn0red 9423

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

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 7998   NN0cn0 9369

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 4202  ax-cnex 8090  ax-resscn 8091  ax-1re 8093  ax-addrcl 8096  ax-rnegex 8108

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 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-int 3924  df-inn 9111  df-n0 9370

This theorem is referenced by:  nn0cnd  9424  nn0readdcl  9428  nn01to3  9812  xnn0dcle  9998  flqmulnn0  10519  modifeq2int  10608  modaddmodup  10609  modaddmodlo  10610  modsumfzodifsn  10618  expnegap0  10769  nn0leexp2  10932  nn0le2msqd  10941  nn0opthlem2d  10943  nn0opthd  10944  faclbnd6  10966  bcval5  10985  filtinf  11013  zfz1isolemiso  11061  wrdlenge2n0  11107  ccatsymb  11137  ccatrn  11144  swrdspsleq  11199  pfxsuffeqwrdeq  11230  swrdccat3blem  11271  mertenslemi1  12046  efcllemp  12169  eftlub  12201  oddge22np1  12392  nn0oddm1d2  12420  bitsfzolem  12465  bitsfzo  12466  bitsmod  12467  gcdaddm  12505  bezoutlemsup  12530  gcdzeq  12543  dvdssqlem  12551  nninfctlemfo  12561  nn0seqcvgd  12563  lcmneg  12596  mulgcddvds  12616  qredeu  12619  pw2dvdseulemle  12689  pw2dvdseu  12690  nn0sqrtelqelz  12728  nonsq  12729  pythagtriplem3  12790  pythagtriplem6  12793  pythagtriplem7  12794  pclemub  12810  pcprendvds  12813  pcpremul  12816  pcidlem  12846  pcgcd1  12851  pc2dvds  12853  pcz  12855  pcprmpw2  12856  fldivp1  12871  pcfaclem  12872  pcfac  12873  pcbc  12874  4sqexercise1  12921  4sqexercise2  12922  4sqlemsdc  12923  4sqlem11  12924  4sqlem12  12925  4sqlem14  12927  ennnfoneleminc  12982  ennnfonelemkh  12983  ennnfonelemex  12985  ennnfonelemim  12995  psrbaglesuppg  14636  mplsubgfilemcl  14663  plyaddlem1  15421  sgmppw  15666  gausslemma2dlem0h  15735  gausslemma2dlem4  15743  gausslemma2dlem6  15746  lgseisenlem1  15749  2lgsoddprmlem2  15785  2sqlem7  15800  2sqlem8  15802