Metamath Proof Explorer

Theorem pcprmpw

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

Ref Expression
Assertion pcprmpw ⊢ P ∈ ℙ ∧ A ∈ ℕ → ∃ n ∈ ℕ 0 A = P n ↔ A = P P pCnt A

Proof

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