pcprmpw

Description: Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015)

		Ref	Expression
	Assertion	pcprmpw	$⊢ (P \in ℙ \land A \in ℕ) \to (\exists n \in ℕ_{0} A = P^{n} \leftrightarrow A = P^{P pCnt A})$

Step	Hyp	Ref	Expression
1		prmz	$⊢ P \in ℙ \to P \in ℤ$
2	1	adantr	$⊢ (P \in ℙ \land A \in ℕ) \to P \in ℤ$
3		zexpcl	$⊢ (P \in ℤ \land n \in ℕ_{0}) \to P^{n} \in ℤ$
4	2 3	sylan	$⊢ ((P \in ℙ \land A \in ℕ) \land n \in ℕ_{0}) \to P^{n} \in ℤ$
5		iddvds	$⊢ P^{n} \in ℤ \to P^{n} ∥ P^{n}$
6	4 5	syl	$⊢ ((P \in ℙ \land A \in ℕ) \land n \in ℕ_{0}) \to P^{n} ∥ P^{n}$
7		breq1	$⊢ A = P^{n} \to (A ∥ P^{n} \leftrightarrow P^{n} ∥ P^{n})$
8	6 7	syl5ibrcom	$⊢ ((P \in ℙ \land A \in ℕ) \land n \in ℕ_{0}) \to (A = P^{n} \to A ∥ P^{n})$
9	8	reximdva	$⊢ (P \in ℙ \land A \in ℕ) \to (\exists n \in ℕ_{0} A = P^{n} \to \exists n \in ℕ_{0} A ∥ P^{n})$
10		pcprmpw2	$⊢ (P \in ℙ \land A \in ℕ) \to (\exists n \in ℕ_{0} A ∥ P^{n} \leftrightarrow A = P^{P pCnt A})$
11	9 10	sylibd	$⊢ (P \in ℙ \land A \in ℕ) \to (\exists n \in ℕ_{0} A = P^{n} \to A = P^{P pCnt A})$
12		pccl	$⊢ (P \in ℙ \land A \in ℕ) \to P pCnt A \in ℕ_{0}$
13		oveq2	$⊢ n = P pCnt A \to P^{n} = P^{P pCnt A}$
14	13	rspceeqv	$⊢ (P pCnt A \in ℕ_{0} \land A = P^{P pCnt A}) \to \exists n \in ℕ_{0} A = P^{n}$
15	14	ex	$⊢ P pCnt A \in ℕ_{0} \to (A = P^{P pCnt A} \to \exists n \in ℕ_{0} A = P^{n})$
16	12 15	syl	$⊢ (P \in ℙ \land A \in ℕ) \to (A = P^{P pCnt A} \to \exists n \in ℕ_{0} A = P^{n})$
17	11 16	impbid	$⊢ (P \in ℙ \land A \in ℕ) \to (\exists n \in ℕ_{0} A = P^{n} \leftrightarrow A = P^{P pCnt A})$

Metamath Proof Explorer