| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > nnindALT | Structured version Visualization version GIF version | ||
| Description: Principle of Mathematical
Induction (inference schema). The last four
hypotheses give us the substitution instances we need; the first two are
the induction step and the basis.
This ALT version of nnind 12180 has a different hypothesis order. It may be easier to use with the Metamath program Proof Assistant, because "MM-PA> ASSIGN LAST" will be applied to the substitution instances first. We may eventually use this one as the official version. You may use either version. After the proof is complete, the ALT version can be changed to the non-ALT version with "MM-PA> MINIMIZE_WITH nnind / MAYGROW". (Contributed by NM, 7-Dec-2005.) (New usage is discouraged.) (Proof modification is discouraged.) |
| Ref | Expression |
|---|---|
| nnindALT.6 | ⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃)) |
| nnindALT.5 | ⊢ 𝜓 |
| nnindALT.1 | ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) |
| nnindALT.2 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
| nnindALT.3 | ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) |
| nnindALT.4 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) |
| Ref | Expression |
|---|---|
| nnindALT | ⊢ (𝐴 ∈ ℕ → 𝜏) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nnindALT.1 | . 2 ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) | |
| 2 | nnindALT.2 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) | |
| 3 | nnindALT.3 | . 2 ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) | |
| 4 | nnindALT.4 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) | |
| 5 | nnindALT.5 | . 2 ⊢ 𝜓 | |
| 6 | nnindALT.6 | . 2 ⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃)) | |
| 7 | 1, 2, 3, 4, 5, 6 | nnind 12180 | 1 ⊢ (𝐴 ∈ ℕ → 𝜏) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2109 (class class class)co 7369 1c1 11045 + caddc 11047 ℕcn 12162 |
| 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 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5246 ax-nul 5256 ax-pr 5382 ax-un 7691 ax-1cn 11102 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-ov 7372 df-om 7823 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-nn 12163 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |