Theorem nn0red 9419

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 7994  ℕ₀cn0 9365

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4201  ax-cnex 8086  ax-resscn 8087  ax-1re 8089  ax-addrcl 8092  ax-rnegex 8104

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-int 3923  df-inn 9107  df-n0 9366

This theorem is referenced by:  nn0cnd  9420  nn0readdcl  9424  nn01to3  9808  xnn0dcle  9994  flqmulnn0  10514  modifeq2int  10603  modaddmodup  10604  modaddmodlo  10605  modsumfzodifsn  10613  expnegap0  10764  nn0leexp2  10927  nn0le2msqd  10936  nn0opthlem2d  10938  nn0opthd  10939  faclbnd6  10961  bcval5  10980  filtinf  11008  zfz1isolemiso  11056  wrdlenge2n0  11102  ccatsymb  11132  ccatrn  11139  swrdspsleq  11194  pfxsuffeqwrdeq  11225  swrdccat3blem  11266  mertenslemi1  12041  efcllemp  12164  eftlub  12196  oddge22np1  12387  nn0oddm1d2  12415  bitsfzolem  12460  bitsfzo  12461  bitsmod  12462  gcdaddm  12500  bezoutlemsup  12525  gcdzeq  12538  dvdssqlem  12546  nninfctlemfo  12556  nn0seqcvgd  12558  lcmneg  12591  mulgcddvds  12611  qredeu  12614  pw2dvdseulemle  12684  pw2dvdseu  12685  nn0sqrtelqelz  12723  nonsq  12724  pythagtriplem3  12785  pythagtriplem6  12788  pythagtriplem7  12789  pclemub  12805  pcprendvds  12808  pcpremul  12811  pcidlem  12841  pcgcd1  12846  pc2dvds  12848  pcz  12850  pcprmpw2  12851  fldivp1  12866  pcfaclem  12867  pcfac  12868  pcbc  12869  4sqexercise1  12916  4sqexercise2  12917  4sqlemsdc  12918  4sqlem11  12919  4sqlem12  12920  4sqlem14  12922  ennnfoneleminc  12977  ennnfonelemkh  12978  ennnfonelemex  12980  ennnfonelemim  12990  psrbaglesuppg  14630  mplsubgfilemcl  14657  plyaddlem1  15415  sgmppw  15660  gausslemma2dlem0h  15729  gausslemma2dlem4  15737  gausslemma2dlem6  15740  lgseisenlem1  15743  2lgsoddprmlem2  15779  2sqlem7  15794  2sqlem8  15796