pczdvds

Description: Defining property of the prime count function. (Contributed by Mario Carneiro, 9-Sep-2014)

		Ref	Expression
	Assertion	pczdvds	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to P^{P pCnt N} ∥ N$

Step	Hyp	Ref	Expression
1		eqid	$⊢ sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <)$
2	1	pczpre	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to P pCnt N = sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <)$
3	2	oveq2d	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to P^{P pCnt N} = P^{sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <)}$
4		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
5		eqid	$⊢ \{n \in ℕ_{0} \| P^{n} ∥ N\} = \{n \in ℕ_{0} \| P^{n} ∥ N\}$
6	5 1	pcprecl	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to (sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <) \in ℕ_{0} \land P^{sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <)} ∥ N)$
7	6	simprd	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to P^{sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <)} ∥ N$
8	4 7	sylan	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to P^{sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <)} ∥ N$
9	3 8	eqbrtrd	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to P^{P pCnt N} ∥ N$

Metamath Proof Explorer