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

Theorem nnind 8756
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 8760 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  |-  ( 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 8751 . . . . . 6  |-  1  e.  NN
2 nnind.5 . . . . . 6  |-  ps
3 nnind.1 . . . . . . 7  |-  ( x  =  1  ->  ( ph 
<->  ps ) )
43elrab 2841 . . . . . 6  |-  ( 1  e.  { x  e.  NN  |  ph }  <->  ( 1  e.  NN  /\  ps ) )
51, 2, 4mpbir2an 927 . . . . 5  |-  1  e.  { x  e.  NN  |  ph }
6 elrabi 2838 . . . . . . 7  |-  ( y  e.  { x  e.  NN  |  ph }  ->  y  e.  NN )
7 peano2nn 8752 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  NN )
87a1d 22 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
y  e.  NN  ->  ( y  +  1 )  e.  NN ) )
9 nnind.6 . . . . . . . . 9  |-  ( y  e.  NN  ->  ( ch  ->  th ) )
108, 9anim12d 333 . . . . . . . 8  |-  ( y  e.  NN  ->  (
( y  e.  NN  /\ 
ch )  ->  (
( y  +  1 )  e.  NN  /\  th ) ) )
11 nnind.2 . . . . . . . . 9  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
1211elrab 2841 . . . . . . . 8  |-  ( y  e.  { x  e.  NN  |  ph }  <->  ( y  e.  NN  /\  ch ) )
13 nnind.3 . . . . . . . . 9  |-  ( x  =  ( y  +  1 )  ->  ( ph 
<->  th ) )
1413elrab 2841 . . . . . . . 8  |-  ( ( y  +  1 )  e.  { x  e.  NN  |  ph }  <->  ( ( y  +  1 )  e.  NN  /\  th ) )
1510, 12, 143imtr4g 204 . . . . . . 7  |-  ( y  e.  NN  ->  (
y  e.  { x  e.  NN  |  ph }  ->  ( y  +  1 )  e.  { x  e.  NN  |  ph }
) )
166, 15mpcom 36 . . . . . 6  |-  ( y  e.  { x  e.  NN  |  ph }  ->  ( y  +  1 )  e.  { x  e.  NN  |  ph }
)
1716rgen 2486 . . . . 5  |-  A. y  e.  { x  e.  NN  |  ph }  ( y  +  1 )  e. 
{ x  e.  NN  |  ph }
18 peano5nni 8743 . . . . 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 423 . . . 4  |-  NN  C_  { x  e.  NN  |  ph }
2019sseli 3094 . . 3  |-  ( A  e.  NN  ->  A  e.  { x  e.  NN  |  ph } )
21 nnind.4 . . . 4  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
2221elrab 2841 . . 3  |-  ( A  e.  { x  e.  NN  |  ph }  <->  ( A  e.  NN  /\  ta ) )
2320, 22sylib 121 . 2  |-  ( A  e.  NN  ->  ( A  e.  NN  /\  ta ) )
2423simprd 113 1  |-  ( A  e.  NN  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1332    e. wcel 1481   A.wral 2417   {crab 2421    C_ wss 3072  (class class class)co 5778   1c1 7641    + caddc 7643   NNcn 8740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4050  ax-cnex 7731  ax-resscn 7732  ax-1re 7734  ax-addrcl 7737
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-rab 2426  df-v 2689  df-un 3076  df-in 3078  df-ss 3085  df-sn 3534  df-pr 3535  df-op 3537  df-uni 3741  df-int 3776  df-br 3934  df-iota 5092  df-fv 5135  df-ov 5781  df-inn 8741
This theorem is referenced by:  nnindALT  8757  nn1m1nn  8758  nnaddcl  8760  nnmulcl  8761  nnge1  8763  nn1gt1  8774  nnsub  8779  zaddcllempos  9111  zaddcllemneg  9113  nneoor  9173  peano5uzti  9179  nn0ind-raph  9188  indstr  9411  exbtwnzlemshrink  10053  exp3vallem  10321  expcllem  10331  expap0  10350  apexp1  10492  seq3coll  10613  resqrexlemover  10810  resqrexlemlo  10813  resqrexlemcalc3  10816  gcdmultiple  11735  rplpwr  11742  prmind2  11828  prmdvdsexp  11853  sqrt2irr  11867  pw2dvdslemn  11870  dvexp  12874
  Copyright terms: Public domain W3C validator