Theorem nn0re 9507

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

Syntax hints:   -> wi 4   e. wcel 2205   RRcr 8128   NN0cn0 9498

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 2216  ax-sep 4230  ax-cnex 8220  ax-resscn 8221  ax-1re 8223  ax-addrcl 8226  ax-rnegex 8238

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3217  df-in 3219  df-ss 3226  df-sn 3697  df-int 3952  df-inn 9240  df-n0 9499

This theorem is referenced by:  nn0nlt0  9524  nn0le0eq0  9526  nn0p1gt0  9527  elnnnn0c  9543  nn0addge1  9544  nn0addge2  9545  nn0ge2m1nn  9562  nn0nndivcl  9564  xnn0xr  9570  nn0nepnf  9573  xnn0nemnf  9576  elnn0z  9592  elznn0nn  9593  ltsubnn0  9647  nn0negleid  9648  difgtsumgt  9649  nn0lt10b  9661  nn0ge0div  9668  xnn0lenn0nn0  10201  xnn0xadd0  10203  nn0fz0  10457  elfz0fzfz0  10464  fz0fzelfz0  10465  fz0fzdiffz0  10468  fzctr  10471  difelfzle  10472  difelfznle  10473  fzoun  10521  nn0p1elfzo  10525  elfzo0le  10528  fzonmapblen  10530  fzofzim  10531  elincfzoext  10542  elfzodifsumelfzo  10550  fzonn0p1  10560  fzonn0p1p1  10562  elfzom1p1elfzo  10563  ubmelm1fzo  10575  fvinim0ffz  10591  subfzo0  10592  adddivflid  10656  divfl0  10660  flltdivnn0lt  10668  addmodid  10738  modfzo0difsn  10761  inftonninf  10808  bernneq  11026  bernneq3  11028  facwordi  11106  faclbnd  11107  faclbnd3  11109  faclbnd6  11110  facubnd  11111  facavg  11112  bcval4  11118  bcval5  11129  bcpasc  11132  fihashneq0  11161  ccat0  11288  ccat2s1fvwd  11339  swrdsbslen  11362  swrdswrdlem  11400  swrdswrd  11401  swrdccatin1  11421  pfxccatin12lem2  11427  pfxccatin12lem3  11428  pfxccat3  11430  swrdccat  11431  swrdccat3blem  11435  nn0maxcl  11914  dvdseq  12538  oddge22np1  12571  nn0ehalf  12593  nn0o  12597  nn0oddm1d2  12599  bitsfi  12647  gcdn0gt0  12678  nn0gcdid0  12681  absmulgcd  12717  nn0seqcvgd  12742  algcvgblem  12750  algcvga  12752  lcmgcdnn  12783  prmfac1  12853  nonsq  12908  hashgcdlem  12939  odzdvds  12947  pcdvdsb  13022  pcidlem  13025  difsqpwdvds  13040  pcfaclem  13051  lgsdinn0  15938  2lgslem1c  15980  clwwlknonex2lem2  16450  eupth2lemsfi  16490  eupth2fi  16491