Theorem nn0red 9230

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

Syntax hints:   -> wi 4   e. wcel 2148   RRcr 7810   NN0cn0 9176

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4122  ax-cnex 7902  ax-resscn 7903  ax-1re 7905  ax-addrcl 7908  ax-rnegex 7920

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-sn 3599  df-int 3846  df-inn 8920  df-n0 9177

This theorem is referenced by:  nn0cnd  9231  nn0readdcl  9235  nn01to3  9617  xnn0dcle  9802  flqmulnn0  10299  modifeq2int  10386  modaddmodup  10387  modaddmodlo  10388  modsumfzodifsn  10396  expnegap0  10528  nn0leexp2  10690  nn0le2msqd  10699  nn0opthlem2d  10701  nn0opthd  10702  faclbnd6  10724  bcval5  10743  filtinf  10771  zfz1isolemiso  10819  mertenslemi1  11543  efcllemp  11666  eftlub  11698  oddge22np1  11886  nn0oddm1d2  11914  gcdaddm  11985  bezoutlemsup  12010  gcdzeq  12023  dvdssqlem  12031  nn0seqcvgd  12041  lcmneg  12074  mulgcddvds  12094  qredeu  12097  pw2dvdseulemle  12167  pw2dvdseu  12168  nn0sqrtelqelz  12206  nonsq  12207  pythagtriplem3  12267  pythagtriplem6  12270  pythagtriplem7  12271  pclemub  12287  pcprendvds  12290  pcpremul  12293  pcidlem  12322  pcgcd1  12327  pc2dvds  12329  pcz  12331  pcprmpw2  12332  fldivp1  12346  pcfaclem  12347  pcfac  12348  pcbc  12349  ennnfoneleminc  12412  ennnfonelemkh  12413  ennnfonelemex  12415  ennnfonelemim  12425  lgseisenlem1  14453  2lgsoddprmlem2  14457  2sqlem7  14471  2sqlem8  14473