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 ⊢ ( 𝑥 = 1 → ( 𝜑 ↔ 𝜒 ) )
indstr2.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
indstr2.3 ⊢ 𝜒
indstr2.4 ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) → ( ∀ 𝑦 ∈ ℕ ( 𝑦 < 𝑥 → 𝜓 ) → 𝜑 ) )
Assertion indstr2 ( 𝑥 ∈ ℕ → 𝜑 )

Proof

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