Theorem nn0re 8190

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

Syntax hints:   -> wi 4   e. wcel 1393   RRcr 6888   NN0cn0 8181

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-cnex 6975  ax-resscn 6976  ax-1re 6978  ax-addrcl 6981  ax-rnegex 6993

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-v 2559  df-un 2922  df-in 2924  df-ss 2931  df-sn 3381  df-int 3616  df-inn 7915  df-n0 8182

This theorem is referenced by:  nn0nlt0  8208  nn0le0eq0  8210  nn0p1gt0  8211  elnnnn0c  8227  nn0addge1  8228  nn0addge2  8229  nn0ge2m1nn  8242  nn0nndivcl  8244  elnn0z  8258  elznn0nn  8259  nn0lt10b  8321  nn0ge0div  8327  nn0fz0  8978  elfz0addOLD  8980  elfz0fzfz0  8983  fz0fzelfz0  8984  fz0fzdiffz0  8987  fzctr  8991  difelfzle  8992  difelfznle  8993  elfzo0le  9041  fzonmapblen  9043  fzofzim  9044  elfzodifsumelfzo  9057  fzonn0p1  9067  fzonn0p1p1  9069  elfzom1p1elfzo  9070  ubmelm1fzo  9082  fvinim0ffz  9096  subfzo0  9097  adddivflid  9134  divfl0  9138  flltdivnn0lt  9146  bernneq  9369  bernneq3  9371  nn0seqcvgd  9880  algcvgblem  9888  ialgcvga  9890