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

Theorem nn0ind-raph 8080
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 (x = 0 → (φψ))
nn0ind-raph.2 (x = y → (φχ))
nn0ind-raph.3 (x = (y + 1) → (φθ))
nn0ind-raph.4 (x = A → (φτ))
nn0ind-raph.5 ψ
nn0ind-raph.6 (y 0 → (χθ))
Assertion
Ref Expression
nn0ind-raph (A 0τ)
Distinct variable groups:   x,y   x,A   ψ,x   χ,x   θ,x   τ,x   φ,y
Allowed substitution hints:   φ(x)   ψ(y)   χ(y)   θ(y)   τ(y)   A(y)

Proof of Theorem nn0ind-raph
Dummy variable z is distinct from all other variables.
StepHypRef Expression
1 elnn0 7909 . 2 (A 0 ↔ (A A = 0))
2 dfsbcq2 2761 . . . 4 (z = 1 → ([z / x]φ[1 / x]φ))
3 nfv 1418 . . . . 5 xχ
4 nn0ind-raph.2 . . . . 5 (x = y → (φχ))
53, 4sbhypf 2597 . . . 4 (z = y → ([z / x]φχ))
6 nfv 1418 . . . . 5 xθ
7 nn0ind-raph.3 . . . . 5 (x = (y + 1) → (φθ))
86, 7sbhypf 2597 . . . 4 (z = (y + 1) → ([z / x]φθ))
9 nfv 1418 . . . . 5 xτ
10 nn0ind-raph.4 . . . . 5 (x = A → (φτ))
119, 10sbhypf 2597 . . . 4 (z = A → ([z / x]φτ))
12 nfsbc1v 2776 . . . . 5 x[1 / x]φ
13 1ex 6772 . . . . 5 1 V
14 c0ex 6771 . . . . . . 7 0 V
15 0nn0 7922 . . . . . . . . . . . 12 0 0
16 eleq1a 2106 . . . . . . . . . . . 12 (0 0 → (y = 0 → y 0))
1715, 16ax-mp 7 . . . . . . . . . . 11 (y = 0 → y 0)
18 nn0ind-raph.5 . . . . . . . . . . . . . . 15 ψ
19 nn0ind-raph.1 . . . . . . . . . . . . . . 15 (x = 0 → (φψ))
2018, 19mpbiri 157 . . . . . . . . . . . . . 14 (x = 0 → φ)
21 eqeq2 2046 . . . . . . . . . . . . . . . 16 (y = 0 → (x = yx = 0))
2221, 4syl6bir 153 . . . . . . . . . . . . . . 15 (y = 0 → (x = 0 → (φχ)))
2322pm5.74d 171 . . . . . . . . . . . . . 14 (y = 0 → ((x = 0 → φ) ↔ (x = 0 → χ)))
2420, 23mpbii 136 . . . . . . . . . . . . 13 (y = 0 → (x = 0 → χ))
2524com12 27 . . . . . . . . . . . 12 (x = 0 → (y = 0 → χ))
2614, 25vtocle 2621 . . . . . . . . . . 11 (y = 0 → χ)
27 nn0ind-raph.6 . . . . . . . . . . 11 (y 0 → (χθ))
2817, 26, 27sylc 56 . . . . . . . . . 10 (y = 0 → θ)
2928adantr 261 . . . . . . . . 9 ((y = 0 x = 1) → θ)
30 oveq1 5459 . . . . . . . . . . . . 13 (y = 0 → (y + 1) = (0 + 1))
31 0p1e1 7759 . . . . . . . . . . . . 13 (0 + 1) = 1
3230, 31syl6eq 2085 . . . . . . . . . . . 12 (y = 0 → (y + 1) = 1)
3332eqeq2d 2048 . . . . . . . . . . 11 (y = 0 → (x = (y + 1) ↔ x = 1))
3433, 7syl6bir 153 . . . . . . . . . 10 (y = 0 → (x = 1 → (φθ)))
3534imp 115 . . . . . . . . 9 ((y = 0 x = 1) → (φθ))
3629, 35mpbird 156 . . . . . . . 8 ((y = 0 x = 1) → φ)
3736ex 108 . . . . . . 7 (y = 0 → (x = 1 → φ))
3814, 37vtocle 2621 . . . . . 6 (x = 1 → φ)
39 sbceq1a 2767 . . . . . 6 (x = 1 → (φ[1 / x]φ))
4038, 39mpbid 135 . . . . 5 (x = 1 → [1 / x]φ)
4112, 13, 40vtoclef 2620 . . . 4 [1 / x]φ
42 nnnn0 7914 . . . . 5 (y ℕ → y 0)
4342, 27syl 14 . . . 4 (y ℕ → (χθ))
442, 5, 8, 11, 41, 43nnind 7662 . . 3 (A ℕ → τ)
45 nfv 1418 . . . . 5 x(0 = Aτ)
46 eqeq1 2043 . . . . . 6 (x = 0 → (x = A ↔ 0 = A))
4719bicomd 129 . . . . . . . . 9 (x = 0 → (ψφ))
4847, 10sylan9bb 435 . . . . . . . 8 ((x = 0 x = A) → (ψτ))
4918, 48mpbii 136 . . . . . . 7 ((x = 0 x = A) → τ)
5049ex 108 . . . . . 6 (x = 0 → (x = Aτ))
5146, 50sylbird 159 . . . . 5 (x = 0 → (0 = Aτ))
5245, 14, 51vtoclef 2620 . . . 4 (0 = Aτ)
5352eqcoms 2040 . . 3 (A = 0 → τ)
5444, 53jaoi 635 . 2 ((A A = 0) → τ)
551, 54sylbi 114 1 (A 0τ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   wo 628   = wceq 1242   wcel 1390  [wsb 1642  [wsbc 2758  (class class class)co 5452  0cc0 6663  1c1 6664   + caddc 6666  cn 7646  0cn0 7907
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-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3865  ax-cnex 6726  ax-resscn 6727  ax-1cn 6728  ax-1re 6729  ax-icn 6730  ax-addcl 6731  ax-addrcl 6732  ax-mulcl 6733  ax-addcom 6735  ax-i2m1 6740  ax-0id 6743
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-sn 3372  df-pr 3373  df-op 3375  df-uni 3571  df-int 3606  df-br 3755  df-iota 4809  df-fv 4852  df-ov 5455  df-inn 7647  df-n0 7908
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator