Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > peano2z | Unicode version |
Description: Second Peano postulate generalized to integers. (Contributed by NM, 13-Feb-2005.) |
Ref | Expression |
---|---|
peano2z |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zre 8249 | . . 3 | |
2 | 1red 7042 | . . 3 | |
3 | 1, 2 | readdcld 7055 | . 2 |
4 | elznn0nn 8259 | . . . . 5 | |
5 | 4 | biimpi 113 | . . . 4 |
6 | 1 | biantrurd 289 | . . . . 5 |
7 | 6 | orbi2d 704 | . . . 4 |
8 | 5, 7 | mpbird 156 | . . 3 |
9 | peano2nn0 8222 | . . . . 5 | |
10 | 9 | a1i 9 | . . . 4 |
11 | 1 | adantr 261 | . . . . . . . . 9 |
12 | 1red 7042 | . . . . . . . . 9 | |
13 | 11, 12 | readdcld 7055 | . . . . . . . 8 |
14 | 13 | renegcld 7378 | . . . . . . 7 |
15 | 14 | recnd 7054 | . . . . . 6 |
16 | 11 | recnd 7054 | . . . . . . . . . . . 12 |
17 | 1cnd 7043 | . . . . . . . . . . . 12 | |
18 | 16, 17 | negdid 7335 | . . . . . . . . . . 11 |
19 | 18 | oveq1d 5527 | . . . . . . . . . 10 |
20 | 16 | negcld 7309 | . . . . . . . . . . 11 |
21 | neg1cn 8022 | . . . . . . . . . . . 12 | |
22 | 21 | a1i 9 | . . . . . . . . . . 11 |
23 | 20, 22, 17 | addassd 7049 | . . . . . . . . . 10 |
24 | 19, 23 | eqtrd 2072 | . . . . . . . . 9 |
25 | ax-1cn 6977 | . . . . . . . . . . 11 | |
26 | 1pneg1e0 8028 | . . . . . . . . . . 11 | |
27 | 25, 21, 26 | addcomli 7158 | . . . . . . . . . 10 |
28 | 27 | oveq2i 5523 | . . . . . . . . 9 |
29 | 24, 28 | syl6eq 2088 | . . . . . . . 8 |
30 | 20 | addid1d 7162 | . . . . . . . 8 |
31 | 29, 30 | eqtrd 2072 | . . . . . . 7 |
32 | simpr 103 | . . . . . . 7 | |
33 | 31, 32 | eqeltrd 2114 | . . . . . 6 |
34 | elnn0nn 8224 | . . . . . 6 | |
35 | 15, 33, 34 | sylanbrc 394 | . . . . 5 |
36 | 35 | ex 108 | . . . 4 |
37 | 10, 36 | orim12d 700 | . . 3 |
38 | 8, 37 | mpd 13 | . 2 |
39 | elznn0 8260 | . 2 | |
40 | 3, 38, 39 | sylanbrc 394 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 wo 629 wcel 1393 (class class class)co 5512 cc 6887 cr 6888 cc0 6889 c1 6890 caddc 6892 cneg 7183 cn 7914 cn0 8181 cz 8245 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-14 1405 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 ax-sep 3875 ax-pow 3927 ax-pr 3944 ax-setind 4262 ax-cnex 6975 ax-resscn 6976 ax-1cn 6977 ax-1re 6978 ax-icn 6979 ax-addcl 6980 ax-addrcl 6981 ax-mulcl 6982 ax-addcom 6984 ax-addass 6986 ax-distr 6988 ax-i2m1 6989 ax-0id 6992 ax-rnegex 6993 ax-cnre 6995 |
This theorem depends on definitions: df-bi 110 df-3or 886 df-3an 887 df-tru 1246 df-fal 1249 df-nf 1350 df-sb 1646 df-eu 1903 df-mo 1904 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-ne 2206 df-ral 2311 df-rex 2312 df-reu 2313 df-rab 2315 df-v 2559 df-sbc 2765 df-dif 2920 df-un 2922 df-in 2924 df-ss 2931 df-pw 3361 df-sn 3381 df-pr 3382 df-op 3384 df-uni 3581 df-int 3616 df-br 3765 df-opab 3819 df-id 4030 df-xp 4351 df-rel 4352 df-cnv 4353 df-co 4354 df-dm 4355 df-iota 4867 df-fun 4904 df-fv 4910 df-riota 5468 df-ov 5515 df-oprab 5516 df-mpt2 5517 df-sub 7184 df-neg 7185 df-inn 7915 df-n0 8182 df-z 8246 |
This theorem is referenced by: zaddcllempos 8282 peano2zm 8283 zleltp1 8299 btwnnz 8334 peano2uz2 8345 uzind 8349 uzind2 8350 peano2zd 8363 eluzp1m1 8496 eluzp1p1 8498 peano2uz 8526 fzp1disj 8942 elfzp1b 8959 fzneuz 8963 fzp1nel 8966 fzval3 9060 fzossfzop1 9068 rebtwn2zlemstep 9107 flhalf 9144 frec2uzzd 9186 frec2uzsucd 9187 zesq 9367 |
Copyright terms: Public domain | W3C validator |