Metamath Proof Explorer

Theorem pcprmpw2

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

Ref Expression
Assertion pcprmpw2 
|- ( ( P e. Prime /\ A e. NN ) -> ( E. n e. NN0 A || ( P ^ n ) <-> A = ( P ^ ( P pCnt A ) ) ) )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> A e. NN )
2 1 nnnn0d 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> A e. NN0 )
3 prmnn 
 |-  ( P e. Prime -> P e. NN )
4 3 ad2antrr 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> P e. NN )
5 pccl 
 |-  ( ( P e. Prime /\ A e. NN ) -> ( P pCnt A ) e. NN0 )
6 5 adantr 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> ( P pCnt A ) e. NN0 )
7 4 6 nnexpcld 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> ( P ^ ( P pCnt A ) ) e. NN )
8 7 nnnn0d 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> ( P ^ ( P pCnt A ) ) e. NN0 )
9 6 nn0red 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> ( P pCnt A ) e. RR )
10 9 leidd 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> ( P pCnt A ) <_ ( P pCnt A ) )
11 simpll 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> P e. Prime )
12 6 nn0zd 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> ( P pCnt A ) e. ZZ )
13 pcid 
 |-  ( ( P e. Prime /\ ( P pCnt A ) e. ZZ ) -> ( P pCnt ( P ^ ( P pCnt A ) ) ) = ( P pCnt A ) )
14 11 12 13 syl2anc 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> ( P pCnt ( P ^ ( P pCnt A ) ) ) = ( P pCnt A ) )
15 10 14 breqtrrd 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> ( P pCnt A ) <_ ( P pCnt ( P ^ ( P pCnt A ) ) ) )
16 15 ad2antrr 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) /\ p = P ) -> ( P pCnt A ) <_ ( P pCnt ( P ^ ( P pCnt A ) ) ) )
17 simpr 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) /\ p = P ) -> p = P )
18 17 oveq1d 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) /\ p = P ) -> ( p pCnt A ) = ( P pCnt A ) )
19 17 oveq1d 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) /\ p = P ) -> ( p pCnt ( P ^ ( P pCnt A ) ) ) = ( P pCnt ( P ^ ( P pCnt A ) ) ) )
20 16 18 19 3brtr4d 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) /\ p = P ) -> ( p pCnt A ) <_ ( p pCnt ( P ^ ( P pCnt A ) ) ) )
21 simplrr 
 |-  ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) -> A || ( P ^ n ) )
22 prmz 
 |-  ( p e. Prime -> p e. ZZ )
23 22 adantl 
 |-  ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) -> p e. ZZ )
24 1 adantr 
 |-  ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) -> A e. NN )
25 24 nnzd 
 |-  ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) -> A e. ZZ )
26 simprl 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> n e. NN0 )
27 4 26 nnexpcld 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> ( P ^ n ) e. NN )
28 27 adantr 
 |-  ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) -> ( P ^ n ) e. NN )
29 28 nnzd 
 |-  ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) -> ( P ^ n ) e. ZZ )
30 dvdstr 
 |-  ( ( p e. ZZ /\ A e. ZZ /\ ( P ^ n ) e. ZZ ) -> ( ( p || A /\ A || ( P ^ n ) ) -> p || ( P ^ n ) ) )
31 23 25 29 30 syl3anc 
 |-  ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) -> ( ( p || A /\ A || ( P ^ n ) ) -> p || ( P ^ n ) ) )
32 21 31 mpan2d 
 |-  ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) -> ( p || A -> p || ( P ^ n ) ) )
33 simpr 
 |-  ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) -> p e. Prime )
34 11 adantr 
 |-  ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) -> P e. Prime )
35 simplrl 
 |-  ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) -> n e. NN0 )
36 prmdvdsexpr 
 |-  ( ( p e. Prime /\ P e. Prime /\ n e. NN0 ) -> ( p || ( P ^ n ) -> p = P ) )
37 33 34 35 36 syl3anc 
 |-  ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) -> ( p || ( P ^ n ) -> p = P ) )
38 32 37 syld 
 |-  ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) -> ( p || A -> p = P ) )
39 38 necon3ad 
 |-  ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) -> ( p =/= P -> -. p || A ) )
40 39 imp 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) /\ p =/= P ) -> -. p || A )
41 simplr 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) /\ p =/= P ) -> p e. Prime )
42 1 ad2antrr 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) /\ p =/= P ) -> A e. NN )
43 pceq0 
 |-  ( ( p e. Prime /\ A e. NN ) -> ( ( p pCnt A ) = 0 <-> -. p || A ) )
44 41 42 43 syl2anc 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) /\ p =/= P ) -> ( ( p pCnt A ) = 0 <-> -. p || A ) )
45 40 44 mpbird 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) /\ p =/= P ) -> ( p pCnt A ) = 0 )
46 7 ad2antrr 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) /\ p =/= P ) -> ( P ^ ( P pCnt A ) ) e. NN )
47 41 46 pccld 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) /\ p =/= P ) -> ( p pCnt ( P ^ ( P pCnt A ) ) ) e. NN0 )
48 47 nn0ge0d 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) /\ p =/= P ) -> 0 <_ ( p pCnt ( P ^ ( P pCnt A ) ) ) )
49 45 48 eqbrtrd 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) /\ p =/= P ) -> ( p pCnt A ) <_ ( p pCnt ( P ^ ( P pCnt A ) ) ) )
50 20 49 pm2.61dane 
 |-  ( ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) /\ p e. Prime ) -> ( p pCnt A ) <_ ( p pCnt ( P ^ ( P pCnt A ) ) ) )
51 50 ralrimiva 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> A. p e. Prime ( p pCnt A ) <_ ( p pCnt ( P ^ ( P pCnt A ) ) ) )
52 1 nnzd 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> A e. ZZ )
53 7 nnzd 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> ( P ^ ( P pCnt A ) ) e. ZZ )
54 pc2dvds 
 |-  ( ( A e. ZZ /\ ( P ^ ( P pCnt A ) ) e. ZZ ) -> ( A || ( P ^ ( P pCnt A ) ) <-> A. p e. Prime ( p pCnt A ) <_ ( p pCnt ( P ^ ( P pCnt A ) ) ) ) )
55 52 53 54 syl2anc 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> ( A || ( P ^ ( P pCnt A ) ) <-> A. p e. Prime ( p pCnt A ) <_ ( p pCnt ( P ^ ( P pCnt A ) ) ) ) )
56 51 55 mpbird 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> A || ( P ^ ( P pCnt A ) ) )
57 pcdvds 
 |-  ( ( P e. Prime /\ A e. NN ) -> ( P ^ ( P pCnt A ) ) || A )
58 57 adantr 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> ( P ^ ( P pCnt A ) ) || A )
59 dvdseq 
 |-  ( ( ( A e. NN0 /\ ( P ^ ( P pCnt A ) ) e. NN0 ) /\ ( A || ( P ^ ( P pCnt A ) ) /\ ( P ^ ( P pCnt A ) ) || A ) ) -> A = ( P ^ ( P pCnt A ) ) )
60 2 8 56 58 59 syl22anc 
 |-  ( ( ( P e. Prime /\ A e. NN ) /\ ( n e. NN0 /\ A || ( P ^ n ) ) ) -> A = ( P ^ ( P pCnt A ) ) )
61 60 rexlimdvaa 
 |-  ( ( P e. Prime /\ A e. NN ) -> ( E. n e. NN0 A || ( P ^ n ) -> A = ( P ^ ( P pCnt A ) ) ) )
62 3 adantr 
 |-  ( ( P e. Prime /\ A e. NN ) -> P e. NN )
63 62 5 nnexpcld 
 |-  ( ( P e. Prime /\ A e. NN ) -> ( P ^ ( P pCnt A ) ) e. NN )
64 63 nnzd 
 |-  ( ( P e. Prime /\ A e. NN ) -> ( P ^ ( P pCnt A ) ) e. ZZ )
65 iddvds 
 |-  ( ( P ^ ( P pCnt A ) ) e. ZZ -> ( P ^ ( P pCnt A ) ) || ( P ^ ( P pCnt A ) ) )
66 64 65 syl 
 |-  ( ( P e. Prime /\ A e. NN ) -> ( P ^ ( P pCnt A ) ) || ( P ^ ( P pCnt A ) ) )
67 oveq2 
 |-  ( n = ( P pCnt A ) -> ( P ^ n ) = ( P ^ ( P pCnt A ) ) )
68 67 breq2d 
 |-  ( n = ( P pCnt A ) -> ( ( P ^ ( P pCnt A ) ) || ( P ^ n ) <-> ( P ^ ( P pCnt A ) ) || ( P ^ ( P pCnt A ) ) ) )
69 68 rspcev 
 |-  ( ( ( P pCnt A ) e. NN0 /\ ( P ^ ( P pCnt A ) ) || ( P ^ ( P pCnt A ) ) ) -> E. n e. NN0 ( P ^ ( P pCnt A ) ) || ( P ^ n ) )
70 5 66 69 syl2anc 
 |-  ( ( P e. Prime /\ A e. NN ) -> E. n e. NN0 ( P ^ ( P pCnt A ) ) || ( P ^ n ) )
71 breq1 
 |-  ( A = ( P ^ ( P pCnt A ) ) -> ( A || ( P ^ n ) <-> ( P ^ ( P pCnt A ) ) || ( P ^ n ) ) )
72 71 rexbidv 
 |-  ( A = ( P ^ ( P pCnt A ) ) -> ( E. n e. NN0 A || ( P ^ n ) <-> E. n e. NN0 ( P ^ ( P pCnt A ) ) || ( P ^ n ) ) )
73 70 72 syl5ibrcom 
 |-  ( ( P e. Prime /\ A e. NN ) -> ( A = ( P ^ ( P pCnt A ) ) -> E. n e. NN0 A || ( P ^ n ) ) )
74 61 73 impbid 
 |-  ( ( P e. Prime /\ A e. NN ) -> ( E. n e. NN0 A || ( P ^ n ) <-> A = ( P ^ ( P pCnt A ) ) ) )