Theorem nn0ind 11064

Description: Principle of Mathematical Induction (inference schema) on nonnegative integers. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by NM, 13-May-2004.)

Hypotheses

Ref	Expression
nn0ind.1	|- ( x = 0 -> ( ph <-> ps ) )
nn0ind.2	|- ( x = y -> ( ph <-> ch ) )
nn0ind.3	|- ( x = ( y + 1 ) -> ( ph <-> th ) )
nn0ind.4	|- ( x = A -> ( ph <-> ta ) )
nn0ind.5	|- ps
nn0ind.6	|- ( y e. NN0 -> ( ch -> th ) )

Assertion

Ref	Expression
nn0ind	|- ( A e. NN0 -> 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 nn0ind

Step	Hyp	Ref	Expression
1		elnn0z 10984	. 2 |- ( A e. NN0 <-> ( A e. ZZ /\ 0 <_ A ) )
2		0z 10982	. . 3 |- 0 e. ZZ
3		nn0ind.1	. . . 4 |- ( x = 0 -> ( ph <-> ps ) )
4		nn0ind.2	. . . 4 |- ( x = y -> ( ph <-> ch ) )
5		nn0ind.3	. . . 4 |- ( x = ( y + 1 ) -> ( ph <-> th ) )
6		nn0ind.4	. . . 4 |- ( x = A -> ( ph <-> ta ) )
7		nn0ind.5	. . . . 5 |- ps
8	7	a1i 11	. . . 4 |- ( 0 e. ZZ -> ps )
9		elnn0z 10984	. . . . . 6 |- ( y e. NN0 <-> ( y e. ZZ /\ 0 <_ y ) )
10		nn0ind.6	. . . . . 6 |- ( y e. NN0 -> ( ch -> th ) )
11	9, 10	sylbir 218	. . . . 5 |- ( ( y e. ZZ /\ 0 <_ y ) -> ( ch -> th ) )
12	11	3adant1 1032	. . . 4 |- ( ( 0 e. ZZ /\ y e. ZZ /\ 0 <_ y ) -> ( ch -> th ) )
13	3, 4, 5, 6, 8, 12	uzind 11061	. . 3 |- ( ( 0 e. ZZ /\ A e. ZZ /\ 0 <_ A ) -> ta )
14	2, 13	mp3an1 1360	. 2 |- ( ( A e. ZZ /\ 0 <_ A ) -> ta )
15	1, 14	sylbi 200	1 |- ( A e. NN0 -> ta )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1455   e. wcel 1898   class class class wbr 4418  (class class class)co 6320   0cc0 9570   1c1 9571   + caddc 9573   <_ cle 9707   NN0cn0 10903   ZZcz 10971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-er 7394  df-en 7601  df-dom 7602  df-sdom 7603  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-nn 10643  df-n0 10904  df-z 10972

This theorem is referenced by:  nn0indALT  11065  nn0indd  11066  zindd  11070  fzennn  12219  mulexp  12349  expadd  12352  expmul  12355  leexp1a  12369  bernneq  12436  modexp  12445  faccl  12507  facdiv  12510  facwordi  12512  faclbnd  12513  faclbnd6  12522  facubnd  12523  bccl  12545  brfi1indALT  12692  wrdind  12876  wrd2ind  12877  cshweqrep  12963  rtrclreclem4  13179  relexpindlem  13181  cjexp  13268  absexp  13422  iseraltlem2  13804  binom  13943  bcxmas  13948  climcndslem1  13962  binomfallfac  14149  demoivreALT  14310  ruclem8  14344  odd2np1lem  14419  bitsinv1  14471  sadcadd  14487  sadadd2  14489  saddisjlem  14493  smu01lem  14514  smumullem  14521  alginv  14589  prmfac1  14726  pcfac  14899  ramcl  15042  mhmmulg  16845  psgnunilem3  17192  sylow1lem1  17305  efgsrel  17439  efgsfo  17444  efgred  17453  srgmulgass  17819  srgpcomp  17820  srgbinom  17833  lmodvsmmulgdi  18181  assamulgscm  18629  mplcoe3  18745  cnfldexp  19056  tmdmulg  21162  expcn  21959  dvnadd  22939  dvnres  22941  dvnfre  22962  ply1divex  23143  fta1g  23174  plyco  23251  dgrco  23285  dvnply2  23296  plydivex  23306  fta1  23317  cxpmul2  23690  facgam  24047  dchrisumlem1  24383  qabvle  24519  qabvexp  24520  ostth2lem2  24528  rusgranumwlk  25741  eupath2  25764  ex-ind-dvds  25955  gxnn0add  26058  gxnn0mul  26061  subfacval2  29960  cvmliftlem7  30064  bccolsum  30425  faclim  30432  faclim2  30434  heiborlem4  32192  mzpexpmpt  35633  pell14qrexpclnn0  35758  rmxypos  35843  jm2.17a  35856  jm2.17b  35857  rmygeid  35860  jm2.19lem3  35892  hbtlem5  36033  cnsrexpcl  36077  relexpiidm  36342  fperiodmullem  37596  m1expevenOLD  37756  stoweidlem17  37978  stoweidlem19  37980  wallispilem3  38030  lmodvsmdi  40536