Theorem nn0re 9374

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 9369	. 2 ⊢ ℕ0 ⊆ ℝ
2	1	sseli 3220	1 ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ)

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:  nn0nlt0  9391  nn0le0eq0  9393  nn0p1gt0  9394  elnnnn0c  9410  nn0addge1  9411  nn0addge2  9412  nn0ge2m1nn  9425  nn0nndivcl  9427  xnn0xr  9433  nn0nepnf  9436  xnn0nemnf  9439  elnn0z  9455  elznn0nn  9456  ltsubnn0  9510  nn0negleid  9511  difgtsumgt  9512  nn0lt10b  9523  nn0ge0div  9530  xnn0lenn0nn0  10057  xnn0xadd0  10059  nn0fz0  10311  elfz0fzfz0  10318  fz0fzelfz0  10319  fz0fzdiffz0  10322  fzctr  10325  difelfzle  10326  difelfznle  10327  fzoun  10375  elfzo0le  10381  fzonmapblen  10383  fzofzim  10384  elincfzoext  10394  elfzodifsumelfzo  10402  fzonn0p1  10412  fzonn0p1p1  10414  elfzom1p1elfzo  10415  ubmelm1fzo  10427  fvinim0ffz  10442  subfzo0  10443  adddivflid  10507  divfl0  10511  flltdivnn0lt  10519  addmodid  10589  modfzo0difsn  10612  inftonninf  10659  bernneq  10877  bernneq3  10879  facwordi  10957  faclbnd  10958  faclbnd3  10960  faclbnd6  10961  facubnd  10962  facavg  10963  bcval4  10969  bcval5  10980  bcpasc  10983  fihashneq0  11011  ccat0  11126  swrdsbslen  11193  swrdswrdlem  11231  swrdswrd  11232  swrdccatin1  11252  pfxccatin12lem2  11258  pfxccatin12lem3  11259  pfxccat3  11261  swrdccat  11262  swrdccat3blem  11266  nn0maxcl  11731  dvdseq  12354  oddge22np1  12387  nn0ehalf  12409  nn0o  12413  nn0oddm1d2  12415  bitsfi  12463  gcdn0gt0  12494  nn0gcdid0  12497  absmulgcd  12533  nn0seqcvgd  12558  algcvgblem  12566  algcvga  12568  lcmgcdnn  12599  prmfac1  12669  nonsq  12724  hashgcdlem  12755  odzdvds  12763  pcdvdsb  12838  pcidlem  12841  difsqpwdvds  12856  pcfaclem  12867  lgsdinn0  15721  2lgslem1c  15763