![]() |
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 8932 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | nnnn0i 9186 |
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 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 7907 |
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 2741 df-un 3135 df-in 3137 df-ss 3144 df-int 3847 df-inn 8922 df-n0 9179 |
This theorem is referenced by: peano2nn0 9218 deccl 9400 10nn0 9403 numsucc 9425 numadd 9432 numaddc 9433 11multnc 9453 6p5lem 9455 6p6e12 9459 7p5e12 9462 8p4e12 9467 9p2e11 9472 9p3e12 9473 10p10e20 9480 4t4e16 9484 5t2e10 9485 5t4e20 9487 6t3e18 9490 6t4e24 9491 7t3e21 9495 7t4e28 9496 8t3e24 9501 9t3e27 9508 9t9e81 9514 nn01to3 9619 fz0to3un2pr 10125 elfzom1elp1fzo 10204 fzo0sn0fzo1 10223 1tonninf 10442 expn1ap0 10532 nn0expcl 10536 sqval 10580 sq10 10694 nn0opthlem1d 10702 fac2 10713 bccl 10749 hashsng 10780 1elfz0hash 10788 bcxmas 11499 arisum 11508 geoisum1 11529 geoisum1c 11530 cvgratnnlemsumlt 11538 mertenslem2 11546 fprodnn0cl 11622 ege2le3 11681 ef4p 11704 efgt1p2 11705 efgt1p 11706 sin01gt0 11771 dvds1 11861 3dvds2dec 11873 isprm5 12144 pcelnn 12322 pockthg 12357 ennnfonelemhom 12418 dsndx 12671 dsid 12672 dsslid 12673 dsndxnn 12674 basendxltdsndx 12675 slotsdifdsndx 12681 unifndx 12682 unifid 12683 unifndxnn 12684 basendxltunifndx 12685 slotsdifunifndx 12688 homid 12689 homslid 12690 ccoid 12691 ccoslid 12692 cnfldstr 13542 dveflem 14272 1kp2ke3k 14561 ex-exp 14564 ex-fac 14565 012of 14830 isomninnlem 14863 trilpolemisumle 14871 iswomninnlem 14882 iswomni0 14884 ismkvnnlem 14885 |
Copyright terms: Public domain | W3C validator |