Theorem ppi1i

Description: Inference form of ppiprm . (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
	ppi1i.1	|- N e. Prime
Assertion	ppi1i	|- ( ppi ` N ) = ( K + 1 )

Proof

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