Metamath Proof Explorer


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 )