Theorem ppi1i

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

	Ref	Expression
Hypotheses	ppi1i.m	$$⊢M\in {\mathbb{N}}_0$$
	ppi1i.n	$$⊢N=M+1$$
	ppi1i.p	$$⊢\underset{\_}{\pi }\left(M\right)=K$$
	ppi1i.1	$$⊢N\in \mathbb{P}$$
Assertion	ppi1i	$$⊢\underset{\_}{\pi }\left(N\right)=K+1$$

Proof

Step	Hyp	Ref	Expression
1		ppi1i.m	$$⊢M\in {\mathbb{N}}_0$$
2		ppi1i.n	$$⊢N=M+1$$
3		ppi1i.p	$$⊢\underset{\_}{\pi }\left(M\right)=K$$
4		ppi1i.1	$$⊢N\in \mathbb{P}$$
5	2	fveq2i	$$⊢\underset{\_}{\pi }\left(N\right)=\underset{\_}{\pi }\left(M+1\right)$$
6	1	nn0zi	$$⊢M\in \mathbb{Z}$$
7	2 4	eqeltrri	$$⊢M+1\in \mathbb{P}$$
8		ppiprm	$$⊢\left(M\in \mathbb{Z}\wedge M+1\in \mathbb{P}\right)\to \underset{\_}{\pi }\left(M+1\right)=\underset{\_}{\pi }\left(M\right)+1$$
9	6 7 8	mp2an	$$⊢\underset{\_}{\pi }\left(M+1\right)=\underset{\_}{\pi }\left(M\right)+1$$
10	3	oveq1i	$$⊢\underset{\_}{\pi }\left(M\right)+1=K+1$$
11	5 9 10	3eqtri	$$⊢\underset{\_}{\pi }\left(N\right)=K+1$$