indstr

Description: Strong Mathematical Induction for positive integers (inference schema). (Contributed by NM, 17-Aug-2001)

	Ref	Expression
Hypotheses	indstr.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
	indstr.2	$⊢ x \in ℕ \to (\forall y \in ℕ (y < x \to ψ) \to φ)$
Assertion	indstr	$⊢ x \in ℕ \to φ$

Proof

Step	Hyp	Ref	Expression
1		indstr.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2		indstr.2	$⊢ x \in ℕ \to (\forall y \in ℕ (y < x \to ψ) \to φ)$
3		pm3.24	$⊢ \neg (φ \land \neg φ)$
4		nnre	$⊢ x \in ℕ \to x \in ℝ$
5		nnre	$⊢ y \in ℕ \to y \in ℝ$
6		lenlt	$⊢ (x \in ℝ \land y \in ℝ) \to (x \leq y \leftrightarrow \neg y < x)$
7	4 5 6	syl2an	$⊢ (x \in ℕ \land y \in ℕ) \to (x \leq y \leftrightarrow \neg y < x)$
8	7	imbi2d	$⊢ (x \in ℕ \land y \in ℕ) \to ((\neg ψ \to x \leq y) \leftrightarrow (\neg ψ \to \neg y < x))$
9		con34b	$⊢ (y < x \to ψ) \leftrightarrow (\neg ψ \to \neg y < x)$
10	8 9	bitr4di	$⊢ (x \in ℕ \land y \in ℕ) \to ((\neg ψ \to x \leq y) \leftrightarrow (y < x \to ψ))$
11	10	ralbidva	$⊢ x \in ℕ \to (\forall y \in ℕ (\neg ψ \to x \leq y) \leftrightarrow \forall y \in ℕ (y < x \to ψ))$
12	11 2	sylbid	$⊢ x \in ℕ \to (\forall y \in ℕ (\neg ψ \to x \leq y) \to φ)$
13	12	anim2d	$⊢ x \in ℕ \to ((\neg φ \land \forall y \in ℕ (\neg ψ \to x \leq y)) \to (\neg φ \land φ))$
14		ancom	$⊢ (\neg φ \land φ) \leftrightarrow (φ \land \neg φ)$
15	13 14	imbitrdi	$⊢ x \in ℕ \to ((\neg φ \land \forall y \in ℕ (\neg ψ \to x \leq y)) \to (φ \land \neg φ))$
16	3 15	mtoi	$⊢ x \in ℕ \to \neg (\neg φ \land \forall y \in ℕ (\neg ψ \to x \leq y))$
17	16	nrex	$⊢ \neg \exists x \in ℕ (\neg φ \land \forall y \in ℕ (\neg ψ \to x \leq y))$
18	1	notbid	$⊢ x = y \to (\neg φ \leftrightarrow \neg ψ)$
19	18	nnwos	$⊢ \exists x \in ℕ \neg φ \to \exists x \in ℕ (\neg φ \land \forall y \in ℕ (\neg ψ \to x \leq y))$
20	17 19	mto	$⊢ \neg \exists x \in ℕ \neg φ$
21		dfral2	$⊢ \forall x \in ℕ φ \leftrightarrow \neg \exists x \in ℕ \neg φ$
22	20 21	mpbir	$⊢ \forall x \in ℕ φ$
23	22	rspec	$⊢ x \in ℕ \to φ$

Metamath Proof Explorer

Theorem indstr

Proof