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 11752 for an example of its use. See nn0ind 12171 for induction on nonnegative integers and uzind 12168, uzind4 12401 for induction on an arbitrary upper set of integers. See indstr 12411 for strong induction. See also nnindALT 11748. 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 11740 | . . . . . 6 ⊢ 1 ∈ ℕ | |
2 | nnind.5 | . . . . . 6 ⊢ 𝜓 | |
3 | nnind.1 | . . . . . . 7 ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) | |
4 | 3 | elrab 3593 | . . . . . 6 ⊢ (1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (1 ∈ ℕ ∧ 𝜓)) |
5 | 1, 2, 4 | mpbir2an 711 | . . . . 5 ⊢ 1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} |
6 | elrabi 3587 | . . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → 𝑦 ∈ ℕ) | |
7 | peano2nn 11741 | . . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ) | |
8 | 7 | a1d 25 | . . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)) |
9 | nnind.6 | . . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃)) | |
10 | 8, 9 | anim12d 612 | . . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((𝑦 ∈ ℕ ∧ 𝜒) → ((𝑦 + 1) ∈ ℕ ∧ 𝜃))) |
11 | nnind.2 | . . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) | |
12 | 11 | elrab 3593 | . . . . . . . 8 ⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝑦 ∈ ℕ ∧ 𝜒)) |
13 | nnind.3 | . . . . . . . . 9 ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) | |
14 | 13 | elrab 3593 | . . . . . . . 8 ⊢ ((𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ ((𝑦 + 1) ∈ ℕ ∧ 𝜃)) |
15 | 10, 12, 14 | 3imtr4g 299 | . . . . . . 7 ⊢ (𝑦 ∈ ℕ → (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑})) |
16 | 6, 15 | mpcom 38 | . . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}) |
17 | 16 | rgen 3064 | . . . . 5 ⊢ ∀𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑} |
18 | peano5nni 11732 | . . . . 5 ⊢ ((1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ∧ ∀𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}) → ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑}) | |
19 | 5, 17, 18 | mp2an 692 | . . . 4 ⊢ ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑} |
20 | 19 | sseli 3883 | . . 3 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑}) |
21 | nnind.4 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) | |
22 | 21 | elrab 3593 | . . 3 ⊢ (𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝐴 ∈ ℕ ∧ 𝜏)) |
23 | 20, 22 | sylib 221 | . 2 ⊢ (𝐴 ∈ ℕ → (𝐴 ∈ ℕ ∧ 𝜏)) |
24 | 23 | simprd 499 | 1 ⊢ (𝐴 ∈ ℕ → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1542 ∈ wcel 2114 ∀wral 3054 {crab 3058 ⊆ wss 3853 (class class class)co 7183 1c1 10629 + caddc 10631 ℕcn 11729 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2711 ax-sep 5177 ax-nul 5184 ax-pr 5306 ax-un 7492 ax-1cn 10686 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2541 df-eu 2571 df-clab 2718 df-cleq 2731 df-clel 2812 df-nfc 2882 df-ne 2936 df-ral 3059 df-rex 3060 df-reu 3061 df-rab 3063 df-v 3402 df-sbc 3686 df-csb 3801 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-pss 3872 df-nul 4222 df-if 4425 df-pw 4500 df-sn 4527 df-pr 4529 df-tp 4531 df-op 4533 df-uni 4807 df-iun 4893 df-br 5041 df-opab 5103 df-mpt 5121 df-tr 5147 df-id 5439 df-eprel 5444 df-po 5452 df-so 5453 df-fr 5493 df-we 5495 df-xp 5541 df-rel 5542 df-cnv 5543 df-co 5544 df-dm 5545 df-rn 5546 df-res 5547 df-ima 5548 df-pred 6139 df-ord 6186 df-on 6187 df-lim 6188 df-suc 6189 df-iota 6308 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-fv 6358 df-ov 7186 df-om 7613 df-wrecs 7989 df-recs 8050 df-rdg 8088 df-nn 11730 |
This theorem is referenced by: nnindALT 11748 nnindd 11749 nn1m1nn 11750 nnaddcl 11752 nnmulcl 11753 nnge1 11757 nnne0 11763 nnsub 11773 nneo 12160 peano5uzi 12165 nn0ind-raph 12176 ser1const 13531 expcllem 13545 expeq0 13564 expmordi 13636 seqcoll 13929 relexpsucnnl 14492 relexpcnv 14497 relexprelg 14500 relexpnndm 14503 relexpaddnn 14513 climcndslem2 15311 sqrt2irr 15707 gcdmultipleOLD 16009 rplpwr 16016 prmind2 16139 prmdvdsexp 16169 eulerthlem2 16232 pcmpt 16341 prmpwdvds 16353 vdwlem10 16439 mulgnnass 18393 imasdsf1olem 23139 ovolunlem1a 24261 ovolicc2lem3 24284 voliunlem1 24315 volsup 24321 dvexp 24718 plyco 25003 dgrcolem1 25035 vieta1 25073 emcllem6 25751 bposlem5 26037 2sqlem10 26177 dchrisum0flb 26259 iuninc 30487 ofldchr 31103 nexple 31560 esumfzf 31620 rrvsum 32004 subfacp1lem6 32731 cvmliftlem10 32840 bcprod 33290 faclimlem1 33295 incsequz 35562 bfplem1 35636 nnn1suc 39913 nnadd1com 39914 nnaddcom 39915 nnadddir 39917 nnmul1com 39918 nnmulcom 39919 2nn0ind 40380 relexpxpnnidm 40898 relexpss1d 40900 iunrelexpmin1 40903 relexpmulnn 40904 trclrelexplem 40906 iunrelexpmin2 40907 relexp0a 40911 cotrcltrcl 40920 trclimalb2 40921 cotrclrcl 40937 inductionexd 41352 fmuldfeq 42707 dvnmptconst 43065 stoweidlem20 43144 wallispilem4 43192 wallispi2lem1 43195 wallispi2lem2 43196 dirkertrigeqlem1 43222 iccelpart 44467 nn0sumshdiglem2 45550 |
Copyright terms: Public domain | W3C validator |