Theorem nn0re 9389

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 9384	. 2 |- NN0 C_ RR
2	1	sseli 3220	1 |- ( A e. NN0 -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 8009   NN0cn0 9380

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 8101  ax-resscn 8102  ax-1re 8104  ax-addrcl 8107  ax-rnegex 8119

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 9122  df-n0 9381

This theorem is referenced by:  nn0nlt0  9406  nn0le0eq0  9408  nn0p1gt0  9409  elnnnn0c  9425  nn0addge1  9426  nn0addge2  9427  nn0ge2m1nn  9440  nn0nndivcl  9442  xnn0xr  9448  nn0nepnf  9451  xnn0nemnf  9454  elnn0z  9470  elznn0nn  9471  ltsubnn0  9525  nn0negleid  9526  difgtsumgt  9527  nn0lt10b  9538  nn0ge0div  9545  xnn0lenn0nn0  10073  xnn0xadd0  10075  nn0fz0  10327  elfz0fzfz0  10334  fz0fzelfz0  10335  fz0fzdiffz0  10338  fzctr  10341  difelfzle  10342  difelfznle  10343  fzoun  10391  elfzo0le  10397  fzonmapblen  10399  fzofzim  10400  elincfzoext  10411  elfzodifsumelfzo  10419  fzonn0p1  10429  fzonn0p1p1  10431  elfzom1p1elfzo  10432  ubmelm1fzo  10444  fvinim0ffz  10459  subfzo0  10460  adddivflid  10524  divfl0  10528  flltdivnn0lt  10536  addmodid  10606  modfzo0difsn  10629  inftonninf  10676  bernneq  10894  bernneq3  10896  facwordi  10974  faclbnd  10975  faclbnd3  10977  faclbnd6  10978  facubnd  10979  facavg  10980  bcval4  10986  bcval5  10997  bcpasc  11000  fihashneq0  11028  ccat0  11144  swrdsbslen  11214  swrdswrdlem  11252  swrdswrd  11253  swrdccatin1  11273  pfxccatin12lem2  11279  pfxccatin12lem3  11280  pfxccat3  11282  swrdccat  11283  swrdccat3blem  11287  nn0maxcl  11752  dvdseq  12375  oddge22np1  12408  nn0ehalf  12430  nn0o  12434  nn0oddm1d2  12436  bitsfi  12484  gcdn0gt0  12515  nn0gcdid0  12518  absmulgcd  12554  nn0seqcvgd  12579  algcvgblem  12587  algcvga  12589  lcmgcdnn  12620  prmfac1  12690  nonsq  12745  hashgcdlem  12776  odzdvds  12784  pcdvdsb  12859  pcidlem  12862  difsqpwdvds  12877  pcfaclem  12888  lgsdinn0  15743  2lgslem1c  15785