Theorem nn0re 9522

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℝcr 8142  ℕ₀cn0 9513

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-sep 4233  ax-cnex 8234  ax-resscn 8235  ax-1re 8237  ax-addrcl 8240  ax-rnegex 8252

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-sn 3700  df-int 3955  df-inn 9255  df-n0 9514

This theorem is referenced by:  nn0nlt0  9539  nn0le0eq0  9541  nn0p1gt0  9542  elnnnn0c  9558  nn0addge1  9559  nn0addge2  9560  nn0ge2m1nn  9577  nn0nndivcl  9579  xnn0xr  9585  nn0nepnf  9588  xnn0nemnf  9591  elnn0z  9607  elznn0nn  9608  ltsubnn0  9662  nn0negleid  9663  difgtsumgt  9664  nn0lt10b  9676  nn0ge0div  9683  xnn0lenn0nn0  10217  xnn0xadd0  10219  nn0fz0  10475  elfz0fzfz0  10482  fz0fzelfz0  10483  fz0fzdiffz0  10486  fzctr  10489  difelfzle  10490  difelfznle  10491  fzoun  10539  nn0p1elfzo  10543  elfzo0le  10546  fzonmapblen  10548  fzofzim  10549  elincfzoext  10560  elfzodifsumelfzo  10568  fzonn0p1  10578  fzonn0p1p1  10580  elfzom1p1elfzo  10581  ubmelm1fzo  10593  fvinim0ffz  10609  subfzo0  10610  adddivflid  10676  divfl0  10680  flltdivnn0lt  10688  addmodid  10758  modfzo0difsn  10781  inftonninf  10828  bernneq  11047  bernneq3  11049  facwordi  11127  faclbnd  11128  faclbnd3  11130  faclbnd6  11131  facubnd  11132  facavg  11133  bcval4  11139  bcval5  11150  bcpasc  11153  fihashneq0  11182  ccat0  11309  ccat2s1fvwd  11360  swrdsbslen  11383  swrdswrdlem  11421  swrdswrd  11422  swrdccatin1  11442  pfxccatin12lem2  11448  pfxccatin12lem3  11449  pfxccat3  11451  swrdccat  11452  swrdccat3blem  11456  nn0maxcl  11935  dvdseq  12559  oddge22np1  12592  nn0ehalf  12614  nn0o  12618  nn0oddm1d2  12620  bitsfi  12668  gcdn0gt0  12699  nn0gcdid0  12702  absmulgcd  12738  nn0seqcvgd  12763  algcvgblem  12771  algcvga  12773  lcmgcdnn  12804  prmfac1  12874  nonsq  12929  hashgcdlem  12960  odzdvds  12968  pcdvdsb  13043  pcidlem  13046  difsqpwdvds  13061  pcfaclem  13072  lgsdinn0  16047  2lgslem1c  16089  clwwlknonex2lem2  16559  eupth2lemsfi  16599  eupth2fi  16600