Theorem nn0re 9454

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

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8074   NN0cn0 9445

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 8166  ax-resscn 8167  ax-1re 8169  ax-addrcl 8172  ax-rnegex 8184

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 9187  df-n0 9446

This theorem is referenced by:  nn0nlt0  9471  nn0le0eq0  9473  nn0p1gt0  9474  elnnnn0c  9490  nn0addge1  9491  nn0addge2  9492  nn0ge2m1nn  9505  nn0nndivcl  9507  xnn0xr  9513  nn0nepnf  9516  xnn0nemnf  9519  elnn0z  9535  elznn0nn  9536  ltsubnn0  9590  nn0negleid  9591  difgtsumgt  9592  nn0lt10b  9603  nn0ge0div  9610  xnn0lenn0nn0  10143  xnn0xadd0  10145  nn0fz0  10397  elfz0fzfz0  10404  fz0fzelfz0  10405  fz0fzdiffz0  10408  fzctr  10411  difelfzle  10412  difelfznle  10413  fzoun  10461  nn0p1elfzo  10465  elfzo0le  10468  fzonmapblen  10470  fzofzim  10471  elincfzoext  10482  elfzodifsumelfzo  10490  fzonn0p1  10500  fzonn0p1p1  10502  elfzom1p1elfzo  10503  ubmelm1fzo  10515  fvinim0ffz  10531  subfzo0  10532  adddivflid  10596  divfl0  10600  flltdivnn0lt  10608  addmodid  10678  modfzo0difsn  10701  inftonninf  10748  bernneq  10966  bernneq3  10968  facwordi  11046  faclbnd  11047  faclbnd3  11049  faclbnd6  11050  facubnd  11051  facavg  11052  bcval4  11058  bcval5  11069  bcpasc  11072  fihashneq0  11100  ccat0  11220  ccat2s1fvwd  11271  swrdsbslen  11294  swrdswrdlem  11332  swrdswrd  11333  swrdccatin1  11353  pfxccatin12lem2  11359  pfxccatin12lem3  11360  pfxccat3  11362  swrdccat  11363  swrdccat3blem  11367  nn0maxcl  11846  dvdseq  12470  oddge22np1  12503  nn0ehalf  12525  nn0o  12529  nn0oddm1d2  12531  bitsfi  12579  gcdn0gt0  12610  nn0gcdid0  12613  absmulgcd  12649  nn0seqcvgd  12674  algcvgblem  12682  algcvga  12684  lcmgcdnn  12715  prmfac1  12785  nonsq  12840  hashgcdlem  12871  odzdvds  12879  pcdvdsb  12954  pcidlem  12957  difsqpwdvds  12972  pcfaclem  12983  lgsdinn0  15844  2lgslem1c  15886  clwwlknonex2lem2  16356  eupth2lemsfi  16396  eupth2fi  16397