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

Theorem nnind 7928
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 7932 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 7923 . . . . . 6 1 ∈ ℕ
2 nnind.5 . . . . . 6 𝜓
3 nnind.1 . . . . . . 7 (𝑥 = 1 → (𝜑𝜓))
43elrab 2698 . . . . . 6 (1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (1 ∈ ℕ ∧ 𝜓))
51, 2, 4mpbir2an 849 . . . . 5 1 ∈ {𝑥 ∈ ℕ ∣ 𝜑}
6 elrabi 2695 . . . . . . 7 (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → 𝑦 ∈ ℕ)
7 peano2nn 7924 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
87a1d 22 . . . . . . . . 9 (𝑦 ∈ ℕ → (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ))
9 nnind.6 . . . . . . . . 9 (𝑦 ∈ ℕ → (𝜒𝜃))
108, 9anim12d 318 . . . . . . . 8 (𝑦 ∈ ℕ → ((𝑦 ∈ ℕ ∧ 𝜒) → ((𝑦 + 1) ∈ ℕ ∧ 𝜃)))
11 nnind.2 . . . . . . . . 9 (𝑥 = 𝑦 → (𝜑𝜒))
1211elrab 2698 . . . . . . . 8 (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝑦 ∈ ℕ ∧ 𝜒))
13 nnind.3 . . . . . . . . 9 (𝑥 = (𝑦 + 1) → (𝜑𝜃))
1413elrab 2698 . . . . . . . 8 ((𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ ((𝑦 + 1) ∈ ℕ ∧ 𝜃))
1510, 12, 143imtr4g 194 . . . . . . 7 (𝑦 ∈ ℕ → (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}))
166, 15mpcom 32 . . . . . 6 (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑})
1716rgen 2374 . . . . 5 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}
18 peano5nni 7915 . . . . 5 ((1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ∧ ∀𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}) → ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑})
195, 17, 18mp2an 402 . . . 4 ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑}
2019sseli 2941 . . 3 (𝐴 ∈ ℕ → 𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑})
21 nnind.4 . . . 4 (𝑥 = 𝐴 → (𝜑𝜏))
2221elrab 2698 . . 3 (𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝐴 ∈ ℕ ∧ 𝜏))
2320, 22sylib 127 . 2 (𝐴 ∈ ℕ → (𝐴 ∈ ℕ ∧ 𝜏))
2423simprd 107 1 (𝐴 ∈ ℕ → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wb 98   = wceq 1243  wcel 1393  wral 2306  {crab 2310  wss 2917  (class class class)co 5512  1c1 6888   + caddc 6890  cn 7912
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 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-cnex 6973  ax-resscn 6974  ax-1re 6976  ax-addrcl 6979
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-rab 2315  df-v 2559  df-un 2922  df-in 2924  df-ss 2931  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-int 3616  df-br 3765  df-iota 4867  df-fv 4910  df-ov 5515  df-inn 7913
This theorem is referenced by:  nnindALT  7929  nn1m1nn  7930  nnaddcl  7932  nnmulcl  7933  nnge1  7935  nn1gt1  7945  nnsub  7950  zaddcllempos  8280  zaddcllemneg  8282  nneoor  8338  peano5uzti  8344  nn0ind-raph  8353  indstr  8534  qbtwnzlemshrink  9102  expivallem  9230  expcllem  9240  expap0  9259  resqrexlemover  9582  resqrexlemlo  9585  resqrexlemcalc3  9588  sqrt2irr  9852
  Copyright terms: Public domain W3C validator