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

Theorem nnind 9766
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 9770 for an example of its use. See nn0ind 10110 for induction on nonnegative integers and uzind 10105, uzind4 10278 for induction on an arbitrary set of upper integers. See indstr 10289 for strong induction. See also nnindALT 9767. (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 9759 . . . . . 6  |-  1  e.  NN
2 nnind.5 . . . . . 6  |-  ps
3 nnind.1 . . . . . . 7  |-  ( x  =  1  ->  ( ph 
<->  ps ) )
43elrab 2925 . . . . . 6  |-  ( 1  e.  { x  e.  NN  |  ph }  <->  ( 1  e.  NN  /\  ps ) )
51, 2, 4mpbir2an 886 . . . . 5  |-  1  e.  { x  e.  NN  |  ph }
6 ssrab2 3260 . . . . . . . 8  |-  { x  e.  NN  |  ph }  C_  NN
76sseli 3178 . . . . . . 7  |-  ( y  e.  { x  e.  NN  |  ph }  ->  y  e.  NN )
8 peano2nn 9760 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  NN )
98a1d 22 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
y  e.  NN  ->  ( y  +  1 )  e.  NN ) )
10 nnind.6 . . . . . . . . 9  |-  ( y  e.  NN  ->  ( ch  ->  th ) )
119, 10anim12d 546 . . . . . . . 8  |-  ( y  e.  NN  ->  (
( y  e.  NN  /\ 
ch )  ->  (
( y  +  1 )  e.  NN  /\  th ) ) )
12 nnind.2 . . . . . . . . 9  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
1312elrab 2925 . . . . . . . 8  |-  ( y  e.  { x  e.  NN  |  ph }  <->  ( y  e.  NN  /\  ch ) )
14 nnind.3 . . . . . . . . 9  |-  ( x  =  ( y  +  1 )  ->  ( ph 
<->  th ) )
1514elrab 2925 . . . . . . . 8  |-  ( ( y  +  1 )  e.  { x  e.  NN  |  ph }  <->  ( ( y  +  1 )  e.  NN  /\  th ) )
1611, 13, 153imtr4g 261 . . . . . . 7  |-  ( y  e.  NN  ->  (
y  e.  { x  e.  NN  |  ph }  ->  ( y  +  1 )  e.  { x  e.  NN  |  ph }
) )
177, 16mpcom 32 . . . . . 6  |-  ( y  e.  { x  e.  NN  |  ph }  ->  ( y  +  1 )  e.  { x  e.  NN  |  ph }
)
1817rgen 2610 . . . . 5  |-  A. y  e.  { x  e.  NN  |  ph }  ( y  +  1 )  e. 
{ x  e.  NN  |  ph }
19 peano5nni 9751 . . . . 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 } )
205, 18, 19mp2an 653 . . . 4  |-  NN  C_  { x  e.  NN  |  ph }
2120sseli 3178 . . 3  |-  ( A  e.  NN  ->  A  e.  { x  e.  NN  |  ph } )
22 nnind.4 . . . 4  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
2322elrab 2925 . . 3  |-  ( A  e.  { x  e.  NN  |  ph }  <->  ( A  e.  NN  /\  ta ) )
2421, 23sylib 188 . 2  |-  ( A  e.  NN  ->  ( A  e.  NN  /\  ta ) )
2524simprd 449 1  |-  ( A  e.  NN  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1625    e. wcel 1686   A.wral 2545   {crab 2549    C_ wss 3154  (class class class)co 5860   1c1 8740    + caddc 8742   NNcn 9748
This theorem is referenced by:  nnindALT  9767  nn1m1nn  9768  nnaddcl  9770  nnmulcl  9771  nnge1  9774  nnsub  9786  nneo  10097  peano5uzi  10102  uzindOLD  10108  nn0ind-raph  10114  ser1const  11104  expcllem  11116  expeq0  11134  seqcoll  11403  climcndslem2  12311  sqr2irr  12529  gcdmultiple  12731  rplpwr  12737  prmind2  12771  prmdvdsexp  12795  eulerthlem2  12852  pcmpt  12942  prmpwdvds  12953  vdwlem10  13039  mulgnnass  14597  imasdsf1olem  17939  ovolunlem1a  18857  ovolicc2lem3  18880  voliunlem1  18909  volsup  18915  dvexp  19304  plyco  19625  dgrcolem1  19656  vieta1  19694  emcllem6  20296  bposlem5  20529  2sqlem10  20615  dchrisum0flb  20661  iuninc  23160  subfacp1lem6  23718  cvmliftlem10  23827  incsequz  26469  bfplem1  26557  2nn0ind  27041  expmordi  27043  fmuldfeq  27724  stoweidlem20  27780  wallispilem4  27828  wallispi2lem1  27831  wallispi2lem2  27832
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514  ax-1cn 8797
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4307  df-id 4311  df-po 4316  df-so 4317  df-fr 4354  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-ov 5863  df-recs 6390  df-rdg 6425  df-nn 9749
  Copyright terms: Public domain W3C validator