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 ) |
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 ) |