Theorem nn0re 9304

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

Syntax hints:   → wi 4   ∈ wcel 2176  ℝcr 7924  ℕ₀cn0 9295

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-sep 4162  ax-cnex 8016  ax-resscn 8017  ax-1re 8019  ax-addrcl 8022  ax-rnegex 8034

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-sn 3639  df-int 3886  df-inn 9037  df-n0 9296

This theorem is referenced by:  nn0nlt0  9321  nn0le0eq0  9323  nn0p1gt0  9324  elnnnn0c  9340  nn0addge1  9341  nn0addge2  9342  nn0ge2m1nn  9355  nn0nndivcl  9357  xnn0xr  9363  nn0nepnf  9366  xnn0nemnf  9369  elnn0z  9385  elznn0nn  9386  ltsubnn0  9440  nn0negleid  9441  difgtsumgt  9442  nn0lt10b  9453  nn0ge0div  9460  xnn0lenn0nn0  9987  xnn0xadd0  9989  nn0fz0  10241  elfz0fzfz0  10248  fz0fzelfz0  10249  fz0fzdiffz0  10252  fzctr  10255  difelfzle  10256  difelfznle  10257  elfzo0le  10309  fzonmapblen  10311  fzofzim  10312  elincfzoext  10322  elfzodifsumelfzo  10330  fzonn0p1  10340  fzonn0p1p1  10342  elfzom1p1elfzo  10343  ubmelm1fzo  10355  fvinim0ffz  10370  subfzo0  10371  adddivflid  10435  divfl0  10439  flltdivnn0lt  10447  addmodid  10517  modfzo0difsn  10540  inftonninf  10587  bernneq  10805  bernneq3  10807  facwordi  10885  faclbnd  10886  faclbnd3  10888  faclbnd6  10889  facubnd  10890  facavg  10891  bcval4  10897  bcval5  10908  bcpasc  10911  fihashneq0  10939  ccat0  11052  swrdsbslen  11119  nn0maxcl  11536  dvdseq  12159  oddge22np1  12192  nn0ehalf  12214  nn0o  12218  nn0oddm1d2  12220  bitsfi  12268  gcdn0gt0  12299  nn0gcdid0  12302  absmulgcd  12338  nn0seqcvgd  12363  algcvgblem  12371  algcvga  12373  lcmgcdnn  12404  prmfac1  12474  nonsq  12529  hashgcdlem  12560  odzdvds  12568  pcdvdsb  12643  pcidlem  12646  difsqpwdvds  12661  pcfaclem  12672  lgsdinn0  15525  2lgslem1c  15567