Theorem 1nn0 8197

Description: 1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
1nn0	|- 1 e. NN0

Proof of Theorem 1nn0

Step	Hyp	Ref	Expression
1		1nn 7925	. 2 |- 1 e. NN
2	1	nnnn0i 8189	1 |- 1 e. NN0

Syntax hints:   e. wcel 1393   1c1 6890   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-1re 6978

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-v 2559  df-un 2922  df-in 2924  df-ss 2931  df-int 3616  df-inn 7915  df-n0 8182

This theorem is referenced by:  peano2nn0  8222  numsucc  8393  numadd  8401  numaddc  8402  6p5lem  8416  6p6e12  8418  7p5e12  8420  8p4e12  8424  9p2e11  8429  9p3e12  8430  10p10e20  8437  4t4e16  8440  5t4e20  8442  6t3e18  8445  6t4e24  8446  7t3e21  8450  7t4e28  8451  8t3e24  8456  9t3e27  8463  9t9e81  8469  nn01to3  8552  elfzom1elp1fzo  9058  fzo0sn0fzo1  9077  expn1ap0  9265  nn0expcl  9269  sqval  9312