Theorem nn0re 9306

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

Syntax hints:   -> wi 4   e. wcel 2176   RRcr 7926   NN0cn0 9297

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-sep 4163  ax-cnex 8018  ax-resscn 8019  ax-1re 8021  ax-addrcl 8024  ax-rnegex 8036

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-sn 3639  df-int 3886  df-inn 9039  df-n0 9298

This theorem is referenced by:  nn0nlt0  9323  nn0le0eq0  9325  nn0p1gt0  9326  elnnnn0c  9342  nn0addge1  9343  nn0addge2  9344  nn0ge2m1nn  9357  nn0nndivcl  9359  xnn0xr  9365  nn0nepnf  9368  xnn0nemnf  9371  elnn0z  9387  elznn0nn  9388  ltsubnn0  9442  nn0negleid  9443  difgtsumgt  9444  nn0lt10b  9455  nn0ge0div  9462  xnn0lenn0nn0  9989  xnn0xadd0  9991  nn0fz0  10243  elfz0fzfz0  10250  fz0fzelfz0  10251  fz0fzdiffz0  10254  fzctr  10257  difelfzle  10258  difelfznle  10259  elfzo0le  10311  fzonmapblen  10313  fzofzim  10314  elincfzoext  10324  elfzodifsumelfzo  10332  fzonn0p1  10342  fzonn0p1p1  10344  elfzom1p1elfzo  10345  ubmelm1fzo  10357  fvinim0ffz  10372  subfzo0  10373  adddivflid  10437  divfl0  10441  flltdivnn0lt  10449  addmodid  10519  modfzo0difsn  10542  inftonninf  10589  bernneq  10807  bernneq3  10809  facwordi  10887  faclbnd  10888  faclbnd3  10890  faclbnd6  10891  facubnd  10892  facavg  10893  bcval4  10899  bcval5  10910  bcpasc  10913  fihashneq0  10941  ccat0  11055  swrdsbslen  11122  nn0maxcl  11569  dvdseq  12192  oddge22np1  12225  nn0ehalf  12247  nn0o  12251  nn0oddm1d2  12253  bitsfi  12301  gcdn0gt0  12332  nn0gcdid0  12335  absmulgcd  12371  nn0seqcvgd  12396  algcvgblem  12404  algcvga  12406  lcmgcdnn  12437  prmfac1  12507  nonsq  12562  hashgcdlem  12593  odzdvds  12601  pcdvdsb  12676  pcidlem  12679  difsqpwdvds  12694  pcfaclem  12705  lgsdinn0  15558  2lgslem1c  15600