Theorem nn0re 9187

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

Syntax hints:   -> wi 4   e. wcel 2148   RRcr 7812   NN0cn0 9178

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4123  ax-cnex 7904  ax-resscn 7905  ax-1re 7907  ax-addrcl 7910  ax-rnegex 7922

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-sn 3600  df-int 3847  df-inn 8922  df-n0 9179

This theorem is referenced by:  nn0nlt0  9204  nn0le0eq0  9206  nn0p1gt0  9207  elnnnn0c  9223  nn0addge1  9224  nn0addge2  9225  nn0ge2m1nn  9238  nn0nndivcl  9240  xnn0xr  9246  nn0nepnf  9249  xnn0nemnf  9252  elnn0z  9268  elznn0nn  9269  ltsubnn0  9322  nn0negleid  9323  difgtsumgt  9324  nn0lt10b  9335  nn0ge0div  9342  xnn0lenn0nn0  9867  xnn0xadd0  9869  nn0fz0  10121  elfz0fzfz0  10128  fz0fzelfz0  10129  fz0fzdiffz0  10132  fzctr  10135  difelfzle  10136  difelfznle  10137  elfzo0le  10187  fzonmapblen  10189  fzofzim  10190  elfzodifsumelfzo  10203  fzonn0p1  10213  fzonn0p1p1  10215  elfzom1p1elfzo  10216  ubmelm1fzo  10228  fvinim0ffz  10243  subfzo0  10244  adddivflid  10294  divfl0  10298  flltdivnn0lt  10306  addmodid  10374  modfzo0difsn  10397  inftonninf  10443  bernneq  10643  bernneq3  10645  facwordi  10722  faclbnd  10723  faclbnd3  10725  faclbnd6  10726  facubnd  10727  facavg  10728  bcval4  10734  bcval5  10745  bcpasc  10748  fihashneq0  10776  dvdseq  11856  oddge22np1  11888  nn0ehalf  11910  nn0o  11914  nn0oddm1d2  11916  gcdn0gt0  11981  nn0gcdid0  11984  absmulgcd  12020  nn0seqcvgd  12043  algcvgblem  12051  algcvga  12053  lcmgcdnn  12084  prmfac1  12154  nonsq  12209  hashgcdlem  12240  odzdvds  12247  pcdvdsb  12321  pcidlem  12324  difsqpwdvds  12339  pcfaclem  12349  lgsdinn0  14488