This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ppi1i

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

Ref Expression
Hypotheses ppi1i.m ⊢ M ∈ ℕ 0
ppi1i.n ⊢ N = M + 1
ppi1i.p ⊢ π _ ⁡ M = K
ppi1i.1 ⊢ N ∈ ℙ
Assertion ppi1i ⊢ π _ ⁡ N = K + 1

Proof

Step Hyp Ref Expression
1 ppi1i.m ⊢ M ∈ ℕ 0
2 ppi1i.n ⊢ N = M + 1
3 ppi1i.p ⊢ π _ ⁡ M = K
4 ppi1i.1 ⊢ N ∈ ℙ
5 2 fveq2i ⊢ π _ ⁡ N = π _ ⁡ M + 1
6 1 nn0zi ⊢ M ∈ ℤ
7 2 4 eqeltrri ⊢ M + 1 ∈ ℙ
8 ppiprm ⊢ M ∈ ℤ ∧ M + 1 ∈ ℙ → π _ ⁡ M + 1 = π _ ⁡ M + 1
9 6 7 8 mp2an ⊢ π _ ⁡ M + 1 = π _ ⁡ M + 1
10 3 oveq1i ⊢ π _ ⁡ M + 1 = K + 1
11 5 9 10 3eqtri ⊢ π _ ⁡ N = K + 1