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 4025 | . . . 4 | |
2 | 1 | elint 3747 | . . 3 |
3 | df-clab 2104 | . . . 4 | |
4 | simpl 108 | . . . . . 6 | |
5 | 4 | sbimi 1722 | . . . . 5 |
6 | clelsb4 2223 | . . . . 5 | |
7 | 5, 6 | sylib 121 | . . . 4 |
8 | 3, 7 | sylbi 120 | . . 3 |
9 | 2, 8 | mpgbir 1414 | . 2 |
10 | dfom3 4476 | . 2 | |
11 | 9, 10 | eleqtrri 2193 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wcel 1465 wsb 1720 cab 2103 wral 2393 c0 3333 cint 3741 csuc 4257 com 4474 |
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 588 ax-in2 589 ax-io 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 ax-nul 4024 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-v 2662 df-dif 3043 df-nul 3334 df-int 3742 df-iom 4475 |
This theorem is referenced by: peano5 4482 limom 4497 nnregexmid 4504 omsinds 4505 nnpredcl 4506 frec0g 6262 frecabcl 6264 frecrdg 6273 oa1suc 6331 nna0r 6342 nnm0r 6343 nnmcl 6345 nnmsucr 6352 1onn 6384 nnm1 6388 nnaordex 6391 nnawordex 6392 php5 6720 php5dom 6725 0fin 6746 findcard2 6751 findcard2s 6752 infm 6766 inffiexmid 6768 0ct 6960 ctmlemr 6961 ctssdclemn0 6963 ctssdc 6966 omct 6970 fodjum 6986 fodju0 6987 ctssexmid 6992 1lt2pi 7116 nq0m0r 7232 nq0a0 7233 prarloclem5 7276 frec2uzrand 10146 frecuzrdg0 10154 frecuzrdg0t 10163 frecfzennn 10167 0tonninf 10180 1tonninf 10181 hashinfom 10492 hashunlem 10518 hash1 10525 ennnfonelemj0 11841 ennnfonelem1 11847 ennnfonelemhf1o 11853 ennnfonelemhom 11855 bj-nn0suc 13089 bj-nn0sucALT 13103 pwle2 13120 pwf1oexmid 13121 subctctexmid 13123 peano3nninf 13128 nninfall 13131 nninfsellemdc 13133 nninfsellemeq 13137 nninffeq 13143 isomninnlem 13152 |
Copyright terms: Public domain | W3C validator |