Theorem nn0red 9553

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℝcr 8125  ℕ₀cn0 9495

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 2214  ax-sep 4227  ax-cnex 8217  ax-resscn 8218  ax-1re 8220  ax-addrcl 8223  ax-rnegex 8235

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2814  df-un 3214  df-in 3216  df-ss 3223  df-sn 3694  df-int 3949  df-inn 9237  df-n0 9496

This theorem is referenced by:  nn0cnd  9554  nn0readdcl  9558  eluzmn  9859  nn01to3  9948  xnn0dcle  10134  flqmulnn0  10658  modifeq2int  10747  modaddmodup  10748  modaddmodlo  10749  modsumfzodifsn  10757  expnegap0  10908  nn0leexp2  11071  nn0le2msqd  11080  nn0opthlem2d  11082  nn0opthd  11083  faclbnd6  11105  bcval5  11124  filtinf  11152  sshashneg  11201  zfz1isolemiso  11207  wrdlenge2n0  11256  ccatsymb  11286  ccatrn  11293  ccatalpha  11297  ccat2s1fvwd  11331  swrdspsleq  11355  pfxsuffeqwrdeq  11386  swrdccat3blem  11427  mertenslemi1  12217  efcllemp  12340  eftlub  12372  oddge22np1  12563  nn0oddm1d2  12591  bitsfzolem  12636  bitsfzo  12637  bitsmod  12638  gcdaddm  12676  bezoutlemsup  12701  gcdzeq  12714  dvdssqlem  12722  nninfctlemfo  12732  nn0seqcvgd  12734  lcmneg  12767  mulgcddvds  12787  qredeu  12790  pw2dvdseulemle  12860  pw2dvdseu  12861  nn0sqrtelqelz  12899  nonsq  12900  pythagtriplem3  12961  pythagtriplem6  12964  pythagtriplem7  12965  pclemub  12981  pcprendvds  12984  pcpremul  12987  pcidlem  13017  pcgcd1  13022  pc2dvds  13024  pcz  13026  pcprmpw2  13027  fldivp1  13042  pcfaclem  13043  pcfac  13044  pcbc  13045  4sqexercise1  13092  4sqexercise2  13093  4sqlemsdc  13094  4sqlem11  13095  4sqlem12  13096  4sqlem14  13098  ennnfoneleminc  13154  ennnfonelemkh  13155  ennnfonelemex  13157  ennnfonelemim  13167  psrbaglesuppg  14813  psrbagcon  14818  mplsubgfilemcl  14846  plyaddlem1  15604  sgmppw  15852  gausslemma2dlem0h  15921  gausslemma2dlem4  15929  gausslemma2dlem6  15932  lgseisenlem1  15935  2lgsoddprmlem2  15971  2sqlem7  15986  2sqlem8  15988  vtxdgfifival  16278  vtxdgfif  16280  vtxd0nedgbfi  16286  eupth2lemsfi  16465