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

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 -> ( ph <-> ch ) )
indstr2.2 
|- ( x = y -> ( ph <-> ps ) )
indstr2.3 
|- ch
indstr2.4 
|- ( x e. ( ZZ>= ` 2 ) -> ( A. y e. NN ( y < x -> ps ) -> ph ) )
Assertion indstr2 
|- ( x e. NN -> ph )

Proof

Step Hyp Ref Expression
1 indstr2.1 
 |-  ( x = 1 -> ( ph <-> ch ) )
2 indstr2.2 
 |-  ( x = y -> ( ph <-> ps ) )
3 indstr2.3 
 |-  ch
4 indstr2.4 
 |-  ( x e. ( ZZ>= ` 2 ) -> ( A. y e. NN ( y < x -> ps ) -> ph ) )
5 elnn1uz2 
 |-  ( x e. NN <-> ( x = 1 \/ x e. ( ZZ>= ` 2 ) ) )
6 nnnlt1 
 |-  ( y e. NN -> -. y < 1 )
7 6 adantl 
 |-  ( ( x = 1 /\ y e. NN ) -> -. y < 1 )
8 breq2 
 |-  ( x = 1 -> ( y < x <-> y < 1 ) )
9 8 adantr 
 |-  ( ( x = 1 /\ y e. NN ) -> ( y < x <-> y < 1 ) )
10 7 9 mtbird 
 |-  ( ( x = 1 /\ y e. NN ) -> -. y < x )
11 10 pm2.21d 
 |-  ( ( x = 1 /\ y e. NN ) -> ( y < x -> ps ) )
12 11 ralrimiva 
 |-  ( x = 1 -> A. y e. NN ( y < x -> ps ) )
13 pm5.5 
 |-  ( A. y e. NN ( y < x -> ps ) -> ( ( A. y e. NN ( y < x -> ps ) -> ph ) <-> ph ) )
14 12 13 syl 
 |-  ( x = 1 -> ( ( A. y e. NN ( y < x -> ps ) -> ph ) <-> ph ) )
15 14 1 bitrd 
 |-  ( x = 1 -> ( ( A. y e. NN ( y < x -> ps ) -> ph ) <-> ch ) )
16 3 15 mpbiri 
 |-  ( x = 1 -> ( A. y e. NN ( y < x -> ps ) -> ph ) )
17 16 4 jaoi 
 |-  ( ( x = 1 \/ x e. ( ZZ>= ` 2 ) ) -> ( A. y e. NN ( y < x -> ps ) -> ph ) )
18 5 17 sylbi 
 |-  ( x e. NN -> ( A. y e. NN ( y < x -> ps ) -> ph ) )
19 2 18 indstr 
 |-  ( x e. NN -> ph )