Theorem nn0re 9303

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

Syntax hints:   → wi 4   ∈ wcel 2175  ℝcr 7923  ℕ₀cn0 9294

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-sep 4161  ax-cnex 8015  ax-resscn 8016  ax-1re 8018  ax-addrcl 8021  ax-rnegex 8033

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-v 2773  df-un 3169  df-in 3171  df-ss 3178  df-sn 3638  df-int 3885  df-inn 9036  df-n0 9295

This theorem is referenced by:  nn0nlt0  9320  nn0le0eq0  9322  nn0p1gt0  9323  elnnnn0c  9339  nn0addge1  9340  nn0addge2  9341  nn0ge2m1nn  9354  nn0nndivcl  9356  xnn0xr  9362  nn0nepnf  9365  xnn0nemnf  9368  elnn0z  9384  elznn0nn  9385  ltsubnn0  9439  nn0negleid  9440  difgtsumgt  9441  nn0lt10b  9452  nn0ge0div  9459  xnn0lenn0nn0  9986  xnn0xadd0  9988  nn0fz0  10240  elfz0fzfz0  10247  fz0fzelfz0  10248  fz0fzdiffz0  10251  fzctr  10254  difelfzle  10255  difelfznle  10256  elfzo0le  10307  fzonmapblen  10309  fzofzim  10310  elincfzoext  10320  elfzodifsumelfzo  10328  fzonn0p1  10338  fzonn0p1p1  10340  elfzom1p1elfzo  10341  ubmelm1fzo  10353  fvinim0ffz  10368  subfzo0  10369  adddivflid  10433  divfl0  10437  flltdivnn0lt  10445  addmodid  10515  modfzo0difsn  10538  inftonninf  10585  bernneq  10803  bernneq3  10805  facwordi  10883  faclbnd  10884  faclbnd3  10886  faclbnd6  10887  facubnd  10888  facavg  10889  bcval4  10895  bcval5  10906  bcpasc  10909  fihashneq0  10937  ccat0  11050  nn0maxcl  11478  dvdseq  12101  oddge22np1  12134  nn0ehalf  12156  nn0o  12160  nn0oddm1d2  12162  bitsfi  12210  gcdn0gt0  12241  nn0gcdid0  12244  absmulgcd  12280  nn0seqcvgd  12305  algcvgblem  12313  algcvga  12315  lcmgcdnn  12346  prmfac1  12416  nonsq  12471  hashgcdlem  12502  odzdvds  12510  pcdvdsb  12585  pcidlem  12588  difsqpwdvds  12603  pcfaclem  12614  lgsdinn0  15467  2lgslem1c  15509