This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrdi 
 |-  ( 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 )