Theorem nn0re 9394

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8014  ℕ₀cn0 9385

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 4202  ax-cnex 8106  ax-resscn 8107  ax-1re 8109  ax-addrcl 8112  ax-rnegex 8124

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 3924  df-inn 9127  df-n0 9386

This theorem is referenced by:  nn0nlt0  9411  nn0le0eq0  9413  nn0p1gt0  9414  elnnnn0c  9430  nn0addge1  9431  nn0addge2  9432  nn0ge2m1nn  9445  nn0nndivcl  9447  xnn0xr  9453  nn0nepnf  9456  xnn0nemnf  9459  elnn0z  9475  elznn0nn  9476  ltsubnn0  9530  nn0negleid  9531  difgtsumgt  9532  nn0lt10b  9543  nn0ge0div  9550  xnn0lenn0nn0  10078  xnn0xadd0  10080  nn0fz0  10332  elfz0fzfz0  10339  fz0fzelfz0  10340  fz0fzdiffz0  10343  fzctr  10346  difelfzle  10347  difelfznle  10348  fzoun  10396  elfzo0le  10402  fzonmapblen  10404  fzofzim  10405  elincfzoext  10416  elfzodifsumelfzo  10424  fzonn0p1  10434  fzonn0p1p1  10436  elfzom1p1elfzo  10437  ubmelm1fzo  10449  fvinim0ffz  10464  subfzo0  10465  adddivflid  10529  divfl0  10533  flltdivnn0lt  10541  addmodid  10611  modfzo0difsn  10634  inftonninf  10681  bernneq  10899  bernneq3  10901  facwordi  10979  faclbnd  10980  faclbnd3  10982  faclbnd6  10983  facubnd  10984  facavg  10985  bcval4  10991  bcval5  11002  bcpasc  11005  fihashneq0  11033  ccat0  11149  swrdsbslen  11219  swrdswrdlem  11257  swrdswrd  11258  swrdccatin1  11278  pfxccatin12lem2  11284  pfxccatin12lem3  11285  pfxccat3  11287  swrdccat  11288  swrdccat3blem  11292  nn0maxcl  11757  dvdseq  12380  oddge22np1  12413  nn0ehalf  12435  nn0o  12439  nn0oddm1d2  12441  bitsfi  12489  gcdn0gt0  12520  nn0gcdid0  12523  absmulgcd  12559  nn0seqcvgd  12584  algcvgblem  12592  algcvga  12594  lcmgcdnn  12625  prmfac1  12695  nonsq  12750  hashgcdlem  12781  odzdvds  12789  pcdvdsb  12864  pcidlem  12867  difsqpwdvds  12882  pcfaclem  12893  lgsdinn0  15748  2lgslem1c  15790