![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > 1nn | Unicode version |
Description: Peano postulate: 1 is a natural number. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
1nn |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1ex 9050 |
. . . 4
![]() ![]() ![]() ![]() | |
2 | fr0g 6660 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 8 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | frfnom 6659 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | peano1 4831 |
. . . 4
![]() ![]() ![]() ![]() | |
6 | fnfvelrn 5834 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 4, 5, 6 | mp2an 654 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 3, 7 | eqeltrri 2483 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | df-nn 9965 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | df-ima 4858 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 9, 10 | eqtri 2432 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 8, 11 | eleqtrri 2485 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem is referenced by: dfnn2 9977 dfnn3 9978 nnind 9982 nn1suc 9985 2nn 10097 nnunb 10181 1nn0 10201 nn0p1nn 10223 elz2 10262 1z 10275 nneo 10317 elnn1uz2 10516 zq 10544 rpnnen1lem4 10567 rpnnen1lem5 10568 ser1const 11342 exp1 11350 nnexpcl 11357 expnbnd 11471 fac1 11533 faccl 11539 faclbnd3 11546 faclbnd4lem1 11547 faclbnd4lem2 11548 faclbnd4lem3 11549 faclbnd4lem4 11550 cats1un 11753 revs1 11760 cats1fvn 11785 isercolllem2 12422 isercolllem3 12423 isercoll 12424 sumsn 12497 climcndslem1 12592 climcndslem2 12593 eftlub 12673 eirrlem 12766 xpnnenOLD 12772 rpnnen2lem5 12781 rpnnen2lem8 12784 rpnnen2 12788 nthruz 12814 dvdsle 12858 ndvdsp1 12892 bitsfzolem 12909 bitsfzo 12910 bitsinv1lem 12916 gcd1 12995 1nprm 13047 1idssfct 13048 qden1elz 13112 phi1 13125 phiprm 13129 pcpre1 13179 pczpre 13184 pcmptcl 13223 pcmpt 13224 infpnlem2 13242 prmreclem1 13247 prmreclem6 13252 mul4sq 13285 vdwmc2 13310 vdwlem8 13319 vdwlem13 13324 vdwnnlem3 13328 5prm 13394 7prm 13396 11prm 13400 13prm 13401 17prm 13402 19prm 13403 37prm 13406 43prm 13407 83prm 13408 139prm 13409 163prm 13410 317prm 13411 631prm 13412 1259lem4 13416 1259lem5 13417 1259prm 13418 2503lem3 13421 2503prm 13422 4001lem1 13423 4001lem2 13424 4001lem3 13425 4001lem4 13426 4001prm 13427 baseid 13474 basendx 13477 2strstr 13528 rngstr 13539 lmodstr 13556 topgrpstr 13579 otpsstr 13586 ocndx 13591 ocid 13592 ressds 13604 resshom 13609 ressco 13610 oppcbas 13907 rescbas 13992 rescabs 13996 catstr 14117 ipostr 14542 mulg1 14860 mulg2 14862 oppgbas 15110 od1 15158 gex1 15188 efgsval2 15328 efgsp1 15332 torsubg 15432 pgpfaclem1 15602 mgpbas 15617 mgpds 15621 opprbas 15697 srabase 16213 srads 16220 opsrbas 16502 zlmbas 16762 znbas2 16783 thlbas 16886 thlle 16887 hauspwdom 17525 ressunif 18253 tuslem 18258 imasdsf1olem 18364 setsmsds 18467 tmslem 18473 tnglem 18642 tngbas 18643 tngds 18650 bcthlem4 19241 bcth3 19245 ovolmge0 19334 ovollb2 19346 ovolctb 19347 ovolunlem1a 19353 ovolunlem1 19354 ovoliunlem1 19359 ovoliun 19362 ovoliun2 19363 ovolicc1 19373 voliunlem1 19405 volsup 19411 ioombl1lem2 19414 ioombl1lem4 19416 uniioombllem1 19434 uniioombllem2 19436 uniioombllem6 19441 itg1climres 19567 itg2seq 19595 itg2monolem1 19603 itg2monolem2 19604 itg2monolem3 19605 itg2mono 19606 itg2i1fseq2 19609 itg2cnlem1 19614 aalioulem5 20214 aaliou2b 20219 aaliou3lem4 20224 aaliou3lem7 20227 dcubic1lem 20644 dcubic2 20645 mcubic 20648 log2ub 20750 emcllem6 20800 emcllem7 20801 ftalem7 20822 efnnfsumcl 20846 vmaprm 20861 efvmacl 20864 efchtdvds 20903 vma1 20910 prmorcht 20922 sqff1o 20926 pclogsum 20960 perfectlem1 20974 perfectlem2 20975 bpos1 21028 bposlem5 21033 lgsdir 21075 1lgs 21082 lgs1 21083 lgsquad2lem2 21104 dchrmusumlema 21148 dchrisum0lema 21169 usgraexmpl 21381 konigsberg 21670 gx1 21811 ipval2 22164 opsqrlem2 23605 ssnnssfz 24109 rge0scvg 24296 zlmds 24309 qqh0 24329 qqh1 24330 esumfzf 24420 esumfsup 24421 esumpcvgval 24429 voliune 24546 rrvsum 24673 ballotlem4 24717 ballotlemi1 24721 ballotlemii 24722 ballotlemic 24725 ballotlem1c 24726 lgam1 24809 gam1 24810 fprodnncl 25242 prodsn 25247 nnrisefaccl 25295 faclimlem1 25318 ovoliunnfl 26155 voliunnfl 26157 volsupnfl 26158 nn0prpwlem 26223 nn0prpw 26224 incsequz 26350 bfplem1 26429 rrncmslem 26439 bezoutr1 26949 jm2.23 26965 rmydioph 26983 rmxdioph 26985 expdiophlem2 26991 expdioph 26992 sumsnd 27572 wallispilem4 27692 wallispi2lem1 27695 wallispi2lem2 27696 stirlinglem8 27705 stirlinglem11 27708 stirlinglem12 27709 stirlinglem13 27710 hlhilsbase 32437 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2393 ax-sep 4298 ax-nul 4306 ax-pow 4345 ax-pr 4371 ax-un 4668 ax-1cn 9012 |
This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2266 df-mo 2267 df-clab 2399 df-cleq 2405 df-clel 2408 df-nfc 2537 df-ne 2577 df-ral 2679 df-rex 2680 df-reu 2681 df-rab 2683 df-v 2926 df-sbc 3130 df-csb 3220 df-dif 3291 df-un 3293 df-in 3295 df-ss 3302 df-pss 3304 df-nul 3597 df-if 3708 df-pw 3769 df-sn 3788 df-pr 3789 df-tp 3790 df-op 3791 df-uni 3984 df-iun 4063 df-br 4181 df-opab 4235 df-mpt 4236 df-tr 4271 df-eprel 4462 df-id 4466 df-po 4471 df-so 4472 df-fr 4509 df-we 4511 df-ord 4552 df-on 4553 df-lim 4554 df-suc 4555 df-om 4813 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-iota 5385 df-fun 5423 df-fn 5424 df-f 5425 df-f1 5426 df-fo 5427 df-f1o 5428 df-fv 5429 df-recs 6600 df-rdg 6635 df-nn 9965 |
Copyright terms: Public domain | W3C validator |