Theorem nn0red 9203

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

Syntax hints:   → wi 4   ∈ wcel 2146  ℝcr 7785  ℕ₀cn0 9149

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-sep 4116  ax-cnex 7877  ax-resscn 7878  ax-1re 7880  ax-addrcl 7883  ax-rnegex 7895

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-rex 2459  df-v 2737  df-un 3131  df-in 3133  df-ss 3140  df-sn 3595  df-int 3841  df-inn 8893  df-n0 9150

This theorem is referenced by:  nn0cnd  9204  nn0readdcl  9208  nn01to3  9590  xnn0dcle  9773  flqmulnn0  10269  modifeq2int  10356  modaddmodup  10357  modaddmodlo  10358  modsumfzodifsn  10366  expnegap0  10498  nn0leexp2  10659  nn0le2msqd  10667  nn0opthlem2d  10669  nn0opthd  10670  faclbnd6  10692  bcval5  10711  filtinf  10739  zfz1isolemiso  10787  mertenslemi1  11511  efcllemp  11634  eftlub  11666  oddge22np1  11853  nn0oddm1d2  11881  gcdaddm  11952  bezoutlemsup  11977  gcdzeq  11990  dvdssqlem  11998  nn0seqcvgd  12008  lcmneg  12041  mulgcddvds  12061  qredeu  12064  pw2dvdseulemle  12134  pw2dvdseu  12135  nn0sqrtelqelz  12173  nonsq  12174  pythagtriplem3  12234  pythagtriplem6  12237  pythagtriplem7  12238  pclemub  12254  pcprendvds  12257  pcpremul  12260  pcidlem  12289  pcgcd1  12294  pc2dvds  12296  pcz  12298  pcprmpw2  12299  fldivp1  12313  pcfaclem  12314  pcfac  12315  pcbc  12316  ennnfoneleminc  12379  ennnfonelemkh  12380  ennnfonelemex  12382  ennnfonelemim  12392  2sqlem7  14037  2sqlem8  14039