| 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 12168 for an example of its use. See nn0ind 12587 for induction on nonnegative integers and uzind 12584, uzind4 12819 for induction on an arbitrary upper set of integers. See indstr 12829 for strong induction. See also nnindALT 12164. 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 12156 | . . . . . 6 ⊢ 1 ∈ ℕ | |
| 2 | nnind.5 | . . . . . 6 ⊢ 𝜓 | |
| 3 | nnind.1 | . . . . . . 7 ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) | |
| 4 | 3 | elrab 3646 | . . . . . 6 ⊢ (1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (1 ∈ ℕ ∧ 𝜓)) |
| 5 | 1, 2, 4 | mpbir2an 711 | . . . . 5 ⊢ 1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} |
| 6 | elrabi 3642 | . . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → 𝑦 ∈ ℕ) | |
| 7 | peano2nn 12157 | . . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ) | |
| 8 | 7 | a1d 25 | . . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)) |
| 9 | nnind.6 | . . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃)) | |
| 10 | 8, 9 | anim12d 609 | . . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((𝑦 ∈ ℕ ∧ 𝜒) → ((𝑦 + 1) ∈ ℕ ∧ 𝜃))) |
| 11 | nnind.2 | . . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) | |
| 12 | 11 | elrab 3646 | . . . . . . . 8 ⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝑦 ∈ ℕ ∧ 𝜒)) |
| 13 | nnind.3 | . . . . . . . . 9 ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) | |
| 14 | 13 | elrab 3646 | . . . . . . . 8 ⊢ ((𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ ((𝑦 + 1) ∈ ℕ ∧ 𝜃)) |
| 15 | 10, 12, 14 | 3imtr4g 296 | . . . . . . 7 ⊢ (𝑦 ∈ ℕ → (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑})) |
| 16 | 6, 15 | mpcom 38 | . . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}) |
| 17 | 16 | rgen 3053 | . . . . 5 ⊢ ∀𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑} |
| 18 | peano5nni 12148 | . . . . 5 ⊢ ((1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ∧ ∀𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}) → ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑}) | |
| 19 | 5, 17, 18 | mp2an 692 | . . . 4 ⊢ ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑} |
| 20 | 19 | sseli 3929 | . . 3 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑}) |
| 21 | nnind.4 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) | |
| 22 | 21 | elrab 3646 | . . 3 ⊢ (𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝐴 ∈ ℕ ∧ 𝜏)) |
| 23 | 20, 22 | sylib 218 | . 2 ⊢ (𝐴 ∈ ℕ → (𝐴 ∈ ℕ ∧ 𝜏)) |
| 24 | 23 | simprd 495 | 1 ⊢ (𝐴 ∈ ℕ → 𝜏) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ∀wral 3051 {crab 3399 ⊆ wss 3901 (class class class)co 7358 1c1 11027 + caddc 11029 ℕcn 12145 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pr 5377 ax-un 7680 ax-1cn 11084 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7361 df-om 7809 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-nn 12146 |
| This theorem is referenced by: nnindALT 12164 nnindd 12165 nn1m1nn 12166 nnaddcl 12168 nnmulcl 12169 nnge1 12173 nnne0 12179 nnsub 12189 nneo 12576 peano5uzi 12581 nn0ind-raph 12592 ser1const 13981 expcllem 13995 expeq0 14015 expmordi 14090 seqcoll 14387 relexpsucnnl 14953 relexpcnv 14958 relexprelg 14961 relexpnndm 14964 relexpaddnn 14974 climcndslem2 15773 sqrt2irr 16174 rplpwr 16485 prmind2 16612 prmdvdsexp 16642 eulerthlem2 16709 pcmpt 16820 prmpwdvds 16832 vdwlem10 16918 mulgnnass 19039 ofldchr 21531 imasdsf1olem 24317 ovolunlem1a 25453 ovolicc2lem3 25476 voliunlem1 25507 volsup 25513 dvexp 25913 plyco 26202 dgrcolem1 26235 vieta1 26276 emcllem6 26967 bposlem5 27255 2sqlem10 27395 dchrisum0flb 27477 iuninc 32635 nexple 32925 esumfzf 34226 rrvsum 34611 subfacp1lem6 35379 cvmliftlem10 35488 bcprod 35932 faclimlem1 35937 incsequz 37949 bfplem1 38023 nnn1suc 42521 nnadd1com 42522 nnaddcom 42523 nnadddir 42525 nnmul1com 42526 nnmulcom 42527 2nn0ind 43187 relexpxpnnidm 43944 relexpss1d 43946 iunrelexpmin1 43949 relexpmulnn 43950 trclrelexplem 43952 iunrelexpmin2 43953 relexp0a 43957 cotrcltrcl 43966 trclimalb2 43967 cotrclrcl 43983 inductionexd 44396 fmuldfeq 45829 dvnmptconst 46185 stoweidlem20 46264 wallispilem4 46312 wallispi2lem1 46315 wallispi2lem2 46316 dirkertrigeqlem1 46342 iccelpart 47679 nn0sumshdiglem2 48868 |
| Copyright terms: Public domain | W3C validator |