![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 1nn0 | GIF version |
Description: 1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.) |
Ref | Expression |
---|---|
1nn0 | ⊢ 1 ∈ ℕ0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1nn 8928 | . 2 ⊢ 1 ∈ ℕ | |
2 | 1 | nnnn0i 9182 | 1 ⊢ 1 ∈ ℕ0 |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2148 1c1 7811 ℕ0cn0 9174 |
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-1re 7904 |
This theorem depends on definitions: df-bi 117 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-v 2739 df-un 3133 df-in 3135 df-ss 3142 df-int 3845 df-inn 8918 df-n0 9175 |
This theorem is referenced by: peano2nn0 9214 deccl 9396 10nn0 9399 numsucc 9421 numadd 9428 numaddc 9429 11multnc 9449 6p5lem 9451 6p6e12 9455 7p5e12 9458 8p4e12 9463 9p2e11 9468 9p3e12 9469 10p10e20 9476 4t4e16 9480 5t2e10 9481 5t4e20 9483 6t3e18 9486 6t4e24 9487 7t3e21 9491 7t4e28 9492 8t3e24 9497 9t3e27 9504 9t9e81 9510 nn01to3 9615 fz0to3un2pr 10120 elfzom1elp1fzo 10199 fzo0sn0fzo1 10218 1tonninf 10437 expn1ap0 10527 nn0expcl 10531 sqval 10575 sq10 10687 nn0opthlem1d 10695 fac2 10706 bccl 10742 hashsng 10773 1elfz0hash 10781 bcxmas 11492 arisum 11501 geoisum1 11522 geoisum1c 11523 cvgratnnlemsumlt 11531 mertenslem2 11539 fprodnn0cl 11615 ege2le3 11674 ef4p 11697 efgt1p2 11698 efgt1p 11699 sin01gt0 11764 dvds1 11853 3dvds2dec 11865 isprm5 12136 pcelnn 12314 pockthg 12349 ennnfonelemhom 12410 dsndx 12660 dsid 12661 dsslid 12662 dsndxnn 12663 basendxltdsndx 12664 slotsdifdsndx 12670 unifndx 12671 unifid 12672 unifndxnn 12673 basendxltunifndx 12674 slotsdifunifndx 12677 cnfldstr 13348 dveflem 14080 1kp2ke3k 14358 ex-exp 14361 ex-fac 14362 012of 14627 isomninnlem 14660 trilpolemisumle 14668 iswomninnlem 14679 iswomni0 14681 ismkvnnlem 14682 |
Copyright terms: Public domain | W3C validator |