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 3884 | . . . 4 | |
2 | 1 | elint 3621 | . . 3 |
3 | df-clab 2027 | . . . 4 | |
4 | simpl 102 | . . . . . 6 | |
5 | 4 | sbimi 1647 | . . . . 5 |
6 | clelsb4 2143 | . . . . 5 | |
7 | 5, 6 | sylib 127 | . . . 4 |
8 | 3, 7 | sylbi 114 | . . 3 |
9 | 2, 8 | mpgbir 1342 | . 2 |
10 | dfom3 4315 | . 2 | |
11 | 9, 10 | eleqtrri 2113 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 wcel 1393 wsb 1645 cab 2026 wral 2306 c0 3224 cint 3615 csuc 4102 com 4313 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 ax-nul 3883 |
This theorem depends on definitions: df-bi 110 df-tru 1246 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-v 2559 df-dif 2920 df-nul 3225 df-int 3616 df-iom 4314 |
This theorem is referenced by: peano5 4321 limom 4336 nnregexmid 4342 frec0g 5983 frecrdg 5992 oa1suc 6047 nna0r 6057 nnm0r 6058 nnmcl 6060 nnmsucr 6067 1onn 6093 nnm1 6097 nnaordex 6100 nnawordex 6101 php5 6321 php5dom 6325 0fin 6341 findcard2 6346 findcard2s 6347 1lt2pi 6438 nq0m0r 6554 nq0a0 6555 prarloclem5 6598 frec2uzrand 9191 frecuzrdg0 9200 frecfzennn 9203 peano5setOLD 10065 bj-nn0suc 10089 bj-nn0sucALT 10103 |
Copyright terms: Public domain | W3C validator |