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

Theorem nnind 9697
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 9701 for an example of its use. See nn0ind 10040 for induction on nonnegative integers and uzind 10035, uzind4 10208 for induction on an arbitrary set of upper integers. See indstr 10219 for strong induction. (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 9690 . . . . . 6  |-  1  e.  NN
2 nnind.5 . . . . . 6  |-  ps
3 nnind.1 . . . . . . 7  |-  ( x  =  1  ->  ( ph 
<->  ps ) )
43elrab 2874 . . . . . 6  |-  ( 1  e.  { x  e.  NN  |  ph }  <->  ( 1  e.  NN  /\  ps ) )
51, 2, 4mpbir2an 891 . . . . 5  |-  1  e.  { x  e.  NN  |  ph }
6 ssrab2 3200 . . . . . . . 8  |-  { x  e.  NN  |  ph }  C_  NN
76sseli 3118 . . . . . . 7  |-  ( y  e.  { x  e.  NN  |  ph }  ->  y  e.  NN )
8 peano2nn 9691 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  NN )
98a1d 24 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
y  e.  NN  ->  ( y  +  1 )  e.  NN ) )
10 nnind.6 . . . . . . . . 9  |-  ( y  e.  NN  ->  ( ch  ->  th ) )
119, 10anim12d 548 . . . . . . . 8  |-  ( y  e.  NN  ->  (
( y  e.  NN  /\ 
ch )  ->  (
( y  +  1 )  e.  NN  /\  th ) ) )
12 nnind.2 . . . . . . . . 9  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
1312elrab 2874 . . . . . . . 8  |-  ( y  e.  { x  e.  NN  |  ph }  <->  ( y  e.  NN  /\  ch ) )
14 nnind.3 . . . . . . . . 9  |-  ( x  =  ( y  +  1 )  ->  ( ph 
<->  th ) )
1514elrab 2874 . . . . . . . 8  |-  ( ( y  +  1 )  e.  { x  e.  NN  |  ph }  <->  ( ( y  +  1 )  e.  NN  /\  th ) )
1611, 13, 153imtr4g 263 . . . . . . 7  |-  ( y  e.  NN  ->  (
y  e.  { x  e.  NN  |  ph }  ->  ( y  +  1 )  e.  { x  e.  NN  |  ph }
) )
177, 16mpcom 34 . . . . . 6  |-  ( y  e.  { x  e.  NN  |  ph }  ->  ( y  +  1 )  e.  { x  e.  NN  |  ph }
)
1817rgen 2579 . . . . 5  |-  A. y  e.  { x  e.  NN  |  ph }  ( y  +  1 )  e. 
{ x  e.  NN  |  ph }
19 peano5nni 9682 . . . . 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 656 . . . 4  |-  NN  C_  { x  e.  NN  |  ph }
2120sseli 3118 . . 3  |-  ( A  e.  NN  ->  A  e.  { x  e.  NN  |  ph } )
22 nnind.4 . . . 4  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
2322elrab 2874 . . 3  |-  ( A  e.  { x  e.  NN  |  ph }  <->  ( A  e.  NN  /\  ta ) )
2421, 23sylib 190 . 2  |-  ( A  e.  NN  ->  ( A  e.  NN  /\  ta ) )
2524simprd 451 1  |-  ( A  e.  NN  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360    = wceq 1619    e. wcel 1621   A.wral 2516   {crab 2519    C_ wss 3094  (class class class)co 5757   1c1 8671    + caddc 8673   NNcn 9679
This theorem is referenced by:  nnindALT  9698  nn1m1nn  9699  nnaddcl  9701  nnmulcl  9702  nnge1  9705  nnsub  9717  nneo  10027  peano5uzi  10032  uzindOLD  10038  nn0ind-raph  10044  ser1const  11033  expcllem  11045  expeq0  11063  seqcoll  11331  climcndslem2  12236  sqr2irr  12454  gcdmultiple  12656  rplpwr  12662  prmind2  12696  prmdvdsexp  12720  eulerthlem2  12777  pcmpt  12867  prmpwdvds  12878  vdwlem10  12964  mulgnnass  14522  imasdsf1olem  17864  ovolunlem1a  18782  ovolicc2lem3  18805  voliunlem1  18834  volsup  18840  dvexp  19229  plyco  19550  dgrcolem1  19581  vieta1  19619  emcllem6  20221  bposlem5  20454  2sqlem10  20540  dchrisum0flb  20586  subfacp1lem6  23053  cvmliftlem10  23162  incsequz  25790  bfplem1  25878  2nn0ind  26362  expmordi  26364  fmuldfeq  27046  stoweidlem20  27069
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4081  ax-nul 4089  ax-pr 4152  ax-un 4449  ax-1cn 8728
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2520  df-rex 2521  df-reu 2522  df-rab 2523  df-v 2742  df-sbc 2936  df-csb 3024  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-pss 3110  df-nul 3398  df-if 3507  df-pw 3568  df-sn 3587  df-pr 3588  df-tp 3589  df-op 3590  df-uni 3769  df-iun 3848  df-br 3964  df-opab 4018  df-mpt 4019  df-tr 4054  df-eprel 4242  df-id 4246  df-po 4251  df-so 4252  df-fr 4289  df-we 4291  df-ord 4332  df-on 4333  df-lim 4334  df-suc 4335  df-om 4594  df-xp 4640  df-rel 4641  df-cnv 4642  df-co 4643  df-dm 4644  df-rn 4645  df-res 4646  df-ima 4647  df-fun 4648  df-fn 4649  df-f 4650  df-f1 4651  df-fo 4652  df-f1o 4653  df-fv 4654  df-ov 5760  df-recs 6321  df-rdg 6356  df-n 9680
  Copyright terms: Public domain W3C validator