Theorem nn0re 9470

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

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8091   NN0cn0 9461

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 2213  ax-sep 4212  ax-cnex 8183  ax-resscn 8184  ax-1re 8186  ax-addrcl 8189  ax-rnegex 8201

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-int 3934  df-inn 9203  df-n0 9462

This theorem is referenced by:  nn0nlt0  9487  nn0le0eq0  9489  nn0p1gt0  9490  elnnnn0c  9506  nn0addge1  9507  nn0addge2  9508  nn0ge2m1nn  9523  nn0nndivcl  9525  xnn0xr  9531  nn0nepnf  9534  xnn0nemnf  9537  elnn0z  9553  elznn0nn  9554  ltsubnn0  9608  nn0negleid  9609  difgtsumgt  9610  nn0lt10b  9621  nn0ge0div  9628  xnn0lenn0nn0  10161  xnn0xadd0  10163  nn0fz0  10416  elfz0fzfz0  10423  fz0fzelfz0  10424  fz0fzdiffz0  10427  fzctr  10430  difelfzle  10431  difelfznle  10432  fzoun  10480  nn0p1elfzo  10484  elfzo0le  10487  fzonmapblen  10489  fzofzim  10490  elincfzoext  10501  elfzodifsumelfzo  10509  fzonn0p1  10519  fzonn0p1p1  10521  elfzom1p1elfzo  10522  ubmelm1fzo  10534  fvinim0ffz  10550  subfzo0  10551  adddivflid  10615  divfl0  10619  flltdivnn0lt  10627  addmodid  10697  modfzo0difsn  10720  inftonninf  10767  bernneq  10985  bernneq3  10987  facwordi  11065  faclbnd  11066  faclbnd3  11068  faclbnd6  11069  facubnd  11070  facavg  11071  bcval4  11077  bcval5  11088  bcpasc  11091  fihashneq0  11119  ccat0  11239  ccat2s1fvwd  11290  swrdsbslen  11313  swrdswrdlem  11351  swrdswrd  11352  swrdccatin1  11372  pfxccatin12lem2  11378  pfxccatin12lem3  11379  pfxccat3  11381  swrdccat  11382  swrdccat3blem  11386  nn0maxcl  11865  dvdseq  12489  oddge22np1  12522  nn0ehalf  12544  nn0o  12548  nn0oddm1d2  12550  bitsfi  12598  gcdn0gt0  12629  nn0gcdid0  12632  absmulgcd  12668  nn0seqcvgd  12693  algcvgblem  12701  algcvga  12703  lcmgcdnn  12734  prmfac1  12804  nonsq  12859  hashgcdlem  12890  odzdvds  12898  pcdvdsb  12973  pcidlem  12976  difsqpwdvds  12991  pcfaclem  13002  lgsdinn0  15867  2lgslem1c  15909  clwwlknonex2lem2  16379  eupth2lemsfi  16419  eupth2fi  16420