Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > peano1 | Unicode version |
Description: Zero is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. (Contributed by NM, 15-May-1994.) |
Ref | Expression |
---|---|
peano1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0ex 4103 | . . . 4 | |
2 | 1 | elint 3824 | . . 3 |
3 | df-clab 2151 | . . . 4 | |
4 | simpl 108 | . . . . . 6 | |
5 | 4 | sbimi 1751 | . . . . 5 |
6 | clelsb4 2270 | . . . . 5 | |
7 | 5, 6 | sylib 121 | . . . 4 |
8 | 3, 7 | sylbi 120 | . . 3 |
9 | 2, 8 | mpgbir 1440 | . 2 |
10 | dfom3 4563 | . 2 | |
11 | 9, 10 | eleqtrri 2240 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wsb 1749 wcel 2135 cab 2150 wral 2442 c0 3404 cint 3818 csuc 4337 com 4561 |
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-in1 604 ax-in2 605 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 ax-nul 4102 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2723 df-dif 3113 df-nul 3405 df-int 3819 df-iom 4562 |
This theorem is referenced by: peano5 4569 limom 4585 nnregexmid 4592 omsinds 4593 nnpredcl 4594 frec0g 6356 frecabcl 6358 frecrdg 6367 oa1suc 6426 nna0r 6437 nnm0r 6438 nnmcl 6440 nnmsucr 6447 1onn 6479 nnm1 6483 nnaordex 6486 nnawordex 6487 php5 6815 php5dom 6820 0fin 6841 findcard2 6846 findcard2s 6847 infm 6861 inffiexmid 6863 0ct 7063 ctmlemr 7064 ctssdclemn0 7066 ctssdc 7069 omct 7073 nninfisol 7088 fodjum 7101 fodju0 7102 ctssexmid 7105 1lt2pi 7272 nq0m0r 7388 nq0a0 7389 prarloclem5 7432 frec2uzrand 10330 frecuzrdg0 10338 frecuzrdg0t 10347 frecfzennn 10351 0tonninf 10364 1tonninf 10365 hashinfom 10680 hashunlem 10706 hash1 10713 ennnfonelemj0 12277 ennnfonelem1 12283 ennnfonelemhf1o 12289 ennnfonelemhom 12291 bj-nn0suc 13687 bj-nn0sucALT 13701 012of 13716 2o01f 13717 pwle2 13719 pwf1oexmid 13720 subctctexmid 13722 peano3nninf 13728 nninfall 13730 nninfsellemdc 13731 nninfsellemeq 13735 nninffeq 13741 isomninnlem 13750 iswomninnlem 13769 ismkvnnlem 13772 |
Copyright terms: Public domain | W3C validator |