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 )