Theorem nn0ind 10896

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 10816	. 2 |- ( A e. NN0 <-> ( A e. ZZ /\ 0 <_ A ) )
2		0z 10814	. . 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 10816	. . . . . 6 |- ( y e. NN0 <-> ( y e. ZZ /\ 0 <_ y ) )
10		nn0ind.6	. . . . . 6 |- ( y e. NN0 -> ( ch -> th ) )
11	9, 10	sylbir 213	. . . . 5 |- ( ( y e. ZZ /\ 0 <_ y ) -> ( ch -> th ) )
12	11	3adant1 1012	. . . 4 |- ( ( 0 e. ZZ /\ y e. ZZ /\ 0 <_ y ) -> ( ch -> th ) )
13	3, 4, 5, 6, 8, 12	uzind 10893	. . 3 |- ( ( 0 e. ZZ /\ A e. ZZ /\ 0 <_ A ) -> ta )
14	2, 13	mp3an1 1309	. 2 |- ( ( A e. ZZ /\ 0 <_ A ) -> ta )
15	1, 14	sylbi 195	1 |- ( A e. NN0 -> ta )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   = wceq 1399   e. wcel 1836   class class class wbr 4384  (class class class)co 6218   0cc0 9425   1c1 9426   + caddc 9428   <_ cle 9562   NN0cn0 10734   ZZcz 10803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618  ax-un 6513  ax-resscn 9482  ax-1cn 9483  ax-icn 9484  ax-addcl 9485  ax-addrcl 9486  ax-mulcl 9487  ax-mulrcl 9488  ax-mulcom 9489  ax-addass 9490  ax-mulass 9491  ax-distr 9492  ax-i2m1 9493  ax-1ne0 9494  ax-1rid 9495  ax-rnegex 9496  ax-rrecex 9497  ax-cnre 9498  ax-pre-lttri 9499  ax-pre-lttrn 9500  ax-pre-ltadd 9501  ax-pre-mulgt0 9502

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-nel 2594  df-ral 2751  df-rex 2752  df-reu 2753  df-rab 2755  df-v 3053  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3729  df-if 3875  df-pw 3946  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-uni 4181  df-iun 4262  df-br 4385  df-opab 4443  df-mpt 4444  df-tr 4478  df-eprel 4722  df-id 4726  df-po 4731  df-so 4732  df-fr 4769  df-we 4771  df-ord 4812  df-on 4813  df-lim 4814  df-suc 4815  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-res 4942  df-ima 4943  df-iota 5477  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-riota 6180  df-ov 6221  df-oprab 6222  df-mpt2 6223  df-om 6622  df-recs 6982  df-rdg 7016  df-er 7251  df-en 7458  df-dom 7459  df-sdom 7460  df-pnf 9563  df-mnf 9564  df-xr 9565  df-ltxr 9566  df-le 9567  df-sub 9742  df-neg 9743  df-nn 10475  df-n0 10735  df-z 10804

This theorem is referenced by:  nn0indALT  10897  nn0indd  10898  zindd  10902  fzennn  12004  mulexp  12131  expadd  12134  expmul  12137  leexp1a  12150  bernneq  12217  modexp  12226  faccl  12288  facdiv  12290  facwordi  12292  faclbnd  12293  faclbnd6  12302  facubnd  12303  bccl  12325  wrdind  12636  wrd2ind  12637  cshweqrep  12723  rtrclreclem4  12919  relexpindlem  12921  cjexp  13008  absexp  13162  iseraltlem2  13530  binom  13667  bcxmas  13672  climcndslem1  13686  demoivreALT  13961  ruclem8  13995  odd2np1lem  14070  bitsinv1  14117  sadcadd  14133  sadadd2  14135  saddisjlem  14139  smu01lem  14160  smumullem  14167  alginv  14229  prmfac1  14284  pcfac  14443  ramcl  14572  mhmmulg  16314  psgnunilem3  16661  sylow1lem1  16758  efgsrel  16892  efgsfo  16897  efgred  16906  srgmulgass  17318  srgpcomp  17319  srgbinom  17332  lmodvsmmulgdi  17683  assamulgscm  18135  mplcoe3  18264  mplcoe3OLD  18265  cnfldexp  18587  tmdmulg  20699  expcn  21484  dvnadd  22440  dvnres  22442  dvnfre  22463  ply1divex  22645  fta1g  22676  plyco  22746  dgrco  22780  dvnply2  22791  plydivex  22801  fta1  22812  cxpmul2  23180  dchrisumlem1  23814  qabvle  23950  qabvexp  23951  ostth2lem2  23959  rusgranumwlk  25103  eupath2  25126  ex-ind-dvds  25316  gxnn0add  25418  gxnn0mul  25421  facgam  28837  subfacval2  28860  cvmliftlem7  28965  binomfallfac  29369  faclim  29377  faclim2  29379  heiborlem4  30516  mzpexpmpt  30883  pell14qrexpclnn0  31007  rmxypos  31090  jm2.17a  31103  jm2.17b  31104  rmygeid  31107  jm2.19lem3  31139  hbtlem5  31285  cnsrexpcl  31322  fperiodmullem  31708  m1expeven  31790  stoweidlem17  32004  stoweidlem19  32006  wallispilem3  32054  lmodvsmdi  33214  relexpiidm  38279