Metamath Proof Explorer

Theorem dvdsprmpweq

Description: If a positive integer divides a prime power, it is a prime power. (Contributed by AV, 25-Jul-2021)

		Ref	Expression
	Assertion	dvdsprmpweq	$⊢ (P \in ℙ \land A \in ℕ \land N \in ℕ_{0}) \to (A ∥ P^{N} \to \exists n \in ℕ_{0} A = P^{n})$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (P \in ℙ \land A \in ℕ \land N \in ℕ_{0}) \to P \in ℙ$
2		simp2	$⊢ (P \in ℙ \land A \in ℕ \land N \in ℕ_{0}) \to A \in ℕ$
3	1 2	pccld	$⊢ (P \in ℙ \land A \in ℕ \land N \in ℕ_{0}) \to P pCnt A \in ℕ_{0}$
4	3	adantr	$⊢ ((P \in ℙ \land A \in ℕ \land N \in ℕ_{0}) \land A ∥ P^{N}) \to P pCnt A \in ℕ_{0}$
5		oveq2	$⊢ n = P pCnt A \to P^{n} = P^{P pCnt A}$
6	5	eqeq2d	$⊢ n = P pCnt A \to (A = P^{n} \leftrightarrow A = P^{P pCnt A})$
7	6	adantl	$⊢ (((P \in ℙ \land A \in ℕ \land N \in ℕ_{0}) \land A ∥ P^{N}) \land n = P pCnt A) \to (A = P^{n} \leftrightarrow A = P^{P pCnt A})$
8		simpl3	$⊢ ((P \in ℙ \land A \in ℕ \land N \in ℕ_{0}) \land A ∥ P^{N}) \to N \in ℕ_{0}$
9		oveq2	$⊢ n = N \to P^{n} = P^{N}$
10	9	breq2d	$⊢ n = N \to (A ∥ P^{n} \leftrightarrow A ∥ P^{N})$
11	10	adantl	$⊢ (((P \in ℙ \land A \in ℕ \land N \in ℕ_{0}) \land A ∥ P^{N}) \land n = N) \to (A ∥ P^{n} \leftrightarrow A ∥ P^{N})$
12		simpr	$⊢ ((P \in ℙ \land A \in ℕ \land N \in ℕ_{0}) \land A ∥ P^{N}) \to A ∥ P^{N}$
13	8 11 12	rspcedvd	$⊢ ((P \in ℙ \land A \in ℕ \land N \in ℕ_{0}) \land A ∥ P^{N}) \to \exists n \in ℕ_{0} A ∥ P^{n}$
14		pcprmpw2	$⊢ (P \in ℙ \land A \in ℕ) \to (\exists n \in ℕ_{0} A ∥ P^{n} \leftrightarrow A = P^{P pCnt A})$
15	14	3adant3	$⊢ (P \in ℙ \land A \in ℕ \land N \in ℕ_{0}) \to (\exists n \in ℕ_{0} A ∥ P^{n} \leftrightarrow A = P^{P pCnt A})$
16	15	adantr	$⊢ ((P \in ℙ \land A \in ℕ \land N \in ℕ_{0}) \land A ∥ P^{N}) \to (\exists n \in ℕ_{0} A ∥ P^{n} \leftrightarrow A = P^{P pCnt A})$
17	13 16	mpbid	$⊢ ((P \in ℙ \land A \in ℕ \land N \in ℕ_{0}) \land A ∥ P^{N}) \to A = P^{P pCnt A}$
18	4 7 17	rspcedvd	$⊢ ((P \in ℙ \land A \in ℕ \land N \in ℕ_{0}) \land A ∥ P^{N}) \to \exists n \in ℕ_{0} A = P^{n}$
19	18	ex	$⊢ (P \in ℙ \land A \in ℕ \land N \in ℕ_{0}) \to (A ∥ P^{N} \to \exists n \in ℕ_{0} A = P^{n})$