Metamath Proof Explorer


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 ( 𝑥 ∈ ℕ → 𝜑 )