Theorem nnnn0t 6108

Description: A natural number is a nonnegative integer.

Assertion

Ref	Expression
nnnn0t	|- (A e. NN -> A e. NN0)

Proof of Theorem nnnn0t

Step	Hyp	Ref	Expression
1		nnssnn0 6104	. 2 |- NN (_ NN0
2	1	sseli 2068	1 |- (A e. NN -> A e. NN0)

Syntax hints:   -> wi 3   e. wcel 960  NNcn 5308  NN0cn0 5309

This theorem is referenced by:  nnnn0 6109  dfn2 6114  nn0addclt 6122  nn0mulcl 6124  elnnnn0b 6175  elnnnn0c 6176  zltp1let 6183  nn0ind-raph 6216  expnnvalt 6573  expcllem 6576  expeq0t 6586  expge0t 6592  expgt1t 6593  expge1t 6594  expordit 6601  expnlbndt 6656  facdivt 6942  facwordit 6944  faclbnd 6945  faclbnd3 6947  faclbnd4lem3 6950  faclbnd4lem4 6951  faclbnd5 6953  faclbnd6 6954  facavgt 6955  bccl2t 6971  bcclt 6972  ser1ser0 7048  binomlem1 7066  binomlem2 7067  binomlem3 7068  binomlem5 7070  binomlem6 7071  bcxmas 7076  climubi 7153  isumnn0nna 7208  fnsmnt 7226  expcnvlem2 7228  expcnv 7233  geolimilem 7235  geoisum1c 7245  0.999... 7246  cvgratlem1ALT 7247  cvgratlem2ALT 7248  cvgratlem1 7250  cvgratlem2 7251  cvgratlem5 7254  efcltlem1 7304  efcltlem2 7305  dfef2 7307  efseq0ex 7311  erelem1 7319  erelem2 7320  erelem3 7321  erelem6 7324  efaddlem3 7340  efaddlem6 7343  efaddlem9 7346  efaddlem15 7352  efaddlem17 7354  efaddlem19 7356  efaddlem27 7364  eftlubclt 7376  reeftlclt 7380  abspef01tlub 7395  absefm1le 7412  xpnnen 7500  infpnlem1 7507  infpnlem2 7508  bcthlem1 7996  bcthlem8 8003  bcthlem21 8016  ipcl 8361  ip1cnilem1 8369  ip1cnilem2 8370  ip1cnilem3 8371  ip1cnilem4 8372  ip1cnilem5 8373  ip1cnilem6 8374  sspival 8393  ipasslem3 8488  ipasslem4 8489

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-un 2053  df-in 2054  df-ss 2056  df-n0 6102

Copyright terms: Public domain