Theorem nn0re 9099

Description: A nonnegative integer is a real number. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nn0re	⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ)

Proof of Theorem nn0re

Step	Hyp	Ref	Expression
1		nn0ssre 9094	. 2 ⊢ ℕ0 ⊆ ℝ
2	1	sseli 3124	1 ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2128  ℝcr 7731  ℕ₀cn0 9090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139  ax-sep 4082  ax-cnex 7823  ax-resscn 7824  ax-1re 7826  ax-addrcl 7829  ax-rnegex 7841

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-sn 3566  df-int 3808  df-inn 8834  df-n0 9091

This theorem is referenced by:  nn0nlt0  9116  nn0le0eq0  9118  nn0p1gt0  9119  elnnnn0c  9135  nn0addge1  9136  nn0addge2  9137  nn0ge2m1nn  9150  nn0nndivcl  9152  xnn0xr  9158  nn0nepnf  9161  xnn0nemnf  9164  elnn0z  9180  elznn0nn  9181  nn0lt10b  9244  nn0ge0div  9251  xnn0lenn0nn0  9769  xnn0xadd0  9771  nn0fz0  10021  elfz0fzfz0  10025  fz0fzelfz0  10026  fz0fzdiffz0  10029  fzctr  10032  difelfzle  10033  difelfznle  10034  elfzo0le  10084  fzonmapblen  10086  fzofzim  10087  elfzodifsumelfzo  10100  fzonn0p1  10110  fzonn0p1p1  10112  elfzom1p1elfzo  10113  ubmelm1fzo  10125  fvinim0ffz  10140  subfzo0  10141  adddivflid  10191  divfl0  10195  flltdivnn0lt  10203  addmodid  10271  modfzo0difsn  10294  inftonninf  10340  bernneq  10538  bernneq3  10540  facwordi  10614  faclbnd  10615  faclbnd3  10617  faclbnd6  10618  facubnd  10619  facavg  10620  bcval4  10626  bcval5  10637  bcpasc  10640  fihashneq0  10669  dvdseq  11739  oddge22np1  11771  nn0ehalf  11793  nn0o  11797  nn0oddm1d2  11799  gcdn0gt0  11861  nn0gcdid0  11864  absmulgcd  11900  nn0seqcvgd  11917  algcvgblem  11925  algcvga  11927  lcmgcdnn  11958  prmfac1  12026  nonsq  12081  hashgcdlem  12112  odzdvds  12119