Metamath Proof Explorer

Theorem pcexp

Description: Prime power of an exponential. (Contributed by Mario Carneiro, 10-Aug-2015)

Ref Expression
Assertion pcexp 
|- ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ N e. ZZ ) -> ( P pCnt ( A ^ N ) ) = ( N x. ( P pCnt A ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = 0 -> ( A ^ x ) = ( A ^ 0 ) )
2 1 oveq2d 
 |-  ( x = 0 -> ( P pCnt ( A ^ x ) ) = ( P pCnt ( A ^ 0 ) ) )
3 oveq1 
 |-  ( x = 0 -> ( x x. ( P pCnt A ) ) = ( 0 x. ( P pCnt A ) ) )
4 2 3 eqeq12d 
 |-  ( x = 0 -> ( ( P pCnt ( A ^ x ) ) = ( x x. ( P pCnt A ) ) <-> ( P pCnt ( A ^ 0 ) ) = ( 0 x. ( P pCnt A ) ) ) )
5 oveq2 
 |-  ( x = y -> ( A ^ x ) = ( A ^ y ) )
6 5 oveq2d 
 |-  ( x = y -> ( P pCnt ( A ^ x ) ) = ( P pCnt ( A ^ y ) ) )
7 oveq1 
 |-  ( x = y -> ( x x. ( P pCnt A ) ) = ( y x. ( P pCnt A ) ) )
8 6 7 eqeq12d 
 |-  ( x = y -> ( ( P pCnt ( A ^ x ) ) = ( x x. ( P pCnt A ) ) <-> ( P pCnt ( A ^ y ) ) = ( y x. ( P pCnt A ) ) ) )
9 oveq2 
 |-  ( x = ( y + 1 ) -> ( A ^ x ) = ( A ^ ( y + 1 ) ) )
10 9 oveq2d 
 |-  ( x = ( y + 1 ) -> ( P pCnt ( A ^ x ) ) = ( P pCnt ( A ^ ( y + 1 ) ) ) )
11 oveq1 
 |-  ( x = ( y + 1 ) -> ( x x. ( P pCnt A ) ) = ( ( y + 1 ) x. ( P pCnt A ) ) )
12 10 11 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( P pCnt ( A ^ x ) ) = ( x x. ( P pCnt A ) ) <-> ( P pCnt ( A ^ ( y + 1 ) ) ) = ( ( y + 1 ) x. ( P pCnt A ) ) ) )
13 oveq2 
 |-  ( x = -u y -> ( A ^ x ) = ( A ^ -u y ) )
14 13 oveq2d 
 |-  ( x = -u y -> ( P pCnt ( A ^ x ) ) = ( P pCnt ( A ^ -u y ) ) )
15 oveq1 
 |-  ( x = -u y -> ( x x. ( P pCnt A ) ) = ( -u y x. ( P pCnt A ) ) )
16 14 15 eqeq12d 
 |-  ( x = -u y -> ( ( P pCnt ( A ^ x ) ) = ( x x. ( P pCnt A ) ) <-> ( P pCnt ( A ^ -u y ) ) = ( -u y x. ( P pCnt A ) ) ) )
17 oveq2 
 |-  ( x = N -> ( A ^ x ) = ( A ^ N ) )
18 17 oveq2d 
 |-  ( x = N -> ( P pCnt ( A ^ x ) ) = ( P pCnt ( A ^ N ) ) )
19 oveq1 
 |-  ( x = N -> ( x x. ( P pCnt A ) ) = ( N x. ( P pCnt A ) ) )
20 18 19 eqeq12d 
 |-  ( x = N -> ( ( P pCnt ( A ^ x ) ) = ( x x. ( P pCnt A ) ) <-> ( P pCnt ( A ^ N ) ) = ( N x. ( P pCnt A ) ) ) )
21 pc1 
 |-  ( P e. Prime -> ( P pCnt 1 ) = 0 )
22 21 adantr 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( P pCnt 1 ) = 0 )
23 qcn 
 |-  ( A e. QQ -> A e. CC )
24 23 ad2antrl 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> A e. CC )
25 24 exp0d 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( A ^ 0 ) = 1 )
26 25 oveq2d 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( P pCnt ( A ^ 0 ) ) = ( P pCnt 1 ) )
27 pcqcl 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( P pCnt A ) e. ZZ )
28 27 zcnd 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( P pCnt A ) e. CC )
29 28 mul02d 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( 0 x. ( P pCnt A ) ) = 0 )
30 22 26 29 3eqtr4d 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( P pCnt ( A ^ 0 ) ) = ( 0 x. ( P pCnt A ) ) )
31 oveq1 
 |-  ( ( P pCnt ( A ^ y ) ) = ( y x. ( P pCnt A ) ) -> ( ( P pCnt ( A ^ y ) ) + ( P pCnt A ) ) = ( ( y x. ( P pCnt A ) ) + ( P pCnt A ) ) )
32 expp1 
 |-  ( ( A e. CC /\ y e. NN0 ) -> ( A ^ ( y + 1 ) ) = ( ( A ^ y ) x. A ) )
33 24 32 sylan 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN0 ) -> ( A ^ ( y + 1 ) ) = ( ( A ^ y ) x. A ) )
34 33 oveq2d 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN0 ) -> ( P pCnt ( A ^ ( y + 1 ) ) ) = ( P pCnt ( ( A ^ y ) x. A ) ) )
35 simpll 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN0 ) -> P e. Prime )
36 simplrl 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN0 ) -> A e. QQ )
37 simplrr 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN0 ) -> A =/= 0 )
38 nn0z 
 |-  ( y e. NN0 -> y e. ZZ )
39 38 adantl 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN0 ) -> y e. ZZ )
40 qexpclz 
 |-  ( ( A e. QQ /\ A =/= 0 /\ y e. ZZ ) -> ( A ^ y ) e. QQ )
41 36 37 39 40 syl3anc 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN0 ) -> ( A ^ y ) e. QQ )
42 24 adantr 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN0 ) -> A e. CC )
43 42 37 39 expne0d 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN0 ) -> ( A ^ y ) =/= 0 )
44 pcqmul 
 |-  ( ( P e. Prime /\ ( ( A ^ y ) e. QQ /\ ( A ^ y ) =/= 0 ) /\ ( A e. QQ /\ A =/= 0 ) ) -> ( P pCnt ( ( A ^ y ) x. A ) ) = ( ( P pCnt ( A ^ y ) ) + ( P pCnt A ) ) )
45 35 41 43 36 37 44 syl122anc 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN0 ) -> ( P pCnt ( ( A ^ y ) x. A ) ) = ( ( P pCnt ( A ^ y ) ) + ( P pCnt A ) ) )
46 34 45 eqtrd 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN0 ) -> ( P pCnt ( A ^ ( y + 1 ) ) ) = ( ( P pCnt ( A ^ y ) ) + ( P pCnt A ) ) )
47 nn0cn 
 |-  ( y e. NN0 -> y e. CC )
48 47 adantl 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN0 ) -> y e. CC )
49 28 adantr 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN0 ) -> ( P pCnt A ) e. CC )
50 48 49 adddirp1d 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN0 ) -> ( ( y + 1 ) x. ( P pCnt A ) ) = ( ( y x. ( P pCnt A ) ) + ( P pCnt A ) ) )
51 46 50 eqeq12d 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN0 ) -> ( ( P pCnt ( A ^ ( y + 1 ) ) ) = ( ( y + 1 ) x. ( P pCnt A ) ) <-> ( ( P pCnt ( A ^ y ) ) + ( P pCnt A ) ) = ( ( y x. ( P pCnt A ) ) + ( P pCnt A ) ) ) )
52 31 51 imbitrrid 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN0 ) -> ( ( P pCnt ( A ^ y ) ) = ( y x. ( P pCnt A ) ) -> ( P pCnt ( A ^ ( y + 1 ) ) ) = ( ( y + 1 ) x. ( P pCnt A ) ) ) )
53 52 ex 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( y e. NN0 -> ( ( P pCnt ( A ^ y ) ) = ( y x. ( P pCnt A ) ) -> ( P pCnt ( A ^ ( y + 1 ) ) ) = ( ( y + 1 ) x. ( P pCnt A ) ) ) ) )
54 negeq 
 |-  ( ( P pCnt ( A ^ y ) ) = ( y x. ( P pCnt A ) ) -> -u ( P pCnt ( A ^ y ) ) = -u ( y x. ( P pCnt A ) ) )
55 nnnn0 
 |-  ( y e. NN -> y e. NN0 )
56 expneg 
 |-  ( ( A e. CC /\ y e. NN0 ) -> ( A ^ -u y ) = ( 1 / ( A ^ y ) ) )
57 24 55 56 syl2an 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN ) -> ( A ^ -u y ) = ( 1 / ( A ^ y ) ) )
58 57 oveq2d 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN ) -> ( P pCnt ( A ^ -u y ) ) = ( P pCnt ( 1 / ( A ^ y ) ) ) )
59 simpll 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN ) -> P e. Prime )
60 55 41 sylan2 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN ) -> ( A ^ y ) e. QQ )
61 55 43 sylan2 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN ) -> ( A ^ y ) =/= 0 )
62 pcrec 
 |-  ( ( P e. Prime /\ ( ( A ^ y ) e. QQ /\ ( A ^ y ) =/= 0 ) ) -> ( P pCnt ( 1 / ( A ^ y ) ) ) = -u ( P pCnt ( A ^ y ) ) )
63 59 60 61 62 syl12anc 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN ) -> ( P pCnt ( 1 / ( A ^ y ) ) ) = -u ( P pCnt ( A ^ y ) ) )
64 58 63 eqtrd 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN ) -> ( P pCnt ( A ^ -u y ) ) = -u ( P pCnt ( A ^ y ) ) )
65 nncn 
 |-  ( y e. NN -> y e. CC )
66 mulneg1 
 |-  ( ( y e. CC /\ ( P pCnt A ) e. CC ) -> ( -u y x. ( P pCnt A ) ) = -u ( y x. ( P pCnt A ) ) )
67 65 28 66 syl2anr 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN ) -> ( -u y x. ( P pCnt A ) ) = -u ( y x. ( P pCnt A ) ) )
68 64 67 eqeq12d 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN ) -> ( ( P pCnt ( A ^ -u y ) ) = ( -u y x. ( P pCnt A ) ) <-> -u ( P pCnt ( A ^ y ) ) = -u ( y x. ( P pCnt A ) ) ) )
69 54 68 imbitrrid 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) /\ y e. NN ) -> ( ( P pCnt ( A ^ y ) ) = ( y x. ( P pCnt A ) ) -> ( P pCnt ( A ^ -u y ) ) = ( -u y x. ( P pCnt A ) ) ) )
70 69 ex 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( y e. NN -> ( ( P pCnt ( A ^ y ) ) = ( y x. ( P pCnt A ) ) -> ( P pCnt ( A ^ -u y ) ) = ( -u y x. ( P pCnt A ) ) ) ) )
71 4 8 12 16 20 30 53 70 zindd 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( N e. ZZ -> ( P pCnt ( A ^ N ) ) = ( N x. ( P pCnt A ) ) ) )
72 71 3impia 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ N e. ZZ ) -> ( P pCnt ( A ^ N ) ) = ( N x. ( P pCnt A ) ) )