Theorem nn0re 9185

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℝcr 7810  ℕ₀cn0 9176

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4122  ax-cnex 7902  ax-resscn 7903  ax-1re 7905  ax-addrcl 7908  ax-rnegex 7920

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-sn 3599  df-int 3846  df-inn 8920  df-n0 9177

This theorem is referenced by:  nn0nlt0  9202  nn0le0eq0  9204  nn0p1gt0  9205  elnnnn0c  9221  nn0addge1  9222  nn0addge2  9223  nn0ge2m1nn  9236  nn0nndivcl  9238  xnn0xr  9244  nn0nepnf  9247  xnn0nemnf  9250  elnn0z  9266  elznn0nn  9267  ltsubnn0  9320  nn0negleid  9321  difgtsumgt  9322  nn0lt10b  9333  nn0ge0div  9340  xnn0lenn0nn0  9865  xnn0xadd0  9867  nn0fz0  10119  elfz0fzfz0  10126  fz0fzelfz0  10127  fz0fzdiffz0  10130  fzctr  10133  difelfzle  10134  difelfznle  10135  elfzo0le  10185  fzonmapblen  10187  fzofzim  10188  elfzodifsumelfzo  10201  fzonn0p1  10211  fzonn0p1p1  10213  elfzom1p1elfzo  10214  ubmelm1fzo  10226  fvinim0ffz  10241  subfzo0  10242  adddivflid  10292  divfl0  10296  flltdivnn0lt  10304  addmodid  10372  modfzo0difsn  10395  inftonninf  10441  bernneq  10641  bernneq3  10643  facwordi  10720  faclbnd  10721  faclbnd3  10723  faclbnd6  10724  facubnd  10725  facavg  10726  bcval4  10732  bcval5  10743  bcpasc  10746  fihashneq0  10774  dvdseq  11854  oddge22np1  11886  nn0ehalf  11908  nn0o  11912  nn0oddm1d2  11914  gcdn0gt0  11979  nn0gcdid0  11982  absmulgcd  12018  nn0seqcvgd  12041  algcvgblem  12049  algcvga  12051  lcmgcdnn  12082  prmfac1  12152  nonsq  12207  hashgcdlem  12238  odzdvds  12245  pcdvdsb  12319  pcidlem  12322  difsqpwdvds  12337  pcfaclem  12347  lgsdinn0  14452