pczndvds2

Description: The remainder after dividing out all factors of P is not divisible by P . (Contributed by Mario Carneiro, 9-Sep-2014)

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

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

Metamath Proof Explorer