Theorem 4nn0 9198

Description: 4 is a nonnegative integer. (Contributed by Mario Carneiro, 18-Feb-2014.)

Assertion

Ref	Expression
4nn0	|- 4 e. NN0

Proof of Theorem 4nn0

Step	Hyp	Ref	Expression
1		4nn 9085	. 2 |- 4 e. NN
2	1	nnnn0i 9187	1 |- 4 e. NN0

Syntax hints:   e. wcel 2148   4c4 8975   NN0cn0 9179

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 7905  ax-resscn 7906  ax-1re 7908  ax-addrcl 7911

This theorem depends on definitions:  df-bi 117  df-3an 980  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-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-br 4006  df-iota 5180  df-fv 5226  df-ov 5881  df-inn 8923  df-2 8981  df-3 8982  df-4 8983  df-n0 9180

This theorem is referenced by:  6p5e11  9459  7p5e12  9463  8p5e13  9469  8p7e15  9471  9p5e14  9476  9p6e15  9477  4t3e12  9484  4t4e16  9485  5t5e25  9489  6t4e24  9492  6t5e30  9493  7t3e21  9496  7t5e35  9498  7t7e49  9500  8t3e24  9502  8t4e32  9503  8t5e40  9504  8t6e48  9505  8t7e56  9506  8t8e64  9507  9t5e45  9511  9t6e54  9512  9t7e63  9513  decbin3  9528  fzo0to42pr  10223  4bc3eq4  10756  resin4p  11729  recos4p  11730  ef01bndlem  11767  sin01bnd  11768  cos01bnd  11769  prm23lt5  12266  slotsdifdsndx  12682  slotsdifunifndx  12689  cnfldstr  13604  binom4  14558  ex-exp  14640  ex-fac  14641  ex-bc  14642