Theorem ppi1i

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

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

Proof

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