Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 1nn | Unicode version |
Description: Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.) |
Ref | Expression |
---|---|
1nn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfnn2 8850 | . . . 4 | |
2 | 1 | eleq2i 2231 | . . 3 |
3 | 1re 7889 | . . . 4 | |
4 | elintg 3826 | . . . 4 | |
5 | 3, 4 | ax-mp 5 | . . 3 |
6 | 2, 5 | bitri 183 | . 2 |
7 | vex 2724 | . . . 4 | |
8 | eleq2 2228 | . . . . 5 | |
9 | eleq2 2228 | . . . . . 6 | |
10 | 9 | raleqbi1dv 2667 | . . . . 5 |
11 | 8, 10 | anbi12d 465 | . . . 4 |
12 | 7, 11 | elab 2865 | . . 3 |
13 | 12 | simplbi 272 | . 2 |
14 | 6, 13 | mprgbir 2522 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 wcel 2135 cab 2150 wral 2442 cint 3818 (class class class)co 5836 cr 7743 c1 7745 caddc 7747 cn 8848 |
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-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-1re 7838 |
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-ral 2447 df-v 2723 df-int 3819 df-inn 8849 |
This theorem is referenced by: nnind 8864 nn1suc 8867 2nn 9009 1nn0 9121 nn0p1nn 9144 1z 9208 neg1z 9214 elz2 9253 nneoor 9284 9p1e10 9315 indstr 9522 elnn1uz2 9536 zq 9555 qreccl 9571 fz01or 10036 exp3vallem 10446 exp1 10451 nnexpcl 10458 expnbnd 10567 3dec 10616 fac1 10631 faccl 10637 faclbnd3 10645 resqrexlemf1 10936 resqrexlemcalc3 10944 resqrexlemnmsq 10945 resqrexlemnm 10946 resqrexlemcvg 10947 resqrexlemglsq 10950 resqrexlemga 10951 sumsnf 11336 cvgratnnlemnexp 11451 cvgratnnlemfm 11456 cvgratnnlemrate 11457 cvgratnn 11458 prodsnf 11519 fprodnncl 11537 eftlub 11617 eirraplem 11703 n2dvds1 11834 ndvdsp1 11854 gcd1 11905 bezoutr1 11951 ncoprmgcdne1b 12000 1nprm 12025 1idssfct 12026 isprm2lem 12027 qden1elz 12114 phicl2 12123 phi1 12128 phiprm 12132 eulerthlema 12139 pcpre1 12201 pczpre 12206 pcmptcl 12249 pcmpt 12250 exmidunben 12296 nninfdc 12325 base0 12380 baseval 12383 baseid 12384 basendx 12385 basendxnn 12386 1strstrg 12429 2strstrg 12431 basendxnplusgndx 12437 basendxnmulrndx 12445 rngstrg 12446 lmodstrd 12464 topgrpstrd 12482 setsmsdsg 13021 trilpolemgt1 13752 |
Copyright terms: Public domain | W3C validator |