Theorem ppi2i

Description: Inference form of ppinprm . (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$$
	ppi2i.1	$$⊢\neg N\in \mathbb{P}$$
Assertion	ppi2i	$$⊢\underset{\_}{\pi }\left(N\right)=K$$

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		ppi2i.1	$$⊢\neg 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	eleq1i	$$⊢N\in \mathbb{P}\leftrightarrow M+1\in \mathbb{P}$$
8	4 7	mtbi	$$⊢\neg M+1\in \mathbb{P}$$
9		ppinprm	$$⊢\left(M\in \mathbb{Z}\wedge \neg M+1\in \mathbb{P}\right)\to \underset{\_}{\pi }\left(M+1\right)=\underset{\_}{\pi }\left(M\right)$$
10	6 8 9	mp2an	$$⊢\underset{\_}{\pi }\left(M+1\right)=\underset{\_}{\pi }\left(M\right)$$
11	5 10 3	3eqtri	$$⊢\underset{\_}{\pi }\left(N\right)=K$$