Theorem nn0red 9411

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 7986  ℕ₀cn0 9357

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 8078  ax-resscn 8079  ax-1re 8081  ax-addrcl 8084  ax-rnegex 8096

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 9099  df-n0 9358

This theorem is referenced by:  nn0cnd  9412  nn0readdcl  9416  nn01to3  9800  xnn0dcle  9986  flqmulnn0  10506  modifeq2int  10595  modaddmodup  10596  modaddmodlo  10597  modsumfzodifsn  10605  expnegap0  10756  nn0leexp2  10919  nn0le2msqd  10928  nn0opthlem2d  10930  nn0opthd  10931  faclbnd6  10953  bcval5  10972  filtinf  11000  zfz1isolemiso  11048  wrdlenge2n0  11093  ccatsymb  11123  ccatrn  11130  swrdspsleq  11185  pfxsuffeqwrdeq  11216  swrdccat3blem  11257  mertenslemi1  12032  efcllemp  12155  eftlub  12187  oddge22np1  12378  nn0oddm1d2  12406  bitsfzolem  12451  bitsfzo  12452  bitsmod  12453  gcdaddm  12491  bezoutlemsup  12516  gcdzeq  12529  dvdssqlem  12537  nninfctlemfo  12547  nn0seqcvgd  12549  lcmneg  12582  mulgcddvds  12602  qredeu  12605  pw2dvdseulemle  12675  pw2dvdseu  12676  nn0sqrtelqelz  12714  nonsq  12715  pythagtriplem3  12776  pythagtriplem6  12779  pythagtriplem7  12780  pclemub  12796  pcprendvds  12799  pcpremul  12802  pcidlem  12832  pcgcd1  12837  pc2dvds  12839  pcz  12841  pcprmpw2  12842  fldivp1  12857  pcfaclem  12858  pcfac  12859  pcbc  12860  4sqexercise1  12907  4sqexercise2  12908  4sqlemsdc  12909  4sqlem11  12910  4sqlem12  12911  4sqlem14  12913  ennnfoneleminc  12968  ennnfonelemkh  12969  ennnfonelemex  12971  ennnfonelemim  12981  psrbaglesuppg  14621  mplsubgfilemcl  14648  plyaddlem1  15406  sgmppw  15651  gausslemma2dlem0h  15720  gausslemma2dlem4  15728  gausslemma2dlem6  15731  lgseisenlem1  15734  2lgsoddprmlem2  15770  2sqlem7  15785  2sqlem8  15787