| 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 9305 |
. 2
| |
| 2 | 1 | nnnn0i 9410 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| 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 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-ext 2213 ax-sep 4207 ax-cnex 8123 ax-resscn 8124 ax-1re 8126 ax-addrcl 8129 |
| This theorem depends on definitions: df-bi 117 df-3an 1006 df-tru 1400 df-nf 1509 df-sb 1811 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ral 2515 df-rex 2516 df-v 2804 df-un 3204 df-in 3206 df-ss 3213 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-br 4089 df-iota 5286 df-fv 5334 df-ov 6021 df-inn 9144 df-2 9202 df-n0 9403 |
| This theorem is referenced by: nn0n0n1ge2 9550 7p6e13 9688 8p3e11 9691 8p5e13 9693 9p3e12 9698 9p4e13 9699 4t3e12 9708 4t4e16 9709 5t3e15 9711 5t5e25 9713 6t3e18 9715 6t5e30 9717 7t3e21 9720 7t4e28 9721 7t5e35 9722 7t6e42 9723 7t7e49 9724 8t3e24 9726 8t4e32 9727 8t5e40 9728 9t3e27 9733 9t4e36 9734 9t8e72 9738 9t9e81 9739 decbin3 9752 2eluzge0 9809 nn01to3 9851 xnn0le2is012 10101 fzo0to42pr 10466 nn0sqcl 10829 sqmul 10864 resqcl 10870 zsqcl 10873 cu2 10901 i3 10904 i4 10905 binom3 10920 nn0opthlem1d 10983 fac3 10995 faclbnd2 11005 abssq 11659 sqabs 11660 ef4p 12273 efgt1p2 12274 efi4p 12296 ef01bndlem 12335 cos01bnd 12337 oexpneg 12456 oddge22np1 12460 isprm5 12732 pythagtriplem4 12859 oddprmdvds 12945 dec2dvds 13002 dec5dvds 13003 2exp4 13022 2exp5 13023 2exp6 13024 2exp7 13025 2exp8 13026 2exp11 13027 2exp16 13028 3exp3 13029 2expltfac 13030 basendxltdsndx 13320 dsndxnplusgndx 13322 dsndxnmulrndx 13323 slotsdnscsi 13324 dsndxntsetndx 13325 slotsdifdsndx 13326 slotsdifunifndx 13333 prdsvalstrd 13372 cnfldstr 14591 setsmsdsg 15223 dveflem 15469 tangtx 15581 2logb9irr 15714 2logb9irrap 15720 binom4 15722 mersenne 15740 lgslem1 15748 gausslemma2dlem6 15815 lgseisenlem4 15821 2lgslem1c 15838 2lgslem3a 15841 2lgslem3b 15842 2lgslem3c 15843 2lgslem3d 15844 upgr2wlkdc 16247 konigsbergiedgwen 16354 konigsberglem1 16358 konigsberglem2 16359 konigsberglem3 16360 konigsberglem5 16362 konigsberg 16363 1kp2ke3k 16367 ex-exp 16370 ex-fac 16371 |
| Copyright terms: Public domain | W3C validator |