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

Theorem nnind 8924
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 8928 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 8919 . . . . . 6 1 ∈ ℕ
2 nnind.5 . . . . . 6 𝜓
3 nnind.1 . . . . . . 7 (𝑥 = 1 → (𝜑𝜓))
43elrab 2893 . . . . . 6 (1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (1 ∈ ℕ ∧ 𝜓))
51, 2, 4mpbir2an 942 . . . . 5 1 ∈ {𝑥 ∈ ℕ ∣ 𝜑}
6 elrabi 2890 . . . . . . 7 (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → 𝑦 ∈ ℕ)
7 peano2nn 8920 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
87a1d 22 . . . . . . . . 9 (𝑦 ∈ ℕ → (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ))
9 nnind.6 . . . . . . . . 9 (𝑦 ∈ ℕ → (𝜒𝜃))
108, 9anim12d 335 . . . . . . . 8 (𝑦 ∈ ℕ → ((𝑦 ∈ ℕ ∧ 𝜒) → ((𝑦 + 1) ∈ ℕ ∧ 𝜃)))
11 nnind.2 . . . . . . . . 9 (𝑥 = 𝑦 → (𝜑𝜒))
1211elrab 2893 . . . . . . . 8 (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝑦 ∈ ℕ ∧ 𝜒))
13 nnind.3 . . . . . . . . 9 (𝑥 = (𝑦 + 1) → (𝜑𝜃))
1413elrab 2893 . . . . . . . 8 ((𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ ((𝑦 + 1) ∈ ℕ ∧ 𝜃))
1510, 12, 143imtr4g 205 . . . . . . 7 (𝑦 ∈ ℕ → (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}))
166, 15mpcom 36 . . . . . 6 (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑})
1716rgen 2530 . . . . 5 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}
18 peano5nni 8911 . . . . 5 ((1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ∧ ∀𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}) → ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑})
195, 17, 18mp2an 426 . . . 4 ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑}
2019sseli 3151 . . 3 (𝐴 ∈ ℕ → 𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑})
21 nnind.4 . . . 4 (𝑥 = 𝐴 → (𝜑𝜏))
2221elrab 2893 . . 3 (𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝐴 ∈ ℕ ∧ 𝜏))
2320, 22sylib 122 . 2 (𝐴 ∈ ℕ → (𝐴 ∈ ℕ ∧ 𝜏))
2423simprd 114 1 (𝐴 ∈ ℕ → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wcel 2148  wral 2455  {crab 2459  wss 3129  (class class class)co 5869  1c1 7803   + caddc 7805  cn 8908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4118  ax-cnex 7893  ax-resscn 7894  ax-1re 7896  ax-addrcl 7899
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-br 4001  df-iota 5174  df-fv 5220  df-ov 5872  df-inn 8909
This theorem is referenced by:  nnindALT  8925  nn1m1nn  8926  nnaddcl  8928  nnmulcl  8929  nnge1  8931  nn1gt1  8942  nnsub  8947  zaddcllempos  9279  zaddcllemneg  9281  nneoor  9344  peano5uzti  9350  nn0ind-raph  9359  indstr  9582  exbtwnzlemshrink  10235  exp3vallem  10507  expcllem  10517  expap0  10536  apexp1  10682  seq3coll  10806  resqrexlemover  11003  resqrexlemlo  11006  resqrexlemcalc3  11009  gcdmultiple  12004  rplpwr  12011  prmind2  12103  prmdvdsexp  12131  sqrt2irr  12145  pw2dvdslemn  12148  pcmpt  12324  prmpwdvds  12336  mulgnnass  12906  dvexp  13842  2sqlem10  14128
  Copyright terms: Public domain W3C validator