Theorem nn0re 9505

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℝcr 8126  ℕ₀cn0 9496

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 2214  ax-sep 4228  ax-cnex 8218  ax-resscn 8219  ax-1re 8221  ax-addrcl 8224  ax-rnegex 8236

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-sn 3695  df-int 3950  df-inn 9238  df-n0 9497

This theorem is referenced by:  nn0nlt0  9522  nn0le0eq0  9524  nn0p1gt0  9525  elnnnn0c  9541  nn0addge1  9542  nn0addge2  9543  nn0ge2m1nn  9560  nn0nndivcl  9562  xnn0xr  9568  nn0nepnf  9571  xnn0nemnf  9574  elnn0z  9590  elznn0nn  9591  ltsubnn0  9645  nn0negleid  9646  difgtsumgt  9647  nn0lt10b  9658  nn0ge0div  9665  xnn0lenn0nn0  10198  xnn0xadd0  10200  nn0fz0  10453  elfz0fzfz0  10460  fz0fzelfz0  10461  fz0fzdiffz0  10464  fzctr  10467  difelfzle  10468  difelfznle  10469  fzoun  10517  nn0p1elfzo  10521  elfzo0le  10524  fzonmapblen  10526  fzofzim  10527  elincfzoext  10538  elfzodifsumelfzo  10546  fzonn0p1  10556  fzonn0p1p1  10558  elfzom1p1elfzo  10559  ubmelm1fzo  10571  fvinim0ffz  10587  subfzo0  10588  adddivflid  10652  divfl0  10656  flltdivnn0lt  10664  addmodid  10734  modfzo0difsn  10757  inftonninf  10804  bernneq  11022  bernneq3  11024  facwordi  11102  faclbnd  11103  faclbnd3  11105  faclbnd6  11106  facubnd  11107  facavg  11108  bcval4  11114  bcval5  11125  bcpasc  11128  fihashneq0  11157  ccat0  11284  ccat2s1fvwd  11335  swrdsbslen  11358  swrdswrdlem  11396  swrdswrd  11397  swrdccatin1  11417  pfxccatin12lem2  11423  pfxccatin12lem3  11424  pfxccat3  11426  swrdccat  11427  swrdccat3blem  11431  nn0maxcl  11910  dvdseq  12534  oddge22np1  12567  nn0ehalf  12589  nn0o  12593  nn0oddm1d2  12595  bitsfi  12643  gcdn0gt0  12674  nn0gcdid0  12677  absmulgcd  12713  nn0seqcvgd  12738  algcvgblem  12746  algcvga  12748  lcmgcdnn  12779  prmfac1  12849  nonsq  12904  hashgcdlem  12935  odzdvds  12943  pcdvdsb  13018  pcidlem  13021  difsqpwdvds  13036  pcfaclem  13047  lgsdinn0  15921  2lgslem1c  15963  clwwlknonex2lem2  16433  eupth2lemsfi  16473  eupth2fi  16474