Theorem nn0red 9604

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

Syntax hints:   → wi 4   ∈ wcel 2209  ℝcr 8172  ℕ₀cn0 9546

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4247  ax-cnex 8264  ax-resscn 8265  ax-1re 8267  ax-addrcl 8270  ax-rnegex 8282

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3714  df-int 3969  df-inn 9288  df-n0 9547

This theorem is referenced by:  nn0cnd  9605  nn0readdcl  9609  eluzmn  9911  nn01to3  10000  xnn0dcle  10187  flqmulnn0  10717  modifeq2int  10806  modaddmodup  10807  modaddmodlo  10808  modsumfzodifsn  10816  expnegap0  10967  nn0leexp2  11131  nn0le2msqd  11140  nn0opthlem2d  11142  nn0opthd  11143  faclbnd6  11165  bcval5  11184  filtinf  11213  sshashneg  11264  hashf1  11270  zfz1isolemiso  11274  wrdlenge2n0  11323  ccatsymb  11353  ccatrn  11360  ccatalpha  11364  ccat2s1fvwd  11398  swrdspsleq  11422  pfxsuffeqwrdeq  11453  swrdccat3blem  11494  mertenslemi1  12285  efcllemp  12408  eftlub  12440  oddge22np1  12631  nn0oddm1d2  12659  bitsfzolem  12704  bitsfzo  12705  bitsmod  12706  gcdaddm  12744  bezoutlemsup  12769  gcdzeq  12782  dvdssqlem  12790  nninfctlemfo  12800  nn0seqcvgd  12802  lcmneg  12835  mulgcddvds  12855  qredeu  12858  pw2dvdseulemle  12928  pw2dvdseu  12929  nn0sqrtelqelz  12967  nonsq  12968  pythagtriplem3  13029  pythagtriplem6  13032  pythagtriplem7  13033  pclemub  13049  pcprendvds  13052  pcpremul  13055  pcidlem  13085  pcgcd1  13090  pc2dvds  13092  pcz  13094  pcprmpw2  13095  fldivp1  13110  pcfaclem  13111  pcfac  13112  pcbc  13113  4sqexercise1  13160  4sqexercise2  13161  4sqlemsdc  13162  4sqlem11  13163  4sqlem12  13164  4sqlem14  13166  ennnfoneleminc  13285  ennnfonelemkh  13286  ennnfonelemex  13288  ennnfonelemim  13298  psrbaglesuppg  15040  psrbagcon  15045  mplsubgfilemcl  15073  plyaddlem1  15831  log2tlbndlog2  16065  birthdaylem2  16071  birthdaylem3  16072  sgmppw  16089  gausslemma2dlem0h  16158  gausslemma2dlem4  16166  gausslemma2dlem6  16169  lgseisenlem1  16172  2lgsoddprmlem2  16208  2sqlem7  16223  2sqlem8  16225  vtxdgfifival  16515  vtxdgfif  16517  vtxd0nedgbfi  16523  eupth2lemsfi  16702