Theorem indstr

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

	Ref	Expression
Hypotheses	indstr.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	indstr.2	⊢ ( 𝑥 ∈ ℕ → ( ∀ 𝑦 ∈ ℕ ( 𝑦 < 𝑥 → 𝜓 ) → 𝜑 ) )
Assertion	indstr	⊢ ( 𝑥 ∈ ℕ → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		indstr.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		indstr.2	⊢ ( 𝑥 ∈ ℕ → ( ∀ 𝑦 ∈ ℕ ( 𝑦 < 𝑥 → 𝜓 ) → 𝜑 ) )
3		pm3.24	⊢ ¬ ( 𝜑 ∧ ¬ 𝜑 )
4		nnre	⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℝ )
5		nnre	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
6		lenlt	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑥 ) )
7	4 5 6	syl2an	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( 𝑥 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑥 ) )
8	7	imbi2d	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( ( ¬ 𝜓 → 𝑥 ≤ 𝑦 ) ↔ ( ¬ 𝜓 → ¬ 𝑦 < 𝑥 ) ) )
9		con34b	⊢ ( ( 𝑦 < 𝑥 → 𝜓 ) ↔ ( ¬ 𝜓 → ¬ 𝑦 < 𝑥 ) )
10	8 9	bitr4di	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( ( ¬ 𝜓 → 𝑥 ≤ 𝑦 ) ↔ ( 𝑦 < 𝑥 → 𝜓 ) ) )
11	10	ralbidva	⊢ ( 𝑥 ∈ ℕ → ( ∀ 𝑦 ∈ ℕ ( ¬ 𝜓 → 𝑥 ≤ 𝑦 ) ↔ ∀ 𝑦 ∈ ℕ ( 𝑦 < 𝑥 → 𝜓 ) ) )
12	11 2	sylbid	⊢ ( 𝑥 ∈ ℕ → ( ∀ 𝑦 ∈ ℕ ( ¬ 𝜓 → 𝑥 ≤ 𝑦 ) → 𝜑 ) )
13	12	anim2d	⊢ ( 𝑥 ∈ ℕ → ( ( ¬ 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( ¬ 𝜓 → 𝑥 ≤ 𝑦 ) ) → ( ¬ 𝜑 ∧ 𝜑 ) ) )
14		ancom	⊢ ( ( ¬ 𝜑 ∧ 𝜑 ) ↔ ( 𝜑 ∧ ¬ 𝜑 ) )
15	13 14	syl6ib	⊢ ( 𝑥 ∈ ℕ → ( ( ¬ 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( ¬ 𝜓 → 𝑥 ≤ 𝑦 ) ) → ( 𝜑 ∧ ¬ 𝜑 ) ) )
16	3 15	mtoi	⊢ ( 𝑥 ∈ ℕ → ¬ ( ¬ 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( ¬ 𝜓 → 𝑥 ≤ 𝑦 ) ) )
17	16	nrex	⊢ ¬ ∃ 𝑥 ∈ ℕ ( ¬ 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( ¬ 𝜓 → 𝑥 ≤ 𝑦 ) )
18	1	notbid	⊢ ( 𝑥 = 𝑦 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
19	18	nnwos	⊢ ( ∃ 𝑥 ∈ ℕ ¬ 𝜑 → ∃ 𝑥 ∈ ℕ ( ¬ 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( ¬ 𝜓 → 𝑥 ≤ 𝑦 ) ) )
20	17 19	mto	⊢ ¬ ∃ 𝑥 ∈ ℕ ¬ 𝜑
21		dfral2	⊢ ( ∀ 𝑥 ∈ ℕ 𝜑 ↔ ¬ ∃ 𝑥 ∈ ℕ ¬ 𝜑 )
22	20 21	mpbir	⊢ ∀ 𝑥 ∈ ℕ 𝜑
23	22	rspec	⊢ ( 𝑥 ∈ ℕ → 𝜑 )