![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > peano2zd | GIF version |
Description: Deduction from second Peano postulate generalized to integers. (Contributed by Mario Carneiro, 28-May-2016.) |
Ref | Expression |
---|---|
zred.1 | ⊢ (𝜑 → 𝐴 ∈ ℤ) |
Ref | Expression |
---|---|
peano2zd | ⊢ (𝜑 → (𝐴 + 1) ∈ ℤ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zred.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℤ) | |
2 | peano2z 9182 | . 2 ⊢ (𝐴 ∈ ℤ → (𝐴 + 1) ∈ ℤ) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (𝐴 + 1) ∈ ℤ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2125 (class class class)co 5814 1c1 7712 + caddc 7714 ℤcz 9146 |
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-in1 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-14 2128 ax-ext 2136 ax-sep 4078 ax-pow 4130 ax-pr 4164 ax-setind 4490 ax-cnex 7802 ax-resscn 7803 ax-1cn 7804 ax-1re 7805 ax-icn 7806 ax-addcl 7807 ax-addrcl 7808 ax-mulcl 7809 ax-addcom 7811 ax-addass 7813 ax-distr 7815 ax-i2m1 7816 ax-0id 7819 ax-rnegex 7820 ax-cnre 7822 |
This theorem depends on definitions: df-bi 116 df-3or 964 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1740 df-eu 2006 df-mo 2007 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-ne 2325 df-ral 2437 df-rex 2438 df-reu 2439 df-rab 2441 df-v 2711 df-sbc 2934 df-dif 3100 df-un 3102 df-in 3104 df-ss 3111 df-pw 3541 df-sn 3562 df-pr 3563 df-op 3565 df-uni 3769 df-int 3804 df-br 3962 df-opab 4022 df-id 4248 df-xp 4585 df-rel 4586 df-cnv 4587 df-co 4588 df-dm 4589 df-iota 5128 df-fun 5165 df-fv 5171 df-riota 5770 df-ov 5817 df-oprab 5818 df-mpo 5819 df-sub 8027 df-neg 8028 df-inn 8813 df-n0 9070 df-z 9147 |
This theorem is referenced by: elfzp1 9952 fznatpl1 9956 fzdifsuc 9961 fseq1p1m1 9974 flqge 10159 2tnp1ge0ge0 10178 ceiqm1l 10188 addmodlteq 10275 frec2uzzd 10277 frec2uzrdg 10286 uzsinds 10319 seq3f1olemqsumkj 10375 seq3f1olemqsumk 10376 bcp1nk 10613 bcval5 10614 hashfz 10672 resqrexlemdecn 10889 telfsumo 11340 fsumparts 11344 binomlem 11357 geo2sum 11388 cvgratnnlemseq 11400 cvgratnnlemabsle 11401 cvgratnnlemsumlt 11402 cvgratnnlemrate 11404 cvgratz 11406 mertenslemub 11408 mertenslemi1 11409 clim2prod 11413 clim2divap 11414 fprodntrivap 11458 fprodeq0 11491 dvdsfac 11725 2tp1odd 11748 opoe 11759 zsupcllemstep 11805 prmind2 11968 hashdvds 12064 cvgcmp2nlemabs 13544 |
Copyright terms: Public domain | W3C validator |