Metamath Proof Explorer
Description: Closure of the prime power function. (Contributed by Mario Carneiro, 29May2016)


Ref 
Expression 

Hypotheses 
pccld.1 
⊢ ( 𝜑 → 𝑃 ∈ ℙ ) 


pccld.2 
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) 

Assertion 
pccld 
⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) ∈ ℕ_{0} ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

pccld.1 
⊢ ( 𝜑 → 𝑃 ∈ ℙ ) 
2 

pccld.2 
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) 
3 

pccl 
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ_{0} ) 
4 
1 2 3

syl2anc 
⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) ∈ ℕ_{0} ) 