pczndvds

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

		Ref	Expression
	Assertion	pczndvds	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to \neg P^{(P pCnt N) + 1} ∥ 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	oveq1d	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to (P pCnt N) + 1 = sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <) + 1$
4	3	oveq2d	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to P^{(P pCnt N) + 1} = P^{sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <) + 1}$
5		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
6		eqid	$⊢ \{n \in ℕ_{0} \| P^{n} ∥ N\} = \{n \in ℕ_{0} \| P^{n} ∥ N\}$
7	6 1	pcprendvds	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to \neg P^{sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <) + 1} ∥ N$
8	5 7	sylan	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to \neg P^{sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <) + 1} ∥ N$
9	4 8	eqnbrtrd	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to \neg P^{(P pCnt N) + 1} ∥ N$

Metamath Proof Explorer