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 )