Theorem nn0re 9389

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8009  ℕ₀cn0 9380

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 8101  ax-resscn 8102  ax-1re 8104  ax-addrcl 8107  ax-rnegex 8119

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 9122  df-n0 9381

This theorem is referenced by:  nn0nlt0  9406  nn0le0eq0  9408  nn0p1gt0  9409  elnnnn0c  9425  nn0addge1  9426  nn0addge2  9427  nn0ge2m1nn  9440  nn0nndivcl  9442  xnn0xr  9448  nn0nepnf  9451  xnn0nemnf  9454  elnn0z  9470  elznn0nn  9471  ltsubnn0  9525  nn0negleid  9526  difgtsumgt  9527  nn0lt10b  9538  nn0ge0div  9545  xnn0lenn0nn0  10073  xnn0xadd0  10075  nn0fz0  10327  elfz0fzfz0  10334  fz0fzelfz0  10335  fz0fzdiffz0  10338  fzctr  10341  difelfzle  10342  difelfznle  10343  fzoun  10391  elfzo0le  10397  fzonmapblen  10399  fzofzim  10400  elincfzoext  10411  elfzodifsumelfzo  10419  fzonn0p1  10429  fzonn0p1p1  10431  elfzom1p1elfzo  10432  ubmelm1fzo  10444  fvinim0ffz  10459  subfzo0  10460  adddivflid  10524  divfl0  10528  flltdivnn0lt  10536  addmodid  10606  modfzo0difsn  10629  inftonninf  10676  bernneq  10894  bernneq3  10896  facwordi  10974  faclbnd  10975  faclbnd3  10977  faclbnd6  10978  facubnd  10979  facavg  10980  bcval4  10986  bcval5  10997  bcpasc  11000  fihashneq0  11028  ccat0  11144  swrdsbslen  11213  swrdswrdlem  11251  swrdswrd  11252  swrdccatin1  11272  pfxccatin12lem2  11278  pfxccatin12lem3  11279  pfxccat3  11281  swrdccat  11282  swrdccat3blem  11286  nn0maxcl  11751  dvdseq  12374  oddge22np1  12407  nn0ehalf  12429  nn0o  12433  nn0oddm1d2  12435  bitsfi  12483  gcdn0gt0  12514  nn0gcdid0  12517  absmulgcd  12553  nn0seqcvgd  12578  algcvgblem  12586  algcvga  12588  lcmgcdnn  12619  prmfac1  12689  nonsq  12744  hashgcdlem  12775  odzdvds  12783  pcdvdsb  12858  pcidlem  12861  difsqpwdvds  12876  pcfaclem  12887  lgsdinn0  15742  2lgslem1c  15784