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 φ