Theorem ppi2i

Description: Inference form of ppinprm . (Contributed by Mario Carneiro, 21-Sep-2014)

	Ref	Expression
Hypotheses	ppi1i.m	|- M e. NN0
	ppi1i.n	|- N = ( M + 1 )
	ppi1i.p	|- ( ppi ` M ) = K
	ppi2i.1	|- -. N e. Prime
Assertion	ppi2i	|- ( ppi ` N ) = K

Proof

Step	Hyp	Ref	Expression
1		ppi1i.m	|- M e. NN0
2		ppi1i.n	|- N = ( M + 1 )
3		ppi1i.p	|- ( ppi ` M ) = K
4		ppi2i.1	|- -. N e. Prime
5	2	fveq2i	|- ( ppi ` N ) = ( ppi ` ( M + 1 ) )
6	1	nn0zi	|- M e. ZZ
7	2	eleq1i	|- ( N e. Prime <-> ( M + 1 ) e. Prime )
8	4 7	mtbi	|- -. ( M + 1 ) e. Prime
9		ppinprm	|- ( ( M e. ZZ /\ -. ( M + 1 ) e. Prime ) -> ( ppi ` ( M + 1 ) ) = ( ppi ` M ) )
10	6 8 9	mp2an	|- ( ppi ` ( M + 1 ) ) = ( ppi ` M )
11	5 10 3	3eqtri	|- ( ppi ` N ) = K