![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nn0ind | Structured version Visualization version Unicode version |
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.) |
Ref | Expression |
---|---|
nn0ind.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
nn0ind.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
nn0ind.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
nn0ind.4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
nn0ind.5 |
![]() ![]() |
nn0ind.6 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nn0ind |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elnn0z 10984 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 0z 10982 |
. . 3
![]() ![]() ![]() ![]() | |
3 | nn0ind.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | nn0ind.2 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | nn0ind.3 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | nn0ind.4 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | nn0ind.5 |
. . . . 5
![]() ![]() | |
8 | 7 | a1i 11 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | elnn0z 10984 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | nn0ind.6 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 9, 10 | sylbir 218 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 11 | 3adant1 1032 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 3, 4, 5, 6, 8, 12 | uzind 11061 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 2, 13 | mp3an1 1360 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 1, 14 | sylbi 200 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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 |
Copyright terms: Public domain | W3C validator |