Metamath Proof Explorer

Theorem 1arithlem1

Description: Lemma for 1arith . (Contributed by Mario Carneiro, 30-May-2014)

Ref Expression
Hypothesis 1arith.1 ⊢ M = n ∈ ℕ ⟼ p ∈ ℙ ⟼ p pCnt n
Assertion 1arithlem1 ⊢ N ∈ ℕ → M ⁡ N = p ∈ ℙ ⟼ p pCnt N

Proof

Step Hyp Ref Expression
1 1arith.1 ⊢ M = n ∈ ℕ ⟼ p ∈ ℙ ⟼ p pCnt n
2 oveq2 ⊢ n = N → p pCnt n = p pCnt N
3 2 mpteq2dv ⊢ n = N → p ∈ ℙ ⟼ p pCnt n = p ∈ ℙ ⟼ p pCnt N
4 prmex ⊢ ℙ ∈ V
5 4 mptex ⊢ p ∈ ℙ ⟼ p pCnt N ∈ V
6 3 1 5 fvmpt ⊢ N ∈ ℕ → M ⁡ N = p ∈ ℙ ⟼ p pCnt N