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