Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  zindd Unicode version

Theorem zindd 9220
 Description: Principle of Mathematical Induction on all integers, deduction version. The first five hypotheses give the substitutions; the last three are the basis, the induction, and the extension to negative numbers. (Contributed by Paul Chapman, 17-Apr-2009.) (Proof shortened by Mario Carneiro, 4-Jan-2017.)
Hypotheses
Ref Expression
zindd.1
zindd.2
zindd.3
zindd.4
zindd.5
zindd.6
zindd.7
zindd.8
Assertion
Ref Expression
zindd
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()   ()

Proof of Theorem zindd
StepHypRef Expression
1 znegcl 9136 . . . . . . 7
2 elznn0nn 9119 . . . . . . 7
31, 2sylib 121 . . . . . 6
4 simpr 109 . . . . . . 7
54orim2i 751 . . . . . 6
63, 5syl 14 . . . . 5
7 zcn 9110 . . . . . . . 8
87negnegd 8115 . . . . . . 7
98eleq1d 2209 . . . . . 6
109orbi2d 780 . . . . 5
116, 10mpbid 146 . . . 4
12 zindd.1 . . . . . . . 8
1312imbi2d 229 . . . . . . 7
14 zindd.2 . . . . . . . 8
1514imbi2d 229 . . . . . . 7
16 zindd.3 . . . . . . . 8
1716imbi2d 229 . . . . . . 7
18 zindd.4 . . . . . . . 8
1918imbi2d 229 . . . . . . 7
20 zindd.6 . . . . . . 7
21 zindd.7 . . . . . . . . 9
2221com12 30 . . . . . . . 8
2322a2d 26 . . . . . . 7
2413, 15, 17, 19, 20, 23nn0ind 9216 . . . . . 6
2524com12 30 . . . . 5
26 nnnn0 9035 . . . . . . . 8
2713, 15, 17, 15, 20, 23nn0ind 9216 . . . . . . . 8
2826, 27syl 14 . . . . . . 7
2928com12 30 . . . . . 6
30 zindd.8 . . . . . 6
3129, 30mpdd 41 . . . . 5
3225, 31jaod 707 . . . 4
3311, 32syl5 32 . . 3
3433ralrimiv 2508 . 2
35 znegcl 9136 . . . . 5
36 negeq 8006 . . . . . . . . 9
37 zcn 9110 . . . . . . . . . 10
3837negnegd 8115 . . . . . . . . 9
3936, 38sylan9eqr 2195 . . . . . . . 8
4039eqcomd 2146 . . . . . . 7
4140, 18syl 14 . . . . . 6
4241bicomd 140 . . . . 5
4335, 42rspcdv 2797 . . . 4
4443com12 30 . . 3
4544ralrimiv 2508 . 2
46 zindd.5 . . 3
4746rspccv 2791 . 2
4834, 45, 473syl 17 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   wo 698   wceq 1332   wcel 1481  wral 2417  (class class class)co 5785  cr 7670  cc0 7671  c1 7672   caddc 7674  cneg 7985  cn 8771  cn0 9028  cz 9105 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 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4055  ax-pow 4107  ax-pr 4141  ax-un 4365  ax-setind 4462  ax-cnex 7762  ax-resscn 7763  ax-1cn 7764  ax-1re 7765  ax-icn 7766  ax-addcl 7767  ax-addrcl 7768  ax-mulcl 7769  ax-addcom 7771  ax-addass 7773  ax-distr 7775  ax-i2m1 7776  ax-0lt1 7777  ax-0id 7779  ax-rnegex 7780  ax-cnre 7782  ax-pre-ltirr 7783  ax-pre-ltwlin 7784  ax-pre-lttrn 7785  ax-pre-ltadd 7787 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 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2692  df-sbc 2915  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-int 3781  df-br 3939  df-opab 3999  df-id 4225  df-xp 4556  df-rel 4557  df-cnv 4558  df-co 4559  df-dm 4560  df-iota 5099  df-fun 5136  df-fv 5142  df-riota 5741  df-ov 5788  df-oprab 5789  df-mpo 5790  df-pnf 7853  df-mnf 7854  df-xr 7855  df-ltxr 7856  df-le 7857  df-sub 7986  df-neg 7987  df-inn 8772  df-n0 9029  df-z 9106 This theorem is referenced by:  efexp  11459
 Copyright terms: Public domain W3C validator