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 -> ( ph <-> ps ) )
indstr.2
|- ( x e. NN -> ( A. y e. NN ( y < x -> ps ) -> ph ) )
Assertion indstr
|- ( x e. NN -> ph )

Proof

Step Hyp Ref Expression
1 indstr.1
 |-  ( x = y -> ( ph <-> ps ) )
2 indstr.2
 |-  ( x e. NN -> ( A. y e. NN ( y < x -> ps ) -> ph ) )
3 pm3.24
 |-  -. ( ph /\ -. ph )
4 nnre
 |-  ( x e. NN -> x e. RR )
5 nnre
 |-  ( y e. NN -> y e. RR )
6 lenlt
 |-  ( ( x e. RR /\ y e. RR ) -> ( x <_ y <-> -. y < x ) )
7 4 5 6 syl2an
 |-  ( ( x e. NN /\ y e. NN ) -> ( x <_ y <-> -. y < x ) )
8 7 imbi2d
 |-  ( ( x e. NN /\ y e. NN ) -> ( ( -. ps -> x <_ y ) <-> ( -. ps -> -. y < x ) ) )
9 con34b
 |-  ( ( y < x -> ps ) <-> ( -. ps -> -. y < x ) )
10 8 9 bitr4di
 |-  ( ( x e. NN /\ y e. NN ) -> ( ( -. ps -> x <_ y ) <-> ( y < x -> ps ) ) )
11 10 ralbidva
 |-  ( x e. NN -> ( A. y e. NN ( -. ps -> x <_ y ) <-> A. y e. NN ( y < x -> ps ) ) )
12 11 2 sylbid
 |-  ( x e. NN -> ( A. y e. NN ( -. ps -> x <_ y ) -> ph ) )
13 12 anim2d
 |-  ( x e. NN -> ( ( -. ph /\ A. y e. NN ( -. ps -> x <_ y ) ) -> ( -. ph /\ ph ) ) )
14 ancom
 |-  ( ( -. ph /\ ph ) <-> ( ph /\ -. ph ) )
15 13 14 syl6ib
 |-  ( x e. NN -> ( ( -. ph /\ A. y e. NN ( -. ps -> x <_ y ) ) -> ( ph /\ -. ph ) ) )
16 3 15 mtoi
 |-  ( x e. NN -> -. ( -. ph /\ A. y e. NN ( -. ps -> x <_ y ) ) )
17 16 nrex
 |-  -. E. x e. NN ( -. ph /\ A. y e. NN ( -. ps -> x <_ y ) )
18 1 notbid
 |-  ( x = y -> ( -. ph <-> -. ps ) )
19 18 nnwos
 |-  ( E. x e. NN -. ph -> E. x e. NN ( -. ph /\ A. y e. NN ( -. ps -> x <_ y ) ) )
20 17 19 mto
 |-  -. E. x e. NN -. ph
21 dfral2
 |-  ( A. x e. NN ph <-> -. E. x e. NN -. ph )
22 20 21 mpbir
 |-  A. x e. NN ph
23 22 rspec
 |-  ( x e. NN -> ph )