This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrdi ⊢ ( 𝑥 ∈ ℕ → ( ( ¬ 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( ¬ 𝜓 → 𝑥 ≤ 𝑦 ) ) → ( 𝜑 ∧ ¬ 𝜑 ) ) )
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 ⊢ ( 𝑥 ∈ ℕ → 𝜑 )