Theorem nn1suc

Description: If a statement holds for 1 and also holds for a successor, it holds for all positive integers. The first three hypotheses give us the substitution instances we need; the last two show that it holds for 1 and for a successor. (Contributed by NM, 11-Oct-2004) (Revised by Mario Carneiro, 16-May-2014)

	Ref	Expression
Hypotheses	nn1suc.1	|- ( x = 1 -> ( ph <-> ps ) )
	nn1suc.3	|- ( x = ( y + 1 ) -> ( ph <-> ch ) )
	nn1suc.4	|- ( x = A -> ( ph <-> th ) )
	nn1suc.5	|- ps
	nn1suc.6	|- ( y e. NN -> ch )
Assertion	nn1suc	|- ( A e. NN -> th )

Proof

Step	Hyp	Ref	Expression
1		nn1suc.1	|- ( x = 1 -> ( ph <-> ps ) )
2		nn1suc.3	|- ( x = ( y + 1 ) -> ( ph <-> ch ) )
3		nn1suc.4	|- ( x = A -> ( ph <-> th ) )
4		nn1suc.5	|- ps
5		nn1suc.6	|- ( y e. NN -> ch )
6		1ex	|- 1 e. _V
7	6 1	sbcie	|- ( [. 1 / x ]. ph <-> ps )
8	4 7	mpbir	|- [. 1 / x ]. ph
9		1nn	|- 1 e. NN
10		eleq1	|- ( A = 1 -> ( A e. NN <-> 1 e. NN ) )
11	9 10	mpbiri	|- ( A = 1 -> A e. NN )
12	3	sbcieg	|- ( A e. NN -> ( [. A / x ]. ph <-> th ) )
13	11 12	syl	|- ( A = 1 -> ( [. A / x ]. ph <-> th ) )
14		dfsbcq	|- ( A = 1 -> ( [. A / x ]. ph <-> [. 1 / x ]. ph ) )
15	13 14	bitr3d	|- ( A = 1 -> ( th <-> [. 1 / x ]. ph ) )
16	8 15	mpbiri	|- ( A = 1 -> th )
17	16	a1i	|- ( A e. NN -> ( A = 1 -> th ) )
18		ovex	|- ( y + 1 ) e. _V
19	18 2	sbcie	|- ( [. ( y + 1 ) / x ]. ph <-> ch )
20		oveq1	|- ( y = ( A - 1 ) -> ( y + 1 ) = ( ( A - 1 ) + 1 ) )
21	20	sbceq1d	|- ( y = ( A - 1 ) -> ( [. ( y + 1 ) / x ]. ph <-> [. ( ( A - 1 ) + 1 ) / x ]. ph ) )
22	19 21	bitr3id	|- ( y = ( A - 1 ) -> ( ch <-> [. ( ( A - 1 ) + 1 ) / x ]. ph ) )
23	22 5	vtoclga	|- ( ( A - 1 ) e. NN -> [. ( ( A - 1 ) + 1 ) / x ]. ph )
24		nncn	|- ( A e. NN -> A e. CC )
25		ax-1cn	|- 1 e. CC
26		npcan	|- ( ( A e. CC /\ 1 e. CC ) -> ( ( A - 1 ) + 1 ) = A )
27	24 25 26	sylancl	|- ( A e. NN -> ( ( A - 1 ) + 1 ) = A )
28	27	sbceq1d	|- ( A e. NN -> ( [. ( ( A - 1 ) + 1 ) / x ]. ph <-> [. A / x ]. ph ) )
29	28 12	bitrd	|- ( A e. NN -> ( [. ( ( A - 1 ) + 1 ) / x ]. ph <-> th ) )
30	23 29	syl5ib	|- ( A e. NN -> ( ( A - 1 ) e. NN -> th ) )
31		nn1m1nn	|- ( A e. NN -> ( A = 1 \/ ( A - 1 ) e. NN ) )
32	17 30 31	mpjaod	|- ( A e. NN -> th )