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

Metamath Proof Explorer

Theorem ppi2i

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

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

Proof

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