Metamath Proof Explorer

Theorem 1arithlem2

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

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

Proof

Step Hyp Ref Expression
1 1arith.1 ⊢ M = n ∈ ℕ ⟼ p ∈ ℙ ⟼ p pCnt n
2 1 1arithlem1 ⊢ N ∈ ℕ → M ⁡ N = p ∈ ℙ ⟼ p pCnt N
3 2 fveq1d ⊢ N ∈ ℕ → M ⁡ N ⁡ P = p ∈ ℙ ⟼ p pCnt N ⁡ P
4 oveq1 ⊢ p = P → p pCnt N = P pCnt N
5 eqid ⊢ p ∈ ℙ ⟼ p pCnt N = p ∈ ℙ ⟼ p pCnt N
6 ovex ⊢ P pCnt N ∈ V
7 4 5 6 fvmpt ⊢ P ∈ ℙ → p ∈ ℙ ⟼ p pCnt N ⁡ P = P pCnt N
8 3 7 sylan9eq ⊢ N ∈ ℕ ∧ P ∈ ℙ → M ⁡ N ⁡ P = P pCnt N