Theorem nn0red 9499

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 9449	. 2 ⊢ ℕ0 ⊆ ℝ
2		nn0red.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sselid 3226	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8074  ℕ₀cn0 9445

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-sep 4212  ax-cnex 8166  ax-resscn 8167  ax-1re 8169  ax-addrcl 8172  ax-rnegex 8184

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-int 3934  df-inn 9187  df-n0 9446

This theorem is referenced by:  nn0cnd  9500  nn0readdcl  9504  eluzmn  9805  nn01to3  9894  xnn0dcle  10080  flqmulnn0  10603  modifeq2int  10692  modaddmodup  10693  modaddmodlo  10694  modsumfzodifsn  10702  expnegap0  10853  nn0leexp2  11016  nn0le2msqd  11025  nn0opthlem2d  11027  nn0opthd  11028  faclbnd6  11050  bcval5  11069  filtinf  11097  zfz1isolemiso  11147  wrdlenge2n0  11196  ccatsymb  11226  ccatrn  11233  ccatalpha  11237  ccat2s1fvwd  11271  swrdspsleq  11295  pfxsuffeqwrdeq  11326  swrdccat3blem  11367  mertenslemi1  12157  efcllemp  12280  eftlub  12312  oddge22np1  12503  nn0oddm1d2  12531  bitsfzolem  12576  bitsfzo  12577  bitsmod  12578  gcdaddm  12616  bezoutlemsup  12641  gcdzeq  12654  dvdssqlem  12662  nninfctlemfo  12672  nn0seqcvgd  12674  lcmneg  12707  mulgcddvds  12727  qredeu  12730  pw2dvdseulemle  12800  pw2dvdseu  12801  nn0sqrtelqelz  12839  nonsq  12840  pythagtriplem3  12901  pythagtriplem6  12904  pythagtriplem7  12905  pclemub  12921  pcprendvds  12924  pcpremul  12927  pcidlem  12957  pcgcd1  12962  pc2dvds  12964  pcz  12966  pcprmpw2  12967  fldivp1  12982  pcfaclem  12983  pcfac  12984  pcbc  12985  4sqexercise1  13032  4sqexercise2  13033  4sqlemsdc  13034  4sqlem11  13035  4sqlem12  13036  4sqlem14  13038  ennnfoneleminc  13093  ennnfonelemkh  13094  ennnfonelemex  13096  ennnfonelemim  13106  psrbaglesuppg  14748  psrbagcon  14752  mplsubgfilemcl  14780  plyaddlem1  15538  sgmppw  15786  gausslemma2dlem0h  15855  gausslemma2dlem4  15863  gausslemma2dlem6  15866  lgseisenlem1  15869  2lgsoddprmlem2  15905  2sqlem7  15920  2sqlem8  15922  vtxdgfifival  16212  vtxdgfif  16214  vtxd0nedgbfi  16220  eupth2lemsfi  16399