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 8835 | . . . . . 6 | |
2 | 1 | eleq2i 2224 | . . . . 5 |
3 | elintg 3815 | . . . . 5 | |
4 | 2, 3 | syl5bb 191 | . . . 4 |
5 | 4 | ibi 175 | . . 3 |
6 | vex 2715 | . . . . . . . 8 | |
7 | eleq2 2221 | . . . . . . . . 9 | |
8 | eleq2 2221 | . . . . . . . . . 10 | |
9 | 8 | raleqbi1dv 2660 | . . . . . . . . 9 |
10 | 7, 9 | anbi12d 465 | . . . . . . . 8 |
11 | 6, 10 | elab 2856 | . . . . . . 7 |
12 | 11 | simprbi 273 | . . . . . 6 |
13 | oveq1 5831 | . . . . . . . 8 | |
14 | 13 | eleq1d 2226 | . . . . . . 7 |
15 | 14 | rspcva 2814 | . . . . . 6 |
16 | 12, 15 | sylan2 284 | . . . . 5 |
17 | 16 | expcom 115 | . . . 4 |
18 | 17 | ralimia 2518 | . . 3 |
19 | 5, 18 | syl 14 | . 2 |
20 | nnre 8840 | . . . 4 | |
21 | 1red 7893 | . . . 4 | |
22 | 20, 21 | readdcld 7907 | . . 3 |
23 | 1 | eleq2i 2224 | . . . 4 |
24 | elintg 3815 | . . . 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 1335 wcel 2128 cab 2143 wral 2435 cint 3807 (class class class)co 5824 cr 7731 c1 7733 caddc 7735 cn 8833 |
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 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 ax-sep 4082 ax-cnex 7823 ax-resscn 7824 ax-1re 7826 ax-addrcl 7829 |
This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1338 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ral 2440 df-rex 2441 df-v 2714 df-un 3106 df-in 3108 df-ss 3115 df-sn 3566 df-pr 3567 df-op 3569 df-uni 3773 df-int 3808 df-br 3966 df-iota 5135 df-fv 5178 df-ov 5827 df-inn 8834 |
This theorem is referenced by: peano2nnd 8848 nnind 8849 nnaddcl 8853 2nn 8994 3nn 8995 4nn 8996 5nn 8997 6nn 8998 7nn 8999 8nn 9000 9nn 9001 nneoor 9266 10nn 9310 nnsplit 10036 fzonn0p1p1 10112 expp1 10426 facp1 10604 resqrexlemfp1 10909 resqrexlemcalc3 10916 trireciplem 11397 trirecip 11398 cvgratnnlemnexp 11421 cvgratz 11429 nno 11797 nnoddm1d2 11801 rplpwr 11911 prmind2 11997 sqrt2irr 12037 |
Copyright terms: Public domain | W3C validator |