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 ⊢ P ∈ ℙ ∧ A ∈ ℕ ∧ N ∈ ℕ 0 → A ∥ P N → ∃ n ∈ ℕ 0 A = P n

Proof

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