Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nnind | Structured version Visualization version GIF version |
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 11663 for an example of its use. See nn0ind 12080 for induction on nonnegative integers and uzind 12077, uzind4 12309 for induction on an arbitrary upper set of integers. See indstr 12319 for strong induction. See also nnindALT 11660. This is an alternative for Metamath 100 proof #74. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.) |
Ref | Expression |
---|---|
nnind.1 | ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) |
nnind.2 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
nnind.3 | ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) |
nnind.4 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) |
nnind.5 | ⊢ 𝜓 |
nnind.6 | ⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃)) |
Ref | Expression |
---|---|
nnind | ⊢ (𝐴 ∈ ℕ → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1nn 11652 | . . . . . 6 ⊢ 1 ∈ ℕ | |
2 | nnind.5 | . . . . . 6 ⊢ 𝜓 | |
3 | nnind.1 | . . . . . . 7 ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) | |
4 | 3 | elrab 3683 | . . . . . 6 ⊢ (1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (1 ∈ ℕ ∧ 𝜓)) |
5 | 1, 2, 4 | mpbir2an 709 | . . . . 5 ⊢ 1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} |
6 | elrabi 3678 | . . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → 𝑦 ∈ ℕ) | |
7 | peano2nn 11653 | . . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ) | |
8 | 7 | a1d 25 | . . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)) |
9 | nnind.6 | . . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃)) | |
10 | 8, 9 | anim12d 610 | . . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((𝑦 ∈ ℕ ∧ 𝜒) → ((𝑦 + 1) ∈ ℕ ∧ 𝜃))) |
11 | nnind.2 | . . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) | |
12 | 11 | elrab 3683 | . . . . . . . 8 ⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝑦 ∈ ℕ ∧ 𝜒)) |
13 | nnind.3 | . . . . . . . . 9 ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) | |
14 | 13 | elrab 3683 | . . . . . . . 8 ⊢ ((𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ ((𝑦 + 1) ∈ ℕ ∧ 𝜃)) |
15 | 10, 12, 14 | 3imtr4g 298 | . . . . . . 7 ⊢ (𝑦 ∈ ℕ → (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑})) |
16 | 6, 15 | mpcom 38 | . . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}) |
17 | 16 | rgen 3151 | . . . . 5 ⊢ ∀𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑} |
18 | peano5nni 11644 | . . . . 5 ⊢ ((1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ∧ ∀𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}) → ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑}) | |
19 | 5, 17, 18 | mp2an 690 | . . . 4 ⊢ ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑} |
20 | 19 | sseli 3966 | . . 3 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑}) |
21 | nnind.4 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) | |
22 | 21 | elrab 3683 | . . 3 ⊢ (𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝐴 ∈ ℕ ∧ 𝜏)) |
23 | 20, 22 | sylib 220 | . 2 ⊢ (𝐴 ∈ ℕ → (𝐴 ∈ ℕ ∧ 𝜏)) |
24 | 23 | simprd 498 | 1 ⊢ (𝐴 ∈ ℕ → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1536 ∈ wcel 2113 ∀wral 3141 {crab 3145 ⊆ wss 3939 (class class class)co 7159 1c1 10541 + caddc 10543 ℕcn 11641 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-sep 5206 ax-nul 5213 ax-pow 5269 ax-pr 5333 ax-un 7464 ax-1cn 10598 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ne 3020 df-ral 3146 df-rex 3147 df-reu 3148 df-rab 3150 df-v 3499 df-sbc 3776 df-csb 3887 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-pss 3957 df-nul 4295 df-if 4471 df-pw 4544 df-sn 4571 df-pr 4573 df-tp 4575 df-op 4577 df-uni 4842 df-iun 4924 df-br 5070 df-opab 5132 df-mpt 5150 df-tr 5176 df-id 5463 df-eprel 5468 df-po 5477 df-so 5478 df-fr 5517 df-we 5519 df-xp 5564 df-rel 5565 df-cnv 5566 df-co 5567 df-dm 5568 df-rn 5569 df-res 5570 df-ima 5571 df-pred 6151 df-ord 6197 df-on 6198 df-lim 6199 df-suc 6200 df-iota 6317 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-ov 7162 df-om 7584 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-nn 11642 |
This theorem is referenced by: nnindALT 11660 nn1m1nn 11661 nnaddcl 11663 nnmulcl 11664 nnge1 11668 nnne0 11674 nnsub 11684 nneo 12069 peano5uzi 12074 nn0ind-raph 12085 ser1const 13429 expcllem 13443 expeq0 13462 expmordi 13534 seqcoll 13825 relexpsucnnl 14394 relexpcnv 14397 relexprelg 14400 relexpnndm 14403 relexpaddnn 14413 climcndslem2 15208 sqrt2irr 15605 gcdmultipleOLD 15903 rplpwr 15910 prmind2 16032 prmdvdsexp 16062 eulerthlem2 16122 pcmpt 16231 prmpwdvds 16243 vdwlem10 16329 mulgnnass 18265 imasdsf1olem 22986 ovolunlem1a 24100 ovolicc2lem3 24123 voliunlem1 24154 volsup 24160 dvexp 24553 plyco 24834 dgrcolem1 24866 vieta1 24904 emcllem6 25581 bposlem5 25867 2sqlem10 26007 dchrisum0flb 26089 iuninc 30315 nnindd 30539 ofldchr 30891 nexple 31272 esumfzf 31332 rrvsum 31716 subfacp1lem6 32436 cvmliftlem10 32545 bcprod 32974 faclimlem1 32979 incsequz 35027 bfplem1 35104 nnn1suc 39165 nnadd1com 39166 nnaddcom 39167 nnadddir 39169 nnmul1com 39170 nnmulcom 39171 2nn0ind 39548 relexpxpnnidm 40054 relexpss1d 40056 iunrelexpmin1 40059 relexpmulnn 40060 trclrelexplem 40062 iunrelexpmin2 40063 relexp0a 40067 cotrcltrcl 40076 trclimalb2 40077 cotrclrcl 40093 inductionexd 40511 fmuldfeq 41870 dvnmptconst 42232 stoweidlem20 42312 wallispilem4 42360 wallispi2lem1 42363 wallispi2lem2 42364 dirkertrigeqlem1 42390 iccelpart 43600 nn0sumshdiglem2 44689 |
Copyright terms: Public domain | W3C validator |