Theorem nn0re 9378

Description: A nonnegative integer is a real number. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nn0re	|- ( A e. NN0 -> A e. RR )

Proof of Theorem nn0re

Step	Hyp	Ref	Expression
1		nn0ssre 9373	. 2 |- NN0 C_ RR
2	1	sseli 3220	1 |- ( A e. NN0 -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 7998   NN0cn0 9369

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 4202  ax-cnex 8090  ax-resscn 8091  ax-1re 8093  ax-addrcl 8096  ax-rnegex 8108

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 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-int 3924  df-inn 9111  df-n0 9370

This theorem is referenced by:  nn0nlt0  9395  nn0le0eq0  9397  nn0p1gt0  9398  elnnnn0c  9414  nn0addge1  9415  nn0addge2  9416  nn0ge2m1nn  9429  nn0nndivcl  9431  xnn0xr  9437  nn0nepnf  9440  xnn0nemnf  9443  elnn0z  9459  elznn0nn  9460  ltsubnn0  9514  nn0negleid  9515  difgtsumgt  9516  nn0lt10b  9527  nn0ge0div  9534  xnn0lenn0nn0  10061  xnn0xadd0  10063  nn0fz0  10315  elfz0fzfz0  10322  fz0fzelfz0  10323  fz0fzdiffz0  10326  fzctr  10329  difelfzle  10330  difelfznle  10331  fzoun  10379  elfzo0le  10385  fzonmapblen  10387  fzofzim  10388  elincfzoext  10399  elfzodifsumelfzo  10407  fzonn0p1  10417  fzonn0p1p1  10419  elfzom1p1elfzo  10420  ubmelm1fzo  10432  fvinim0ffz  10447  subfzo0  10448  adddivflid  10512  divfl0  10516  flltdivnn0lt  10524  addmodid  10594  modfzo0difsn  10617  inftonninf  10664  bernneq  10882  bernneq3  10884  facwordi  10962  faclbnd  10963  faclbnd3  10965  faclbnd6  10966  facubnd  10967  facavg  10968  bcval4  10974  bcval5  10985  bcpasc  10988  fihashneq0  11016  ccat0  11131  swrdsbslen  11198  swrdswrdlem  11236  swrdswrd  11237  swrdccatin1  11257  pfxccatin12lem2  11263  pfxccatin12lem3  11264  pfxccat3  11266  swrdccat  11267  swrdccat3blem  11271  nn0maxcl  11736  dvdseq  12359  oddge22np1  12392  nn0ehalf  12414  nn0o  12418  nn0oddm1d2  12420  bitsfi  12468  gcdn0gt0  12499  nn0gcdid0  12502  absmulgcd  12538  nn0seqcvgd  12563  algcvgblem  12571  algcvga  12573  lcmgcdnn  12604  prmfac1  12674  nonsq  12729  hashgcdlem  12760  odzdvds  12768  pcdvdsb  12843  pcidlem  12846  difsqpwdvds  12861  pcfaclem  12872  lgsdinn0  15727  2lgslem1c  15769