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 x = y φ ψ
indstr.2 x y y < x ψ φ
Assertion indstr x φ

Proof

Step Hyp Ref Expression
1 indstr.1 x = y φ ψ
2 indstr.2 x y y < x ψ φ
3 pm3.24 ¬ φ ¬ φ
4 nnre x x
5 nnre y y
6 lenlt x y x y ¬ y < x
7 4 5 6 syl2an x y x y ¬ y < x
8 7 imbi2d x y ¬ ψ x y ¬ ψ ¬ y < x
9 con34b y < x ψ ¬ ψ ¬ y < x
10 8 9 bitr4di x y ¬ ψ x y y < x ψ
11 10 ralbidva x y ¬ ψ x y y y < x ψ
12 11 2 sylbid x y ¬ ψ x y φ
13 12 anim2d x ¬ φ y ¬ ψ x y ¬ φ φ
14 ancom ¬ φ φ φ ¬ φ
15 13 14 syl6ib x ¬ φ y ¬ ψ x y φ ¬ φ
16 3 15 mtoi x ¬ ¬ φ y ¬ ψ x y
17 16 nrex ¬ x ¬ φ y ¬ ψ x y
18 1 notbid x = y ¬ φ ¬ ψ
19 18 nnwos x ¬ φ x ¬ φ y ¬ ψ x y
20 17 19 mto ¬ x ¬ φ
21 dfral2 x φ ¬ x ¬ φ
22 20 21 mpbir x φ
23 22 rspec x φ