![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 1nn0 | Unicode version |
Description: 1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.) |
Ref | Expression |
---|---|
1nn0 |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1nn 8494 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | nnnn0i 8742 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 ax-1re 7500 |
This theorem depends on definitions: df-bi 116 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-ral 2365 df-v 2622 df-un 3004 df-in 3006 df-ss 3013 df-int 3695 df-inn 8484 df-n0 8735 |
This theorem is referenced by: peano2nn0 8774 deccl 8952 10nn0 8955 numsucc 8977 numadd 8984 numaddc 8985 11multnc 9005 6p5lem 9007 6p6e12 9011 7p5e12 9014 8p4e12 9019 9p2e11 9024 9p3e12 9025 10p10e20 9032 4t4e16 9036 5t2e10 9037 5t4e20 9039 6t3e18 9042 6t4e24 9043 7t3e21 9047 7t4e28 9048 8t3e24 9053 9t3e27 9060 9t9e81 9066 nn01to3 9163 elfzom1elp1fzo 9674 fzo0sn0fzo1 9693 1tonninf 9907 expn1ap0 10026 nn0expcl 10030 sqval 10074 sq10 10182 nn0opthlem1d 10189 fac2 10200 bccl 10236 hashsng 10267 1elfz0hash 10275 bcxmas 10944 arisum 10953 geoisum1 10974 geoisum1c 10975 cvgratnnlemsumlt 10983 mertenslem2 10991 ege2le3 11022 ef4p 11045 efgt1p2 11046 efgt1p 11047 sin01gt0 11113 dvds1 11193 3dvds2dec 11205 1kp2ke3k 11924 ex-exp 11927 ex-fac 11928 |
Copyright terms: Public domain | W3C validator |