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

Theorem nn0ind-raph 9275
 Description: Principle of Mathematical Induction (inference schema) on nonnegative integers. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. Raph Levien remarks: "This seems a bit painful. I wonder if an explicit substitution version would be easier." (Contributed by Raph Levien, 10-Apr-2004.)
Hypotheses
Ref Expression
nn0ind-raph.1
nn0ind-raph.2
nn0ind-raph.3
nn0ind-raph.4
nn0ind-raph.5
nn0ind-raph.6
Assertion
Ref Expression
nn0ind-raph
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()

Proof of Theorem nn0ind-raph
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 elnn0 9086 . 2
2 dfsbcq2 2940 . . . 4
3 nfv 1508 . . . . 5
4 nn0ind-raph.2 . . . . 5
53, 4sbhypf 2761 . . . 4
6 nfv 1508 . . . . 5
7 nn0ind-raph.3 . . . . 5
86, 7sbhypf 2761 . . . 4
9 nfv 1508 . . . . 5
10 nn0ind-raph.4 . . . . 5
119, 10sbhypf 2761 . . . 4
12 nfsbc1v 2955 . . . . 5
13 1ex 7867 . . . . 5
14 c0ex 7866 . . . . . . 7
15 0nn0 9099 . . . . . . . . . . . 12
16 eleq1a 2229 . . . . . . . . . . . 12
1715, 16ax-mp 5 . . . . . . . . . . 11
18 nn0ind-raph.5 . . . . . . . . . . . . . . 15
19 nn0ind-raph.1 . . . . . . . . . . . . . . 15
2018, 19mpbiri 167 . . . . . . . . . . . . . 14
21 eqeq2 2167 . . . . . . . . . . . . . . . 16
2221, 4syl6bir 163 . . . . . . . . . . . . . . 15
2322pm5.74d 181 . . . . . . . . . . . . . 14
2420, 23mpbii 147 . . . . . . . . . . . . 13
2524com12 30 . . . . . . . . . . . 12
2614, 25vtocle 2786 . . . . . . . . . . 11
27 nn0ind-raph.6 . . . . . . . . . . 11
2817, 26, 27sylc 62 . . . . . . . . . 10
2928adantr 274 . . . . . . . . 9
30 oveq1 5828 . . . . . . . . . . . . 13
31 0p1e1 8941 . . . . . . . . . . . . 13
3230, 31eqtrdi 2206 . . . . . . . . . . . 12
3332eqeq2d 2169 . . . . . . . . . . 11
3433, 7syl6bir 163 . . . . . . . . . 10
3534imp 123 . . . . . . . . 9
3629, 35mpbird 166 . . . . . . . 8
3736ex 114 . . . . . . 7
3814, 37vtocle 2786 . . . . . 6
39 sbceq1a 2946 . . . . . 6
4038, 39mpbid 146 . . . . 5
4112, 13, 40vtoclef 2785 . . . 4
42 nnnn0 9091 . . . . 5
4342, 27syl 14 . . . 4
442, 5, 8, 11, 41, 43nnind 8843 . . 3
45 nfv 1508 . . . . 5
46 eqeq1 2164 . . . . . 6
4719bicomd 140 . . . . . . . . 9
4847, 10sylan9bb 458 . . . . . . . 8
4918, 48mpbii 147 . . . . . . 7
5049ex 114 . . . . . 6
5146, 50sylbird 169 . . . . 5
5245, 14, 51vtoclef 2785 . . . 4
5352eqcoms 2160 . . 3
5444, 53jaoi 706 . 2
551, 54sylbi 120 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   wo 698   wceq 1335  wsb 1742   wcel 2128  wsbc 2937  (class class class)co 5821  cc0 7726  c1 7727   caddc 7729  cn 8827  cn0 9084 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 7817  ax-resscn 7818  ax-1cn 7819  ax-1re 7820  ax-icn 7821  ax-addcl 7822  ax-addrcl 7823  ax-mulcl 7824  ax-addcom 7826  ax-i2m1 7831  ax-0id 7834 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-rab 2444  df-v 2714  df-sbc 2938  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 5134  df-fv 5177  df-ov 5824  df-inn 8828  df-n0 9085 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator