This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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