indstr2

Description: Strong Mathematical Induction for positive integers (inference schema). The first two hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by Paul Chapman, 21-Nov-2012)

	Ref	Expression
Hypotheses	indstr2.1	$⊢ x = 1 \to (φ \leftrightarrow χ)$
	indstr2.2	$⊢ x = y \to (φ \leftrightarrow ψ)$
	indstr2.3	$⊢ χ$
	indstr2.4	$⊢ x \in ℤ_{\geq 2} \to (\forall y \in ℕ (y < x \to ψ) \to φ)$
Assertion	indstr2	$⊢ x \in ℕ \to φ$

Proof

Step	Hyp	Ref	Expression
1		indstr2.1	$⊢ x = 1 \to (φ \leftrightarrow χ)$
2		indstr2.2	$⊢ x = y \to (φ \leftrightarrow ψ)$
3		indstr2.3	$⊢ χ$
4		indstr2.4	$⊢ x \in ℤ_{\geq 2} \to (\forall y \in ℕ (y < x \to ψ) \to φ)$
5		elnn1uz2	$⊢ x \in ℕ \leftrightarrow (x = 1 \lor x \in ℤ_{\geq 2})$
6		nnnlt1	$⊢ y \in ℕ \to \neg y < 1$
7	6	adantl	$⊢ (x = 1 \land y \in ℕ) \to \neg y < 1$
8		breq2	$⊢ x = 1 \to (y < x \leftrightarrow y < 1)$
9	8	adantr	$⊢ (x = 1 \land y \in ℕ) \to (y < x \leftrightarrow y < 1)$
10	7 9	mtbird	$⊢ (x = 1 \land y \in ℕ) \to \neg y < x$
11	10	pm2.21d	$⊢ (x = 1 \land y \in ℕ) \to (y < x \to ψ)$
12	11	ralrimiva	$⊢ x = 1 \to \forall y \in ℕ (y < x \to ψ)$
13		pm5.5	$⊢ \forall y \in ℕ (y < x \to ψ) \to ((\forall y \in ℕ (y < x \to ψ) \to φ) \leftrightarrow φ)$
14	12 13	syl	$⊢ x = 1 \to ((\forall y \in ℕ (y < x \to ψ) \to φ) \leftrightarrow φ)$
15	14 1	bitrd	$⊢ x = 1 \to ((\forall y \in ℕ (y < x \to ψ) \to φ) \leftrightarrow χ)$
16	3 15	mpbiri	$⊢ x = 1 \to (\forall y \in ℕ (y < x \to ψ) \to φ)$
17	16 4	jaoi	$⊢ (x = 1 \lor x \in ℤ_{\geq 2}) \to (\forall y \in ℕ (y < x \to ψ) \to φ)$
18	5 17	sylbi	$⊢ x \in ℕ \to (\forall y \in ℕ (y < x \to ψ) \to φ)$
19	2 18	indstr	$⊢ x \in ℕ \to φ$

Metamath Proof Explorer

Theorem indstr2

Proof