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

Theorem nnind 8410
Description: Principle of Mathematical Induction (inference schema). The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. See nnaddcl 8414 for an example of its use. This is an alternative for Metamath 100 proof #74. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.)
Hypotheses
Ref Expression
nnind.1 (𝑥 = 1 → (𝜑𝜓))
nnind.2 (𝑥 = 𝑦 → (𝜑𝜒))
nnind.3 (𝑥 = (𝑦 + 1) → (𝜑𝜃))
nnind.4 (𝑥 = 𝐴 → (𝜑𝜏))
nnind.5 𝜓
nnind.6 (𝑦 ∈ ℕ → (𝜒𝜃))
Assertion
Ref Expression
nnind (𝐴 ∈ ℕ → 𝜏)
Distinct variable groups:   𝑥,𝑦   𝑥,𝐴   𝜓,𝑥   𝜒,𝑥   𝜃,𝑥   𝜏,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝜒(𝑦)   𝜃(𝑦)   𝜏(𝑦)   𝐴(𝑦)

Proof of Theorem nnind
StepHypRef Expression
1 1nn 8405 . . . . . 6 1 ∈ ℕ
2 nnind.5 . . . . . 6 𝜓
3 nnind.1 . . . . . . 7 (𝑥 = 1 → (𝜑𝜓))
43elrab 2769 . . . . . 6 (1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (1 ∈ ℕ ∧ 𝜓))
51, 2, 4mpbir2an 888 . . . . 5 1 ∈ {𝑥 ∈ ℕ ∣ 𝜑}
6 elrabi 2766 . . . . . . 7 (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → 𝑦 ∈ ℕ)
7 peano2nn 8406 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
87a1d 22 . . . . . . . . 9 (𝑦 ∈ ℕ → (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ))
9 nnind.6 . . . . . . . . 9 (𝑦 ∈ ℕ → (𝜒𝜃))
108, 9anim12d 328 . . . . . . . 8 (𝑦 ∈ ℕ → ((𝑦 ∈ ℕ ∧ 𝜒) → ((𝑦 + 1) ∈ ℕ ∧ 𝜃)))
11 nnind.2 . . . . . . . . 9 (𝑥 = 𝑦 → (𝜑𝜒))
1211elrab 2769 . . . . . . . 8 (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝑦 ∈ ℕ ∧ 𝜒))
13 nnind.3 . . . . . . . . 9 (𝑥 = (𝑦 + 1) → (𝜑𝜃))
1413elrab 2769 . . . . . . . 8 ((𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ ((𝑦 + 1) ∈ ℕ ∧ 𝜃))
1510, 12, 143imtr4g 203 . . . . . . 7 (𝑦 ∈ ℕ → (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}))
166, 15mpcom 36 . . . . . 6 (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑})
1716rgen 2428 . . . . 5 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}
18 peano5nni 8397 . . . . 5 ((1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ∧ ∀𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}) → ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑})
195, 17, 18mp2an 417 . . . 4 ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑}
2019sseli 3019 . . 3 (𝐴 ∈ ℕ → 𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑})
21 nnind.4 . . . 4 (𝑥 = 𝐴 → (𝜑𝜏))
2221elrab 2769 . . 3 (𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝐴 ∈ ℕ ∧ 𝜏))
2320, 22sylib 120 . 2 (𝐴 ∈ ℕ → (𝐴 ∈ ℕ ∧ 𝜏))
2423simprd 112 1 (𝐴 ∈ ℕ → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103   = wceq 1289  wcel 1438  wral 2359  {crab 2363  wss 2997  (class class class)co 5634  1c1 7330   + caddc 7332  cn 8394
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-cnex 7415  ax-resscn 7416  ax-1re 7418  ax-addrcl 7421
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-rab 2368  df-v 2621  df-un 3001  df-in 3003  df-ss 3010  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-int 3684  df-br 3838  df-iota 4967  df-fv 5010  df-ov 5637  df-inn 8395
This theorem is referenced by:  nnindALT  8411  nn1m1nn  8412  nnaddcl  8414  nnmulcl  8415  nnge1  8417  nn1gt1  8427  nnsub  8432  zaddcllempos  8757  zaddcllemneg  8759  nneoor  8818  peano5uzti  8824  nn0ind-raph  8833  indstr  9050  exbtwnzlemshrink  9625  exp3vallem  9921  expcllem  9931  expap0  9950  iseqcoll  10212  resqrexlemover  10408  resqrexlemlo  10411  resqrexlemcalc3  10414  gcdmultiple  11102  rplpwr  11109  prmind2  11195  prmdvdsexp  11220  sqrt2irr  11234  pw2dvdslemn  11236
  Copyright terms: Public domain W3C validator