![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nn0ind | 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 8753 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 0z 8751 |
. . 3
![]() ![]() ![]() ![]() | |
3 | nn0ind.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | nn0ind.2 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | nn0ind.3 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | nn0ind.4 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | nn0ind.5 |
. . . . 5
![]() ![]() | |
8 | 7 | a1i 9 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | elnn0z 8753 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | nn0ind.6 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 9, 10 | sylbir 133 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 11 | 3adant1 961 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 3, 4, 5, 6, 8, 12 | uzind 8847 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 2, 13 | mp3an1 1260 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 1, 14 | sylbi 119 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 579 ax-in2 580 ax-io 665 ax-5 1381 ax-7 1382 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-8 1440 ax-10 1441 ax-11 1442 ax-i12 1443 ax-bndl 1444 ax-4 1445 ax-13 1449 ax-14 1450 ax-17 1464 ax-i9 1468 ax-ial 1472 ax-i5r 1473 ax-ext 2070 ax-sep 3955 ax-pow 4007 ax-pr 4034 ax-un 4258 ax-setind 4351 ax-cnex 7426 ax-resscn 7427 ax-1cn 7428 ax-1re 7429 ax-icn 7430 ax-addcl 7431 ax-addrcl 7432 ax-mulcl 7433 ax-addcom 7435 ax-addass 7437 ax-distr 7439 ax-i2m1 7440 ax-0lt1 7441 ax-0id 7443 ax-rnegex 7444 ax-cnre 7446 ax-pre-ltirr 7447 ax-pre-ltwlin 7448 ax-pre-lttrn 7449 ax-pre-ltadd 7451 |
This theorem depends on definitions: df-bi 115 df-3or 925 df-3an 926 df-tru 1292 df-fal 1295 df-nf 1395 df-sb 1693 df-eu 1951 df-mo 1952 df-clab 2075 df-cleq 2081 df-clel 2084 df-nfc 2217 df-ne 2256 df-nel 2351 df-ral 2364 df-rex 2365 df-reu 2366 df-rab 2368 df-v 2621 df-sbc 2841 df-dif 3001 df-un 3003 df-in 3005 df-ss 3012 df-pw 3429 df-sn 3450 df-pr 3451 df-op 3453 df-uni 3652 df-int 3687 df-br 3844 df-opab 3898 df-id 4118 df-xp 4442 df-rel 4443 df-cnv 4444 df-co 4445 df-dm 4446 df-iota 4975 df-fun 5012 df-fv 5018 df-riota 5600 df-ov 5647 df-oprab 5648 df-mpt2 5649 df-pnf 7514 df-mnf 7515 df-xr 7516 df-ltxr 7517 df-le 7518 df-sub 7645 df-neg 7646 df-inn 8413 df-n0 8664 df-z 8741 |
This theorem is referenced by: zindd 8854 uzaddcl 9064 frecfzennn 9821 mulexp 9982 expadd 9985 expmul 9988 leexp1a 9998 bernneq 10062 faccl 10131 facdiv 10134 facwordi 10136 faclbnd 10137 faclbnd6 10140 facubnd 10141 bccl 10163 cjexp 10315 absexp 10500 binom 10865 bcxmas 10870 demoivreALT 11050 odd2np1lem 11137 ialginv 11294 prmfac1 11396 |
Copyright terms: Public domain | W3C validator |