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 8889 | . 2 ⊢ 1 ∈ ℕ | |
2 | 1 | nnnn0i 9143 | 1 ⊢ 1 ∈ ℕ0 |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2141 1c1 7775 ℕ0cn0 9135 |
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 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 ax-1re 7868 |
This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 df-v 2732 df-un 3125 df-in 3127 df-ss 3134 df-int 3832 df-inn 8879 df-n0 9136 |
This theorem is referenced by: peano2nn0 9175 deccl 9357 10nn0 9360 numsucc 9382 numadd 9389 numaddc 9390 11multnc 9410 6p5lem 9412 6p6e12 9416 7p5e12 9419 8p4e12 9424 9p2e11 9429 9p3e12 9430 10p10e20 9437 4t4e16 9441 5t2e10 9442 5t4e20 9444 6t3e18 9447 6t4e24 9448 7t3e21 9452 7t4e28 9453 8t3e24 9458 9t3e27 9465 9t9e81 9471 nn01to3 9576 fz0to3un2pr 10079 elfzom1elp1fzo 10158 fzo0sn0fzo1 10177 1tonninf 10396 expn1ap0 10486 nn0expcl 10490 sqval 10534 sq10 10646 nn0opthlem1d 10654 fac2 10665 bccl 10701 hashsng 10733 1elfz0hash 10741 bcxmas 11452 arisum 11461 geoisum1 11482 geoisum1c 11483 cvgratnnlemsumlt 11491 mertenslem2 11499 fprodnn0cl 11575 ege2le3 11634 ef4p 11657 efgt1p2 11658 efgt1p 11659 sin01gt0 11724 dvds1 11813 3dvds2dec 11825 isprm5 12096 pcelnn 12274 pockthg 12309 ennnfonelemhom 12370 dsndx 12576 dsid 12577 dsslid 12578 dveflem 13481 1kp2ke3k 13759 ex-exp 13762 ex-fac 13763 012of 14028 isomninnlem 14062 trilpolemisumle 14070 iswomninnlem 14081 iswomni0 14083 ismkvnnlem 14084 |
Copyright terms: Public domain | W3C validator |