Theorem ppi2i

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

	Ref	Expression
Hypotheses	ppi1i.m	⊢ 𝑀 ∈ ℕ0
	ppi1i.n	⊢ 𝑁 = ( 𝑀 + 1 )
	ppi1i.p	⊢ ( π ‘ 𝑀 ) = 𝐾
	ppi2i.1	⊢ ¬ 𝑁 ∈ ℙ
Assertion	ppi2i	⊢ ( π ‘ 𝑁 ) = 𝐾

Proof

Step	Hyp	Ref	Expression
1		ppi1i.m	⊢ 𝑀 ∈ ℕ0
2		ppi1i.n	⊢ 𝑁 = ( 𝑀 + 1 )
3		ppi1i.p	⊢ ( π ‘ 𝑀 ) = 𝐾
4		ppi2i.1	⊢ ¬ 𝑁 ∈ ℙ
5	2	fveq2i	⊢ ( π ‘ 𝑁 ) = ( π ‘ ( 𝑀 + 1 ) )
6	1	nn0zi	⊢ 𝑀 ∈ ℤ
7	2	eleq1i	⊢ ( 𝑁 ∈ ℙ ↔ ( 𝑀 + 1 ) ∈ ℙ )
8	4 7	mtbi	⊢ ¬ ( 𝑀 + 1 ) ∈ ℙ
9		ppinprm	⊢ ( ( 𝑀 ∈ ℤ ∧ ¬ ( 𝑀 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝑀 + 1 ) ) = ( π ‘ 𝑀 ) )
10	6 8 9	mp2an	⊢ ( π ‘ ( 𝑀 + 1 ) ) = ( π ‘ 𝑀 )
11	5 10 3	3eqtri	⊢ ( π ‘ 𝑁 ) = 𝐾