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	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) → ∃ 𝑛 ∈ ℕ0 𝐴 = ( 𝑃 ↑ 𝑛 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝑃 ∈ ℙ )
2		simp2	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℕ )
3	1 2	pccld	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 )
4	3	adantr	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) ) → ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 )
5		oveq2	⊢ ( 𝑛 = ( 𝑃 pCnt 𝐴 ) → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) )
6	5	eqeq2d	⊢ ( 𝑛 = ( 𝑃 pCnt 𝐴 ) → ( 𝐴 = ( 𝑃 ↑ 𝑛 ) ↔ 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
7	6	adantl	⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑛 = ( 𝑃 pCnt 𝐴 ) ) → ( 𝐴 = ( 𝑃 ↑ 𝑛 ) ↔ 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
8		simpl3	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
9		oveq2	⊢ ( 𝑛 = 𝑁 → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ 𝑁 ) )
10	9	breq2d	⊢ ( 𝑛 = 𝑁 → ( 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ↔ 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) ) )
11	10	adantl	⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑛 = 𝑁 ) → ( 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ↔ 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) ) )
12		simpr	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) ) → 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) )
13	8 11 12	rspcedvd	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) ) → ∃ 𝑛 ∈ ℕ0 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) )
14		pcprmpw2	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ↔ 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
15	14	3adant3	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ∃ 𝑛 ∈ ℕ0 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ↔ 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
16	15	adantr	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) ) → ( ∃ 𝑛 ∈ ℕ0 𝐴 ∥ ( 𝑃 ↑ 𝑛 ) ↔ 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ) )
17	13 16	mpbid	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) ) → 𝐴 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) )
18	4 7 17	rspcedvd	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) ) → ∃ 𝑛 ∈ ℕ0 𝐴 = ( 𝑃 ↑ 𝑛 ) )
19	18	ex	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) → ∃ 𝑛 ∈ ℕ0 𝐴 = ( 𝑃 ↑ 𝑛 ) ) )