Theorem nn0re 9339

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

Syntax hints:   -> wi 4   e. wcel 2178   RRcr 7959   NN0cn0 9330

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-sep 4178  ax-cnex 8051  ax-resscn 8052  ax-1re 8054  ax-addrcl 8057  ax-rnegex 8069

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-sn 3649  df-int 3900  df-inn 9072  df-n0 9331

This theorem is referenced by:  nn0nlt0  9356  nn0le0eq0  9358  nn0p1gt0  9359  elnnnn0c  9375  nn0addge1  9376  nn0addge2  9377  nn0ge2m1nn  9390  nn0nndivcl  9392  xnn0xr  9398  nn0nepnf  9401  xnn0nemnf  9404  elnn0z  9420  elznn0nn  9421  ltsubnn0  9475  nn0negleid  9476  difgtsumgt  9477  nn0lt10b  9488  nn0ge0div  9495  xnn0lenn0nn0  10022  xnn0xadd0  10024  nn0fz0  10276  elfz0fzfz0  10283  fz0fzelfz0  10284  fz0fzdiffz0  10287  fzctr  10290  difelfzle  10291  difelfznle  10292  fzoun  10340  elfzo0le  10346  fzonmapblen  10348  fzofzim  10349  elincfzoext  10359  elfzodifsumelfzo  10367  fzonn0p1  10377  fzonn0p1p1  10379  elfzom1p1elfzo  10380  ubmelm1fzo  10392  fvinim0ffz  10407  subfzo0  10408  adddivflid  10472  divfl0  10476  flltdivnn0lt  10484  addmodid  10554  modfzo0difsn  10577  inftonninf  10624  bernneq  10842  bernneq3  10844  facwordi  10922  faclbnd  10923  faclbnd3  10925  faclbnd6  10926  facubnd  10927  facavg  10928  bcval4  10934  bcval5  10945  bcpasc  10948  fihashneq0  10976  ccat0  11090  swrdsbslen  11157  swrdswrdlem  11195  swrdswrd  11196  swrdccatin1  11216  pfxccatin12lem2  11222  pfxccatin12lem3  11223  pfxccat3  11225  swrdccat  11226  swrdccat3blem  11230  nn0maxcl  11651  dvdseq  12274  oddge22np1  12307  nn0ehalf  12329  nn0o  12333  nn0oddm1d2  12335  bitsfi  12383  gcdn0gt0  12414  nn0gcdid0  12417  absmulgcd  12453  nn0seqcvgd  12478  algcvgblem  12486  algcvga  12488  lcmgcdnn  12519  prmfac1  12589  nonsq  12644  hashgcdlem  12675  odzdvds  12683  pcdvdsb  12758  pcidlem  12761  difsqpwdvds  12776  pcfaclem  12787  lgsdinn0  15640  2lgslem1c  15682