Theorem nn0re 9583

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 9578	. 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 8184   NN0cn0 9574

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 4251  ax-cnex 8276  ax-resscn 8277  ax-1re 8279  ax-addrcl 8282  ax-rnegex 8294

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 9314  df-n0 9575

This theorem is used by:  nn0nlt0  9600  nn0le0eq0  9602  nn0p1gt0  9603  elnnnn0c  9619  nn0addge1  9620  nn0addge2  9621  nn0ge2m1nn  9638  nn0nndivcl  9640  xnn0xr  9646  nn0nepnf  9649  xnn0nemnf  9652  elnn0z  9668  elznn0nn  9669  ltsubnn0  9723  nn0negleid  9724  difgtsumgt  9725  nn0lt10b  9737  nn0ge0div  9744  xnn0lenn0nn0  10284  xnn0xadd0  10286  nn0fz0  10543  elfz0fzfz0  10550  fz0fzelfz0  10551  fz0fzdiffz0  10554  fzctr  10557  difelfzle  10558  difelfznle  10559  fzoun  10607  nn0p1elfzo  10611  elfzo0le  10614  fzonmapblen  10616  fzofzim  10617  elincfzoext  10628  elfzodifsumelfzo  10636  fzonn0p1  10646  fzonn0p1p1  10648  elfzom1p1elfzo  10649  ubmelm1fzo  10661  fvinim0ffz  10677  subfzo0  10678  adddivflid  10748  divfl0  10752  flltdivnn0lt  10760  addmodid  10830  modfzo0difsn  10853  inftonninf  10900  bernneq  11119  bernneq3  11121  facwordi  11200  faclbnd  11201  faclbnd3  11203  faclbnd6  11204  facubnd  11205  facavg  11206  bcval4  11212  bcval5  11223  bcpasc  11226  fihashneq0  11255  ccat0  11386  ccat2s1fvwd  11437  swrdsbslen  11460  swrdswrdlem  11498  swrdswrd  11499  swrdccatin1  11519  pfxccatin12lem2  11525  pfxccatin12lem3  11526  pfxccat3  11528  swrdccat  11529  swrdccat3blem  11533  nn0maxcl  12014  dvdseq  12640  oddge22np1  12673  nn0ehalf  12695  nn0o  12699  nn0oddm1d2  12701  bitsfi  12749  gcdn0gt0  12780  nn0gcdid0  12783  absmulgcd  12819  nn0seqcvgd  12844  algcvgblem  12852  algcvga  12854  lcmgcdnn  12885  prmfac1  12956  nonsq  13012  sqrtrirr  13014  hashgcdlem  13045  odzdvds  13053  pcdvdsb  13128  pcidlem  13131  difsqpwdvds  13146  pcfaclem  13157  gsumbagdiaglem  15175  psrridmfi  15200  log2tlbndlog2  16220  birthdaylem3  16227  bcmono  16304  bcmax  16305  lgsdinn0  16372  2lgslem1c  16414  clwwlknonex2lem2  16884  eupth2lemsfi  16924  eupth2fi  16925