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

Theorem nnind 9950
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 hypothesis. See nnaddcl 9954 for an example of its use. See nn0ind 10298 for induction on nonnegative integers and uzind 10293, uzind4 10466 for induction on an arbitrary set of upper integers. See indstr 10477 for strong induction. See also nnindALT 9951. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.)
Hypotheses
Ref Expression
nnind.1  |-  ( x  =  1  ->  ( ph 
<->  ps ) )
nnind.2  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
nnind.3  |-  ( x  =  ( y  +  1 )  ->  ( ph 
<->  th ) )
nnind.4  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
nnind.5  |-  ps
nnind.6  |-  ( y  e.  NN  ->  ( ch  ->  th ) )
Assertion
Ref Expression
nnind  |-  ( A  e.  NN  ->  ta )
Distinct variable groups:    x, y    x, A    ps, x    ch, x    th, x    ta, x    ph, y
Allowed substitution hints:    ph( x)    ps( y)    ch( y)    th( y)    ta( y)    A( y)

Proof of Theorem nnind
StepHypRef Expression
1 1nn 9943 . . . . . 6  |-  1  e.  NN
2 nnind.5 . . . . . 6  |-  ps
3 nnind.1 . . . . . . 7  |-  ( x  =  1  ->  ( ph 
<->  ps ) )
43elrab 3035 . . . . . 6  |-  ( 1  e.  { x  e.  NN  |  ph }  <->  ( 1  e.  NN  /\  ps ) )
51, 2, 4mpbir2an 887 . . . . 5  |-  1  e.  { x  e.  NN  |  ph }
6 elrabi 3033 . . . . . . 7  |-  ( y  e.  { x  e.  NN  |  ph }  ->  y  e.  NN )
7 peano2nn 9944 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  NN )
87a1d 23 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
y  e.  NN  ->  ( y  +  1 )  e.  NN ) )
9 nnind.6 . . . . . . . . 9  |-  ( y  e.  NN  ->  ( ch  ->  th ) )
108, 9anim12d 547 . . . . . . . 8  |-  ( y  e.  NN  ->  (
( y  e.  NN  /\ 
ch )  ->  (
( y  +  1 )  e.  NN  /\  th ) ) )
11 nnind.2 . . . . . . . . 9  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
1211elrab 3035 . . . . . . . 8  |-  ( y  e.  { x  e.  NN  |  ph }  <->  ( y  e.  NN  /\  ch ) )
13 nnind.3 . . . . . . . . 9  |-  ( x  =  ( y  +  1 )  ->  ( ph 
<->  th ) )
1413elrab 3035 . . . . . . . 8  |-  ( ( y  +  1 )  e.  { x  e.  NN  |  ph }  <->  ( ( y  +  1 )  e.  NN  /\  th ) )
1510, 12, 143imtr4g 262 . . . . . . 7  |-  ( y  e.  NN  ->  (
y  e.  { x  e.  NN  |  ph }  ->  ( y  +  1 )  e.  { x  e.  NN  |  ph }
) )
166, 15mpcom 34 . . . . . 6  |-  ( y  e.  { x  e.  NN  |  ph }  ->  ( y  +  1 )  e.  { x  e.  NN  |  ph }
)
1716rgen 2714 . . . . 5  |-  A. y  e.  { x  e.  NN  |  ph }  ( y  +  1 )  e. 
{ x  e.  NN  |  ph }
18 peano5nni 9935 . . . . 5  |-  ( ( 1  e.  { x  e.  NN  |  ph }  /\  A. y  e.  {
x  e.  NN  |  ph }  ( y  +  1 )  e.  {
x  e.  NN  |  ph } )  ->  NN  C_ 
{ x  e.  NN  |  ph } )
195, 17, 18mp2an 654 . . . 4  |-  NN  C_  { x  e.  NN  |  ph }
2019sseli 3287 . . 3  |-  ( A  e.  NN  ->  A  e.  { x  e.  NN  |  ph } )
21 nnind.4 . . . 4  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
2221elrab 3035 . . 3  |-  ( A  e.  { x  e.  NN  |  ph }  <->  ( A  e.  NN  /\  ta ) )
2320, 22sylib 189 . 2  |-  ( A  e.  NN  ->  ( A  e.  NN  /\  ta ) )
2423simprd 450 1  |-  ( A  e.  NN  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   A.wral 2649   {crab 2653    C_ wss 3263  (class class class)co 6020   1c1 8924    + caddc 8926   NNcn 9932
This theorem is referenced by:  nnindALT  9951  nn1m1nn  9952  nnaddcl  9954  nnmulcl  9955  nnge1  9958  nnsub  9970  nneo  10285  peano5uzi  10290  uzindOLD  10296  nn0ind-raph  10302  ser1const  11306  expcllem  11319  expeq0  11337  seqcoll  11639  climcndslem2  12557  sqr2irr  12775  gcdmultiple  12977  rplpwr  12983  prmind2  13017  prmdvdsexp  13041  eulerthlem2  13098  pcmpt  13188  prmpwdvds  13199  vdwlem10  13285  mulgnnass  14845  imasdsf1olem  18311  ovolunlem1a  19259  ovolicc2lem3  19282  voliunlem1  19311  volsup  19317  dvexp  19706  plyco  20027  dgrcolem1  20058  vieta1  20096  emcllem6  20706  bposlem5  20939  2sqlem10  21025  dchrisum0flb  21071  iuninc  23855  ofldchr  24070  esumfzf  24255  rrvsum  24491  subfacp1lem6  24650  cvmliftlem10  24760  faclimlem1  25120  incsequz  26143  bfplem1  26222  2nn0ind  26699  expmordi  26701  fmuldfeq  27381  stoweidlem20  27437  wallispilem4  27485  wallispi2lem1  27488  wallispi2lem2  27489
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641  ax-1cn 8981
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-reu 2656  df-rab 2658  df-v 2901  df-sbc 3105  df-csb 3195  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-pss 3279  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-tp 3765  df-op 3766  df-uni 3958  df-iun 4037  df-br 4154  df-opab 4208  df-mpt 4209  df-tr 4244  df-eprel 4435  df-id 4439  df-po 4444  df-so 4445  df-fr 4482  df-we 4484  df-ord 4525  df-on 4526  df-lim 4527  df-suc 4528  df-om 4786  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831  df-iota 5358  df-fun 5396  df-fn 5397  df-f 5398  df-f1 5399  df-fo 5400  df-f1o 5401  df-fv 5402  df-ov 6023  df-recs 6569  df-rdg 6604  df-nn 9933
  Copyright terms: Public domain W3C validator