Theorem nn0re 9401

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8021  ℕ₀cn0 9392

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4205  ax-cnex 8113  ax-resscn 8114  ax-1re 8116  ax-addrcl 8119  ax-rnegex 8131

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-sn 3673  df-int 3927  df-inn 9134  df-n0 9393

This theorem is referenced by:  nn0nlt0  9418  nn0le0eq0  9420  nn0p1gt0  9421  elnnnn0c  9437  nn0addge1  9438  nn0addge2  9439  nn0ge2m1nn  9452  nn0nndivcl  9454  xnn0xr  9460  nn0nepnf  9463  xnn0nemnf  9466  elnn0z  9482  elznn0nn  9483  ltsubnn0  9537  nn0negleid  9538  difgtsumgt  9539  nn0lt10b  9550  nn0ge0div  9557  xnn0lenn0nn0  10090  xnn0xadd0  10092  nn0fz0  10344  elfz0fzfz0  10351  fz0fzelfz0  10352  fz0fzdiffz0  10355  fzctr  10358  difelfzle  10359  difelfznle  10360  fzoun  10408  elfzo0le  10414  fzonmapblen  10416  fzofzim  10417  elincfzoext  10428  elfzodifsumelfzo  10436  fzonn0p1  10446  fzonn0p1p1  10448  elfzom1p1elfzo  10449  ubmelm1fzo  10461  fvinim0ffz  10477  subfzo0  10478  adddivflid  10542  divfl0  10546  flltdivnn0lt  10554  addmodid  10624  modfzo0difsn  10647  inftonninf  10694  bernneq  10912  bernneq3  10914  facwordi  10992  faclbnd  10993  faclbnd3  10995  faclbnd6  10996  facubnd  10997  facavg  10998  bcval4  11004  bcval5  11015  bcpasc  11018  fihashneq0  11046  ccat0  11163  ccat2s1fvwd  11214  swrdsbslen  11237  swrdswrdlem  11275  swrdswrd  11276  swrdccatin1  11296  pfxccatin12lem2  11302  pfxccatin12lem3  11303  pfxccat3  11305  swrdccat  11306  swrdccat3blem  11310  nn0maxcl  11776  dvdseq  12399  oddge22np1  12432  nn0ehalf  12454  nn0o  12458  nn0oddm1d2  12460  bitsfi  12508  gcdn0gt0  12539  nn0gcdid0  12542  absmulgcd  12578  nn0seqcvgd  12603  algcvgblem  12611  algcvga  12613  lcmgcdnn  12644  prmfac1  12714  nonsq  12769  hashgcdlem  12800  odzdvds  12808  pcdvdsb  12883  pcidlem  12886  difsqpwdvds  12901  pcfaclem  12912  lgsdinn0  15767  2lgslem1c  15809  clwwlknonex2lem2  16233