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 e. Prime /\ A e. NN /\ N e. NN0 ) -> ( A || ( P ^ N ) -> E. n e. NN0 A = ( P ^ n ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> P e. Prime )
2 simp2 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> A e. NN )
3 1 2 pccld 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> ( P pCnt A ) e. NN0 )
4 3 adantr 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) -> ( P pCnt A ) e. NN0 )
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 e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) /\ n = ( P pCnt A ) ) -> ( A = ( P ^ n ) <-> A = ( P ^ ( P pCnt A ) ) ) )
8 simpl3 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) -> N e. NN0 )
9 oveq2 
 |-  ( n = N -> ( P ^ n ) = ( P ^ N ) )
10 9 breq2d 
 |-  ( n = N -> ( A || ( P ^ n ) <-> A || ( P ^ N ) ) )
11 10 adantl 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) /\ n = N ) -> ( A || ( P ^ n ) <-> A || ( P ^ N ) ) )
12 simpr 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) -> A || ( P ^ N ) )
13 8 11 12 rspcedvd 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) -> E. n e. NN0 A || ( P ^ n ) )
14 pcprmpw2 
 |-  ( ( P e. Prime /\ A e. NN ) -> ( E. n e. NN0 A || ( P ^ n ) <-> A = ( P ^ ( P pCnt A ) ) ) )
15 14 3adant3 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> ( E. n e. NN0 A || ( P ^ n ) <-> A = ( P ^ ( P pCnt A ) ) ) )
16 15 adantr 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) -> ( E. n e. NN0 A || ( P ^ n ) <-> A = ( P ^ ( P pCnt A ) ) ) )
17 13 16 mpbid 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) -> A = ( P ^ ( P pCnt A ) ) )
18 4 7 17 rspcedvd 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) -> E. n e. NN0 A = ( P ^ n ) )
19 18 ex 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> ( A || ( P ^ N ) -> E. n e. NN0 A = ( P ^ n ) ) )