Theorem nn0re 9249

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℝcr 7871  ℕ₀cn0 9240

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4147  ax-cnex 7963  ax-resscn 7964  ax-1re 7966  ax-addrcl 7969  ax-rnegex 7981

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-sn 3624  df-int 3871  df-inn 8983  df-n0 9241

This theorem is referenced by:  nn0nlt0  9266  nn0le0eq0  9268  nn0p1gt0  9269  elnnnn0c  9285  nn0addge1  9286  nn0addge2  9287  nn0ge2m1nn  9300  nn0nndivcl  9302  xnn0xr  9308  nn0nepnf  9311  xnn0nemnf  9314  elnn0z  9330  elznn0nn  9331  ltsubnn0  9384  nn0negleid  9385  difgtsumgt  9386  nn0lt10b  9397  nn0ge0div  9404  xnn0lenn0nn0  9931  xnn0xadd0  9933  nn0fz0  10185  elfz0fzfz0  10192  fz0fzelfz0  10193  fz0fzdiffz0  10196  fzctr  10199  difelfzle  10200  difelfznle  10201  elfzo0le  10252  fzonmapblen  10254  fzofzim  10255  elfzodifsumelfzo  10268  fzonn0p1  10278  fzonn0p1p1  10280  elfzom1p1elfzo  10281  ubmelm1fzo  10293  fvinim0ffz  10308  subfzo0  10309  adddivflid  10361  divfl0  10365  flltdivnn0lt  10373  addmodid  10443  modfzo0difsn  10466  inftonninf  10513  bernneq  10731  bernneq3  10733  facwordi  10811  faclbnd  10812  faclbnd3  10814  faclbnd6  10815  facubnd  10816  facavg  10817  bcval4  10823  bcval5  10834  bcpasc  10837  fihashneq0  10865  dvdseq  11990  oddge22np1  12022  nn0ehalf  12044  nn0o  12048  nn0oddm1d2  12050  gcdn0gt0  12115  nn0gcdid0  12118  absmulgcd  12154  nn0seqcvgd  12179  algcvgblem  12187  algcvga  12189  lcmgcdnn  12220  prmfac1  12290  nonsq  12345  hashgcdlem  12376  odzdvds  12383  pcdvdsb  12458  pcidlem  12461  difsqpwdvds  12476  pcfaclem  12487  lgsdinn0  15164