Theorem nn0red 9320

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

Syntax hints:   -> wi 4   e. wcel 2167   RRcr 7895   NN0cn0 9266

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152  ax-cnex 7987  ax-resscn 7988  ax-1re 7990  ax-addrcl 7993  ax-rnegex 8005

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-sn 3629  df-int 3876  df-inn 9008  df-n0 9267

This theorem is referenced by:  nn0cnd  9321  nn0readdcl  9325  nn01to3  9708  xnn0dcle  9894  flqmulnn0  10406  modifeq2int  10495  modaddmodup  10496  modaddmodlo  10497  modsumfzodifsn  10505  expnegap0  10656  nn0leexp2  10819  nn0le2msqd  10828  nn0opthlem2d  10830  nn0opthd  10831  faclbnd6  10853  bcval5  10872  filtinf  10900  zfz1isolemiso  10948  wrdlenge2n0  10987  mertenslemi1  11717  efcllemp  11840  eftlub  11872  oddge22np1  12063  nn0oddm1d2  12091  bitsfzolem  12136  bitsfzo  12137  bitsmod  12138  gcdaddm  12176  bezoutlemsup  12201  gcdzeq  12214  dvdssqlem  12222  nninfctlemfo  12232  nn0seqcvgd  12234  lcmneg  12267  mulgcddvds  12287  qredeu  12290  pw2dvdseulemle  12360  pw2dvdseu  12361  nn0sqrtelqelz  12399  nonsq  12400  pythagtriplem3  12461  pythagtriplem6  12464  pythagtriplem7  12465  pclemub  12481  pcprendvds  12484  pcpremul  12487  pcidlem  12517  pcgcd1  12522  pc2dvds  12524  pcz  12526  pcprmpw2  12527  fldivp1  12542  pcfaclem  12543  pcfac  12544  pcbc  12545  4sqexercise1  12592  4sqexercise2  12593  4sqlemsdc  12594  4sqlem11  12595  4sqlem12  12596  4sqlem14  12598  ennnfoneleminc  12653  ennnfonelemkh  12654  ennnfonelemex  12656  ennnfonelemim  12666  psrbaglesuppg  14302  plyaddlem1  15067  sgmppw  15312  gausslemma2dlem0h  15381  gausslemma2dlem4  15389  gausslemma2dlem6  15392  lgseisenlem1  15395  2lgsoddprmlem2  15431  2sqlem7  15446  2sqlem8  15448