Theorem nn0re 9577

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   RRcr 8179   NN0cn0 9568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4249  ax-cnex 8271  ax-resscn 8272  ax-1re 8274  ax-addrcl 8277  ax-rnegex 8289

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-int 3971  df-inn 9308  df-n0 9569

This theorem is used by:  nn0nlt0  9594  nn0le0eq0  9596  nn0p1gt0  9597  elnnnn0c  9613  nn0addge1  9614  nn0addge2  9615  nn0ge2m1nn  9632  nn0nndivcl  9634  xnn0xr  9640  nn0nepnf  9643  xnn0nemnf  9646  elnn0z  9662  elznn0nn  9663  ltsubnn0  9717  nn0negleid  9718  difgtsumgt  9719  nn0lt10b  9731  nn0ge0div  9738  xnn0lenn0nn0  10278  xnn0xadd0  10280  nn0fz0  10537  elfz0fzfz0  10544  fz0fzelfz0  10545  fz0fzdiffz0  10548  fzctr  10551  difelfzle  10552  difelfznle  10553  fzoun  10601  nn0p1elfzo  10605  elfzo0le  10608  fzonmapblen  10610  fzofzim  10611  elincfzoext  10622  elfzodifsumelfzo  10630  fzonn0p1  10640  fzonn0p1p1  10642  elfzom1p1elfzo  10643  ubmelm1fzo  10655  fvinim0ffz  10671  subfzo0  10672  adddivflid  10742  divfl0  10746  flltdivnn0lt  10754  addmodid  10824  modfzo0difsn  10847  inftonninf  10894  bernneq  11113  bernneq3  11115  facwordi  11194  faclbnd  11195  faclbnd3  11197  faclbnd6  11198  facubnd  11199  facavg  11200  bcval4  11206  bcval5  11217  bcpasc  11220  fihashneq0  11249  ccat0  11380  ccat2s1fvwd  11431  swrdsbslen  11454  swrdswrdlem  11492  swrdswrd  11493  swrdccatin1  11513  pfxccatin12lem2  11519  pfxccatin12lem3  11520  pfxccat3  11522  swrdccat  11523  swrdccat3blem  11527  nn0maxcl  12008  dvdseq  12634  oddge22np1  12667  nn0ehalf  12689  nn0o  12693  nn0oddm1d2  12695  bitsfi  12743  gcdn0gt0  12774  nn0gcdid0  12777  absmulgcd  12813  nn0seqcvgd  12838  algcvgblem  12846  algcvga  12848  lcmgcdnn  12879  prmfac1  12950  nonsq  13006  sqrtrirr  13008  hashgcdlem  13039  odzdvds  13047  pcdvdsb  13122  pcidlem  13125  difsqpwdvds  13140  pcfaclem  13151  log2tlbndlog2  16181  birthdaylem3  16188  bcmono  16265  bcmax  16266  lgsdinn0  16333  2lgslem1c  16375  clwwlknonex2lem2  16845  eupth2lemsfi  16885  eupth2fi  16886