Theorem nn0re 9576

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℝcr 8178  ℕ₀cn0 9567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4249  ax-cnex 8270  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276  ax-rnegex 8288

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-int 3971  df-inn 9307  df-n0 9568

This theorem is used by:  nn0nlt0  9593  nn0le0eq0  9595  nn0p1gt0  9596  elnnnn0c  9612  nn0addge1  9613  nn0addge2  9614  nn0ge2m1nn  9631  nn0nndivcl  9633  xnn0xr  9639  nn0nepnf  9642  xnn0nemnf  9645  elnn0z  9661  elznn0nn  9662  ltsubnn0  9716  nn0negleid  9717  difgtsumgt  9718  nn0lt10b  9730  nn0ge0div  9737  xnn0lenn0nn0  10277  xnn0xadd0  10279  nn0fz0  10536  elfz0fzfz0  10543  fz0fzelfz0  10544  fz0fzdiffz0  10547  fzctr  10550  difelfzle  10551  difelfznle  10552  fzoun  10600  nn0p1elfzo  10604  elfzo0le  10607  fzonmapblen  10609  fzofzim  10610  elincfzoext  10621  elfzodifsumelfzo  10629  fzonn0p1  10639  fzonn0p1p1  10641  elfzom1p1elfzo  10642  ubmelm1fzo  10654  fvinim0ffz  10670  subfzo0  10671  adddivflid  10740  divfl0  10744  flltdivnn0lt  10752  addmodid  10822  modfzo0difsn  10845  inftonninf  10892  bernneq  11111  bernneq3  11113  facwordi  11192  faclbnd  11193  faclbnd3  11195  faclbnd6  11196  facubnd  11197  facavg  11198  bcval4  11204  bcval5  11215  bcpasc  11218  fihashneq0  11247  ccat0  11378  ccat2s1fvwd  11429  swrdsbslen  11452  swrdswrdlem  11490  swrdswrd  11491  swrdccatin1  11511  pfxccatin12lem2  11517  pfxccatin12lem3  11518  pfxccat3  11520  swrdccat  11521  swrdccat3blem  11525  nn0maxcl  12006  dvdseq  12631  oddge22np1  12664  nn0ehalf  12686  nn0o  12690  nn0oddm1d2  12692  bitsfi  12740  gcdn0gt0  12771  nn0gcdid0  12774  absmulgcd  12810  nn0seqcvgd  12835  algcvgblem  12843  algcvga  12845  lcmgcdnn  12876  prmfac1  12947  nonsq  13003  sqrtrirr  13005  hashgcdlem  13036  odzdvds  13044  pcdvdsb  13119  pcidlem  13122  difsqpwdvds  13137  pcfaclem  13148  log2tlbndlog2  16139  birthdaylem3  16146  bcmono  16202  bcmax  16203  lgsdinn0  16265  2lgslem1c  16307  clwwlknonex2lem2  16777  eupth2lemsfi  16817  eupth2fi  16818