![]() |
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 12232 for an example of its use. See nn0ind 12654 for induction on nonnegative integers and uzind 12651, uzind4 12887 for induction on an arbitrary upper set of integers. See indstr 12897 for strong induction. See also nnindALT 12228. 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 12220 | . . . . . 6 ⊢ 1 ∈ ℕ | |
2 | nnind.5 | . . . . . 6 ⊢ 𝜓 | |
3 | nnind.1 | . . . . . . 7 ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) | |
4 | 3 | elrab 3675 | . . . . . 6 ⊢ (1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (1 ∈ ℕ ∧ 𝜓)) |
5 | 1, 2, 4 | mpbir2an 708 | . . . . 5 ⊢ 1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} |
6 | elrabi 3669 | . . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → 𝑦 ∈ ℕ) | |
7 | peano2nn 12221 | . . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ) | |
8 | 7 | a1d 25 | . . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)) |
9 | nnind.6 | . . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃)) | |
10 | 8, 9 | anim12d 608 | . . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((𝑦 ∈ ℕ ∧ 𝜒) → ((𝑦 + 1) ∈ ℕ ∧ 𝜃))) |
11 | nnind.2 | . . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) | |
12 | 11 | elrab 3675 | . . . . . . . 8 ⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝑦 ∈ ℕ ∧ 𝜒)) |
13 | nnind.3 | . . . . . . . . 9 ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) | |
14 | 13 | elrab 3675 | . . . . . . . 8 ⊢ ((𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ ((𝑦 + 1) ∈ ℕ ∧ 𝜃)) |
15 | 10, 12, 14 | 3imtr4g 296 | . . . . . . 7 ⊢ (𝑦 ∈ ℕ → (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑})) |
16 | 6, 15 | mpcom 38 | . . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}) |
17 | 16 | rgen 3055 | . . . . 5 ⊢ ∀𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑} |
18 | peano5nni 12212 | . . . . 5 ⊢ ((1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ∧ ∀𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}) → ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑}) | |
19 | 5, 17, 18 | mp2an 689 | . . . 4 ⊢ ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑} |
20 | 19 | sseli 3970 | . . 3 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑}) |
21 | nnind.4 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) | |
22 | 21 | elrab 3675 | . . 3 ⊢ (𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝐴 ∈ ℕ ∧ 𝜏)) |
23 | 20, 22 | sylib 217 | . 2 ⊢ (𝐴 ∈ ℕ → (𝐴 ∈ ℕ ∧ 𝜏)) |
24 | 23 | simprd 495 | 1 ⊢ (𝐴 ∈ ℕ → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1533 ∈ wcel 2098 ∀wral 3053 {crab 3424 ⊆ wss 3940 (class class class)co 7401 1c1 11107 + caddc 11109 ℕcn 12209 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-sep 5289 ax-nul 5296 ax-pr 5417 ax-un 7718 ax-1cn 11164 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-ral 3054 df-rex 3063 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-pss 3959 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-iun 4989 df-br 5139 df-opab 5201 df-mpt 5222 df-tr 5256 df-id 5564 df-eprel 5570 df-po 5578 df-so 5579 df-fr 5621 df-we 5623 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6290 df-ord 6357 df-on 6358 df-lim 6359 df-suc 6360 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-ov 7404 df-om 7849 df-2nd 7969 df-frecs 8261 df-wrecs 8292 df-recs 8366 df-rdg 8405 df-nn 12210 |
This theorem is referenced by: nnindALT 12228 nnindd 12229 nn1m1nn 12230 nnaddcl 12232 nnmulcl 12233 nnge1 12237 nnne0 12243 nnsub 12253 nneo 12643 peano5uzi 12648 nn0ind-raph 12659 ser1const 14021 expcllem 14035 expeq0 14055 expmordi 14129 seqcoll 14422 relexpsucnnl 14974 relexpcnv 14979 relexprelg 14982 relexpnndm 14985 relexpaddnn 14995 climcndslem2 15793 sqrt2irr 16189 rplpwr 16496 prmind2 16619 prmdvdsexp 16649 eulerthlem2 16714 pcmpt 16824 prmpwdvds 16836 vdwlem10 16922 mulgnnass 19026 imasdsf1olem 24201 ovolunlem1a 25347 ovolicc2lem3 25370 voliunlem1 25401 volsup 25407 dvexp 25807 plyco 26095 dgrcolem1 26128 vieta1 26166 emcllem6 26849 bposlem5 27137 2sqlem10 27277 dchrisum0flb 27359 iuninc 32261 ofldchr 32898 nexple 33496 esumfzf 33556 rrvsum 33942 subfacp1lem6 34665 cvmliftlem10 34774 bcprod 35203 faclimlem1 35208 incsequz 37106 bfplem1 37180 nnn1suc 41669 nnadd1com 41670 nnaddcom 41671 nnadddir 41673 nnmul1com 41674 nnmulcom 41675 2nn0ind 42173 relexpxpnnidm 42943 relexpss1d 42945 iunrelexpmin1 42948 relexpmulnn 42949 trclrelexplem 42951 iunrelexpmin2 42952 relexp0a 42956 cotrcltrcl 42965 trclimalb2 42966 cotrclrcl 42982 inductionexd 43395 fmuldfeq 44784 dvnmptconst 45142 stoweidlem20 45221 wallispilem4 45269 wallispi2lem1 45272 wallispi2lem2 45273 dirkertrigeqlem1 45299 iccelpart 46586 nn0sumshdiglem2 47496 |
Copyright terms: Public domain | W3C validator |