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

Metamath Proof Explorer

Theorem 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 → φ ↔ χ
indstr2.2 ⊢ x = y → φ ↔ ψ
indstr2.3 ⊢ χ
indstr2.4 ⊢ x ∈ ℤ ≥ 2 → ∀ y ∈ ℕ y < x → ψ → φ
Assertion indstr2 ⊢ x ∈ ℕ → φ

Proof

Step Hyp Ref Expression
1 indstr2.1 ⊢ x = 1 → φ ↔ χ
2 indstr2.2 ⊢ x = y → φ ↔ ψ
3 indstr2.3 ⊢ χ
4 indstr2.4 ⊢ x ∈ ℤ ≥ 2 → ∀ y ∈ ℕ y < x → ψ → φ
5 elnn1uz2 ⊢ x ∈ ℕ ↔ x = 1 ∨ x ∈ ℤ ≥ 2
6 nnnlt1 ⊢ y ∈ ℕ → ¬ y < 1
7 6 adantl ⊢ x = 1 ∧ y ∈ ℕ → ¬ y < 1
8 breq2 ⊢ x = 1 → y < x ↔ y < 1
9 8 adantr ⊢ x = 1 ∧ y ∈ ℕ → y < x ↔ y < 1
10 7 9 mtbird ⊢ x = 1 ∧ y ∈ ℕ → ¬ y < x
11 10 pm2.21d ⊢ x = 1 ∧ y ∈ ℕ → y < x → ψ
12 11 ralrimiva ⊢ x = 1 → ∀ y ∈ ℕ y < x → ψ
13 pm5.5 ⊢ ∀ y ∈ ℕ y < x → ψ → ∀ y ∈ ℕ y < x → ψ → φ ↔ φ
14 12 13 syl ⊢ x = 1 → ∀ y ∈ ℕ y < x → ψ → φ ↔ φ
15 14 1 bitrd ⊢ x = 1 → ∀ y ∈ ℕ y < x → ψ → φ ↔ χ
16 3 15 mpbiri ⊢ x = 1 → ∀ y ∈ ℕ y < x → ψ → φ
17 16 4 jaoi ⊢ x = 1 ∨ x ∈ ℤ ≥ 2 → ∀ y ∈ ℕ y < x → ψ → φ
18 5 17 sylbi ⊢ x ∈ ℕ → ∀ y ∈ ℕ y < x → ψ → φ
19 2 18 indstr ⊢ x ∈ ℕ → φ