Theorem nn0re 9572

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

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

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 9305  df-n0 9564

This theorem is used by:  nn0nlt0  9589  nn0le0eq0  9591  nn0p1gt0  9592  elnnnn0c  9608  nn0addge1  9609  nn0addge2  9610  nn0ge2m1nn  9627  nn0nndivcl  9629  xnn0xr  9635  nn0nepnf  9638  xnn0nemnf  9641  elnn0z  9657  elznn0nn  9658  ltsubnn0  9712  nn0negleid  9713  difgtsumgt  9714  nn0lt10b  9726  nn0ge0div  9733  xnn0lenn0nn0  10267  xnn0xadd0  10269  nn0fz0  10526  elfz0fzfz0  10533  fz0fzelfz0  10534  fz0fzdiffz0  10537  fzctr  10540  difelfzle  10541  difelfznle  10542  fzoun  10590  nn0p1elfzo  10594  elfzo0le  10597  fzonmapblen  10599  fzofzim  10600  elincfzoext  10611  elfzodifsumelfzo  10619  fzonn0p1  10629  fzonn0p1p1  10631  elfzom1p1elfzo  10632  ubmelm1fzo  10644  fvinim0ffz  10660  subfzo0  10661  adddivflid  10727  divfl0  10731  flltdivnn0lt  10739  addmodid  10809  modfzo0difsn  10832  inftonninf  10879  bernneq  11098  bernneq3  11100  facwordi  11178  faclbnd  11179  faclbnd3  11181  faclbnd6  11182  facubnd  11183  facavg  11184  bcval4  11190  bcval5  11201  bcpasc  11204  fihashneq0  11233  ccat0  11364  ccat2s1fvwd  11415  swrdsbslen  11438  swrdswrdlem  11476  swrdswrd  11477  swrdccatin1  11497  pfxccatin12lem2  11503  pfxccatin12lem3  11504  pfxccat3  11506  swrdccat  11507  swrdccat3blem  11511  nn0maxcl  11991  dvdseq  12615  oddge22np1  12648  nn0ehalf  12670  nn0o  12674  nn0oddm1d2  12676  bitsfi  12724  gcdn0gt0  12755  nn0gcdid0  12758  absmulgcd  12794  nn0seqcvgd  12819  algcvgblem  12827  algcvga  12829  lcmgcdnn  12860  prmfac1  12930  nonsq  12985  hashgcdlem  13016  odzdvds  13024  pcdvdsb  13099  pcidlem  13102  difsqpwdvds  13117  pcfaclem  13128  log2tlbndlog2  16082  birthdaylem3  16089  lgsdinn0  16167  2lgslem1c  16209  clwwlknonex2lem2  16679  eupth2lemsfi  16719  eupth2fi  16720