Theorem nn0red 9456

Description: A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nn0red.1	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Assertion

Ref	Expression
nn0red	⊢ (𝜑 → 𝐴 ∈ ℝ)

Proof of Theorem nn0red

Step	Hyp	Ref	Expression
1		nn0ssre 9406	. 2 ⊢ ℕ0 ⊆ ℝ
2		nn0red.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sselid 3225	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8031  ℕ₀cn0 9402

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8123  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129  ax-rnegex 8141

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-int 3929  df-inn 9144  df-n0 9403

This theorem is referenced by:  nn0cnd  9457  nn0readdcl  9461  eluzmn  9762  nn01to3  9851  xnn0dcle  10037  flqmulnn0  10560  modifeq2int  10649  modaddmodup  10650  modaddmodlo  10651  modsumfzodifsn  10659  expnegap0  10810  nn0leexp2  10973  nn0le2msqd  10982  nn0opthlem2d  10984  nn0opthd  10985  faclbnd6  11007  bcval5  11026  filtinf  11054  zfz1isolemiso  11104  wrdlenge2n0  11153  ccatsymb  11183  ccatrn  11190  ccatalpha  11194  ccat2s1fvwd  11228  swrdspsleq  11252  pfxsuffeqwrdeq  11283  swrdccat3blem  11324  mertenslemi1  12101  efcllemp  12224  eftlub  12256  oddge22np1  12447  nn0oddm1d2  12475  bitsfzolem  12520  bitsfzo  12521  bitsmod  12522  gcdaddm  12560  bezoutlemsup  12585  gcdzeq  12598  dvdssqlem  12606  nninfctlemfo  12616  nn0seqcvgd  12618  lcmneg  12651  mulgcddvds  12671  qredeu  12674  pw2dvdseulemle  12744  pw2dvdseu  12745  nn0sqrtelqelz  12783  nonsq  12784  pythagtriplem3  12845  pythagtriplem6  12848  pythagtriplem7  12849  pclemub  12865  pcprendvds  12868  pcpremul  12871  pcidlem  12901  pcgcd1  12906  pc2dvds  12908  pcz  12910  pcprmpw2  12911  fldivp1  12926  pcfaclem  12927  pcfac  12928  pcbc  12929  4sqexercise1  12976  4sqexercise2  12977  4sqlemsdc  12978  4sqlem11  12979  4sqlem12  12980  4sqlem14  12982  ennnfoneleminc  13037  ennnfonelemkh  13038  ennnfonelemex  13040  ennnfonelemim  13050  psrbaglesuppg  14692  mplsubgfilemcl  14719  plyaddlem1  15477  sgmppw  15722  gausslemma2dlem0h  15791  gausslemma2dlem4  15799  gausslemma2dlem6  15802  lgseisenlem1  15805  2lgsoddprmlem2  15841  2sqlem7  15856  2sqlem8  15858  vtxdgfifival  16148  vtxdgfif  16150  vtxd0nedgbfi  16156  eupth2lemsfi  16335