MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnind Structured version   Visualization version   GIF version

Theorem nnind 11238
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 11242 for an example of its use. See nn0ind 11672 for induction on nonnegative integers and uzind 11669, uzind4 11946 for induction on an arbitrary upper set of integers. See indstr 11957 for strong induction. See also nnindALT 11239. 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 11231 . . . . . 6 1 ∈ ℕ
2 nnind.5 . . . . . 6 𝜓
3 nnind.1 . . . . . . 7 (𝑥 = 1 → (𝜑𝜓))
43elrab 3515 . . . . . 6 (1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (1 ∈ ℕ ∧ 𝜓))
51, 2, 4mpbir2an 690 . . . . 5 1 ∈ {𝑥 ∈ ℕ ∣ 𝜑}
6 elrabi 3510 . . . . . . 7 (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → 𝑦 ∈ ℕ)
7 peano2nn 11232 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
87a1d 25 . . . . . . . . 9 (𝑦 ∈ ℕ → (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ))
9 nnind.6 . . . . . . . . 9 (𝑦 ∈ ℕ → (𝜒𝜃))
108, 9anim12d 596 . . . . . . . 8 (𝑦 ∈ ℕ → ((𝑦 ∈ ℕ ∧ 𝜒) → ((𝑦 + 1) ∈ ℕ ∧ 𝜃)))
11 nnind.2 . . . . . . . . 9 (𝑥 = 𝑦 → (𝜑𝜒))
1211elrab 3515 . . . . . . . 8 (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝑦 ∈ ℕ ∧ 𝜒))
13 nnind.3 . . . . . . . . 9 (𝑥 = (𝑦 + 1) → (𝜑𝜃))
1413elrab 3515 . . . . . . . 8 ((𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ ((𝑦 + 1) ∈ ℕ ∧ 𝜃))
1510, 12, 143imtr4g 285 . . . . . . 7 (𝑦 ∈ ℕ → (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}))
166, 15mpcom 38 . . . . . 6 (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑})
1716rgen 3071 . . . . 5 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}
18 peano5nni 11223 . . . . 5 ((1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ∧ ∀𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}) → ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑})
195, 17, 18mp2an 672 . . . 4 ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑}
2019sseli 3748 . . 3 (𝐴 ∈ ℕ → 𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑})
21 nnind.4 . . . 4 (𝑥 = 𝐴 → (𝜑𝜏))
2221elrab 3515 . . 3 (𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝐴 ∈ ℕ ∧ 𝜏))
2320, 22sylib 208 . 2 (𝐴 ∈ ℕ → (𝐴 ∈ ℕ ∧ 𝜏))
2423simprd 483 1 (𝐴 ∈ ℕ → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  wral 3061  {crab 3065  wss 3723  (class class class)co 6791  1c1 10137   + caddc 10139  cn 11220
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7094  ax-1cn 10194
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5821  df-ord 5867  df-on 5868  df-lim 5869  df-suc 5870  df-iota 5992  df-fun 6031  df-fn 6032  df-f 6033  df-f1 6034  df-fo 6035  df-f1o 6036  df-fv 6037  df-ov 6794  df-om 7211  df-wrecs 7557  df-recs 7619  df-rdg 7657  df-nn 11221
This theorem is referenced by:  nnindALT  11239  nn1m1nn  11240  nnaddcl  11242  nnmulcl  11243  nnge1  11246  nnsub  11259  nneo  11661  peano5uzi  11666  nn0ind-raph  11677  ser1const  13057  expcllem  13071  expeq0  13090  seqcoll  13443  relexpsucnnl  13973  relexpcnv  13976  relexprelg  13979  relexpnndm  13982  relexpaddnn  13992  climcndslem2  14782  sqrt2irr  15178  gcdmultiple  15470  rplpwr  15477  prmind2  15598  prmdvdsexp  15627  eulerthlem2  15687  pcmpt  15796  prmpwdvds  15808  vdwlem10  15894  mulgnnass  17777  mulgnnassOLD  17778  imasdsf1olem  22391  ovolunlem1a  23477  ovolicc2lem3  23500  voliunlem1  23531  volsup  23537  dvexp  23929  plyco  24210  dgrcolem1  24242  vieta1  24280  emcllem6  24941  bposlem5  25227  2sqlem10  25367  dchrisum0flb  25413  iuninc  29710  nnindd  29899  ofldchr  30147  nexple  30404  esumfzf  30464  rrvsum  30849  subfacp1lem6  31498  cvmliftlem10  31607  bcprod  31955  faclimlem1  31960  incsequz  33869  bfplem1  33946  2nn0ind  38029  expmordi  38031  relexpxpnnidm  38514  relexpss1d  38516  iunrelexpmin1  38519  relexpmulnn  38520  trclrelexplem  38522  iunrelexpmin2  38523  relexp0a  38527  cotrcltrcl  38536  trclimalb2  38537  cotrclrcl  38553  inductionexd  38972  fmuldfeq  40326  dvnmptconst  40667  stoweidlem20  40747  wallispilem4  40795  wallispi2lem1  40798  wallispi2lem2  40799  dirkertrigeqlem1  40825  iccelpart  41890  nn0sumshdiglem2  42937
  Copyright terms: Public domain W3C validator