Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > peano2nn | Unicode version |
Description: Peano postulate: a successor of a positive integer is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
peano2nn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfnn2 8880 | . . . . . 6 | |
2 | 1 | eleq2i 2237 | . . . . 5 |
3 | elintg 3839 | . . . . 5 | |
4 | 2, 3 | syl5bb 191 | . . . 4 |
5 | 4 | ibi 175 | . . 3 |
6 | vex 2733 | . . . . . . . 8 | |
7 | eleq2 2234 | . . . . . . . . 9 | |
8 | eleq2 2234 | . . . . . . . . . 10 | |
9 | 8 | raleqbi1dv 2673 | . . . . . . . . 9 |
10 | 7, 9 | anbi12d 470 | . . . . . . . 8 |
11 | 6, 10 | elab 2874 | . . . . . . 7 |
12 | 11 | simprbi 273 | . . . . . 6 |
13 | oveq1 5860 | . . . . . . . 8 | |
14 | 13 | eleq1d 2239 | . . . . . . 7 |
15 | 14 | rspcva 2832 | . . . . . 6 |
16 | 12, 15 | sylan2 284 | . . . . 5 |
17 | 16 | expcom 115 | . . . 4 |
18 | 17 | ralimia 2531 | . . 3 |
19 | 5, 18 | syl 14 | . 2 |
20 | nnre 8885 | . . . 4 | |
21 | 1red 7935 | . . . 4 | |
22 | 20, 21 | readdcld 7949 | . . 3 |
23 | 1 | eleq2i 2237 | . . . 4 |
24 | elintg 3839 | . . . 4 | |
25 | 23, 24 | syl5bb 191 | . . 3 |
26 | 22, 25 | syl 14 | . 2 |
27 | 19, 26 | mpbird 166 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 wceq 1348 wcel 2141 cab 2156 wral 2448 cint 3831 (class class class)co 5853 cr 7773 c1 7775 caddc 7777 cn 8878 |
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 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 ax-sep 4107 ax-cnex 7865 ax-resscn 7866 ax-1re 7868 ax-addrcl 7871 |
This theorem depends on definitions: df-bi 116 df-3an 975 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 df-rex 2454 df-v 2732 df-un 3125 df-in 3127 df-ss 3134 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-br 3990 df-iota 5160 df-fv 5206 df-ov 5856 df-inn 8879 |
This theorem is referenced by: peano2nnd 8893 nnind 8894 nnaddcl 8898 2nn 9039 3nn 9040 4nn 9041 5nn 9042 6nn 9043 7nn 9044 8nn 9045 9nn 9046 nneoor 9314 10nn 9358 nnsplit 10093 fzonn0p1p1 10169 expp1 10483 facp1 10664 resqrexlemfp1 10973 resqrexlemcalc3 10980 trireciplem 11463 trirecip 11464 cvgratnnlemnexp 11487 cvgratz 11495 nno 11865 nnoddm1d2 11869 rplpwr 11982 prmind2 12074 sqrt2irr 12116 pcmpt 12295 pockthi 12310 2sqlem10 13755 |
Copyright terms: Public domain | W3C validator |