Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 2nn0 | Unicode version |
Description: 2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.) |
Ref | Expression |
---|---|
2nn0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2nn 9009 | . 2 | |
2 | 1 | nnnn0i 9113 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 2135 c2 8899 cn0 9105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 ax-sep 4094 ax-cnex 7835 ax-resscn 7836 ax-1re 7838 ax-addrcl 7841 |
This theorem depends on definitions: df-bi 116 df-3an 969 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-ral 2447 df-rex 2448 df-v 2723 df-un 3115 df-in 3117 df-ss 3124 df-sn 3576 df-pr 3577 df-op 3579 df-uni 3784 df-int 3819 df-br 3977 df-iota 5147 df-fv 5190 df-ov 5839 df-inn 8849 df-2 8907 df-n0 9106 |
This theorem is referenced by: nn0n0n1ge2 9252 7p6e13 9390 8p3e11 9393 8p5e13 9395 9p3e12 9400 9p4e13 9401 4t3e12 9410 4t4e16 9411 5t3e15 9413 5t5e25 9415 6t3e18 9417 6t5e30 9419 7t3e21 9422 7t4e28 9423 7t5e35 9424 7t6e42 9425 7t7e49 9426 8t3e24 9428 8t4e32 9429 8t5e40 9430 9t3e27 9435 9t4e36 9436 9t8e72 9440 9t9e81 9441 decbin3 9454 2eluzge0 9504 nn01to3 9546 xnn0le2is012 9793 fzo0to42pr 10145 nn0sqcl 10472 sqmul 10507 resqcl 10512 zsqcl 10515 cu2 10543 i3 10546 i4 10547 binom3 10561 nn0opthlem1d 10622 fac3 10634 faclbnd2 10644 abssq 11009 sqabs 11010 ef4p 11621 efgt1p2 11622 efi4p 11644 ef01bndlem 11683 cos01bnd 11685 oexpneg 11799 oddge22np1 11803 isprm5 12053 pythagtriplem4 12179 oddprmdvds 12263 setsmsdsg 13027 dveflem 13234 tangtx 13306 2logb9irr 13436 2logb9irrap 13442 binom4 13444 1kp2ke3k 13448 ex-exp 13451 ex-fac 13452 |
Copyright terms: Public domain | W3C validator |