Theorem nn0red 9260

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

Syntax hints:   -> wi 4   e. wcel 2160   RRcr 7840   NN0cn0 9206

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-sep 4136  ax-cnex 7932  ax-resscn 7933  ax-1re 7935  ax-addrcl 7938  ax-rnegex 7950

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-sn 3613  df-int 3860  df-inn 8950  df-n0 9207

This theorem is referenced by:  nn0cnd  9261  nn0readdcl  9265  nn01to3  9647  xnn0dcle  9832  flqmulnn0  10330  modifeq2int  10417  modaddmodup  10418  modaddmodlo  10419  modsumfzodifsn  10427  expnegap0  10559  nn0leexp2  10722  nn0le2msqd  10731  nn0opthlem2d  10733  nn0opthd  10734  faclbnd6  10756  bcval5  10775  filtinf  10803  zfz1isolemiso  10851  mertenslemi1  11575  efcllemp  11698  eftlub  11730  oddge22np1  11918  nn0oddm1d2  11946  gcdaddm  12017  bezoutlemsup  12042  gcdzeq  12055  dvdssqlem  12063  nn0seqcvgd  12073  lcmneg  12106  mulgcddvds  12126  qredeu  12129  pw2dvdseulemle  12199  pw2dvdseu  12200  nn0sqrtelqelz  12238  nonsq  12239  pythagtriplem3  12299  pythagtriplem6  12302  pythagtriplem7  12303  pclemub  12319  pcprendvds  12322  pcpremul  12325  pcidlem  12355  pcgcd1  12360  pc2dvds  12362  pcz  12364  pcprmpw2  12365  fldivp1  12380  pcfaclem  12381  pcfac  12382  pcbc  12383  4sqexercise1  12430  4sqexercise2  12431  4sqlemsdc  12432  4sqlem11  12433  4sqlem12  12434  4sqlem14  12436  ennnfoneleminc  12462  ennnfonelemkh  12463  ennnfonelemex  12465  ennnfonelemim  12475  psrbaglesuppg  13950  lgseisenlem1  14911  2lgsoddprmlem2  14915  2sqlem7  14929  2sqlem8  14931