Theorem pcprmpw

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

	Ref	Expression
Assertion	pcprmpw	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 𝐴 = ( 𝑃 ↑ 𝑛 ) ↔ 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
2	1	adantr	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → 𝑃 ∈ ℤ )
3		zexpcl	⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑛 ) ∈ ℤ )
4	2 3	sylan	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑛 ) ∈ ℤ )
5		iddvds	⊢ ( ( 𝑃 ↑ 𝑛 ) ∈ ℤ → ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑃 ↑ 𝑛 ) )
6	4 5	syl	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑃 ↑ 𝑛 ) )
7		breq1	⊢ ( 𝐴 = ( 𝑃 ↑ 𝑛 ) → ( 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ↔ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑃 ↑ 𝑛 ) ) )
8	6 7	syl5ibrcom	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 = ( 𝑃 ↑ 𝑛 ) → 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) )
9	8	reximdva	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 𝐴 = ( 𝑃 ↑ 𝑛 ) → ∃ 𝑛 ∈ ℕ0 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ) )
10		pcprmpw2	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ↔ 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
11	9 10	sylibd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 𝐴 = ( 𝑃 ↑ 𝑛 ) → 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
12		pccl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 )
13		oveq2	⊢ ( 𝑛 = ( 𝑃 pCnt 𝐴 ) → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) )
14	13	rspceeqv	⊢ ( ( ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 ∧ 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) → ∃ 𝑛 ∈ ℕ0 𝐴 = ( 𝑃 ↑ 𝑛 ) )
15	14	ex	⊢ ( ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 → ( 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) → ∃ 𝑛 ∈ ℕ0 𝐴 = ( 𝑃 ↑ 𝑛 ) ) )
16	12 15	syl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) → ∃ 𝑛 ∈ ℕ0 𝐴 = ( 𝑃 ↑ 𝑛 ) ) )
17	11 16	impbid	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 𝐴 = ( 𝑃 ↑ 𝑛 ) ↔ 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )