Theorem nnnn0t 6106

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 6102	. 2 |- NN (_ NN0
2	1	sseli 2065	1 |- (A e. NN -> A e. NN0)

Syntax hints:   -> wi 3   e. wcel 958  NNcn 5296  NN0cn0 5297

This theorem is referenced by:  nnnn0 6107  dfn2 6112  nn0addclt 6120  nn0mulcl 6122  elnnnn0b 6173  elnnnn0c 6174  zltp1let 6181  nn0ind-raph 6214  quoremOLD 6252  expnnvalt 6572  expcllem 6575  expeq0t 6585  expge0t 6591  expgt1t 6592  expge1t 6593  expordit 6600  expnlbndt 6655  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 7499  infpnlem1 7506  infpnlem2 7507  bcthlem1 7999  bcthlem8 8006  bcthlem21 8019  ipcl 8365  ip1cnilem1 8373  ip1cnilem2 8374  ip1cnilem3 8375  ip1cnilem4 8376  ip1cnilem5 8377  ip1cnilem6 8378  sspival 8397  ipasslem3 8492  ipasslem4 8493

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-in 2051  df-ss 2053  df-n0 6100

Copyright terms: Public domain