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

Metamath Proof Explorer

Theorem 1arithlem3

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

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

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 pccl ⊢ p ∈ ℙ ∧ N ∈ ℕ → p pCnt N ∈ ℕ 0
4 3 ancoms ⊢ N ∈ ℕ ∧ p ∈ ℙ → p pCnt N ∈ ℕ 0
5 2 4 fmpt3d ⊢ N ∈ ℕ → M ⁡ N : ℙ ⟶ ℕ 0