Metamath Proof Explorer


Theorem pcexp

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

Ref Expression
Assertion pcexp ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ ) ) = ( ๐‘ ยท ( ๐‘ƒ pCnt ๐ด ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 โŠข ( ๐‘ฅ = 0 โ†’ ( ๐ด โ†‘ ๐‘ฅ ) = ( ๐ด โ†‘ 0 ) )
2 1 oveq2d โŠข ( ๐‘ฅ = 0 โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฅ ) ) = ( ๐‘ƒ pCnt ( ๐ด โ†‘ 0 ) ) )
3 oveq1 โŠข ( ๐‘ฅ = 0 โ†’ ( ๐‘ฅ ยท ( ๐‘ƒ pCnt ๐ด ) ) = ( 0 ยท ( ๐‘ƒ pCnt ๐ด ) ) )
4 2 3 eqeq12d โŠข ( ๐‘ฅ = 0 โ†’ ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฅ ) ) = ( ๐‘ฅ ยท ( ๐‘ƒ pCnt ๐ด ) ) โ†” ( ๐‘ƒ pCnt ( ๐ด โ†‘ 0 ) ) = ( 0 ยท ( ๐‘ƒ pCnt ๐ด ) ) ) )
5 oveq2 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ๐ด โ†‘ ๐‘ฅ ) = ( ๐ด โ†‘ ๐‘ฆ ) )
6 5 oveq2d โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฅ ) ) = ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) )
7 oveq1 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ๐‘ฅ ยท ( ๐‘ƒ pCnt ๐ด ) ) = ( ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) )
8 6 7 eqeq12d โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฅ ) ) = ( ๐‘ฅ ยท ( ๐‘ƒ pCnt ๐ด ) ) โ†” ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) = ( ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) ) )
9 oveq2 โŠข ( ๐‘ฅ = ( ๐‘ฆ + 1 ) โ†’ ( ๐ด โ†‘ ๐‘ฅ ) = ( ๐ด โ†‘ ( ๐‘ฆ + 1 ) ) )
10 9 oveq2d โŠข ( ๐‘ฅ = ( ๐‘ฆ + 1 ) โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฅ ) ) = ( ๐‘ƒ pCnt ( ๐ด โ†‘ ( ๐‘ฆ + 1 ) ) ) )
11 oveq1 โŠข ( ๐‘ฅ = ( ๐‘ฆ + 1 ) โ†’ ( ๐‘ฅ ยท ( ๐‘ƒ pCnt ๐ด ) ) = ( ( ๐‘ฆ + 1 ) ยท ( ๐‘ƒ pCnt ๐ด ) ) )
12 10 11 eqeq12d โŠข ( ๐‘ฅ = ( ๐‘ฆ + 1 ) โ†’ ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฅ ) ) = ( ๐‘ฅ ยท ( ๐‘ƒ pCnt ๐ด ) ) โ†” ( ๐‘ƒ pCnt ( ๐ด โ†‘ ( ๐‘ฆ + 1 ) ) ) = ( ( ๐‘ฆ + 1 ) ยท ( ๐‘ƒ pCnt ๐ด ) ) ) )
13 oveq2 โŠข ( ๐‘ฅ = - ๐‘ฆ โ†’ ( ๐ด โ†‘ ๐‘ฅ ) = ( ๐ด โ†‘ - ๐‘ฆ ) )
14 13 oveq2d โŠข ( ๐‘ฅ = - ๐‘ฆ โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฅ ) ) = ( ๐‘ƒ pCnt ( ๐ด โ†‘ - ๐‘ฆ ) ) )
15 oveq1 โŠข ( ๐‘ฅ = - ๐‘ฆ โ†’ ( ๐‘ฅ ยท ( ๐‘ƒ pCnt ๐ด ) ) = ( - ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) )
16 14 15 eqeq12d โŠข ( ๐‘ฅ = - ๐‘ฆ โ†’ ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฅ ) ) = ( ๐‘ฅ ยท ( ๐‘ƒ pCnt ๐ด ) ) โ†” ( ๐‘ƒ pCnt ( ๐ด โ†‘ - ๐‘ฆ ) ) = ( - ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) ) )
17 oveq2 โŠข ( ๐‘ฅ = ๐‘ โ†’ ( ๐ด โ†‘ ๐‘ฅ ) = ( ๐ด โ†‘ ๐‘ ) )
18 17 oveq2d โŠข ( ๐‘ฅ = ๐‘ โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฅ ) ) = ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ ) ) )
19 oveq1 โŠข ( ๐‘ฅ = ๐‘ โ†’ ( ๐‘ฅ ยท ( ๐‘ƒ pCnt ๐ด ) ) = ( ๐‘ ยท ( ๐‘ƒ pCnt ๐ด ) ) )
20 18 19 eqeq12d โŠข ( ๐‘ฅ = ๐‘ โ†’ ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฅ ) ) = ( ๐‘ฅ ยท ( ๐‘ƒ pCnt ๐ด ) ) โ†” ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ ) ) = ( ๐‘ ยท ( ๐‘ƒ pCnt ๐ด ) ) ) )
21 pc1 โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ( ๐‘ƒ pCnt 1 ) = 0 )
22 21 adantr โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โ†’ ( ๐‘ƒ pCnt 1 ) = 0 )
23 qcn โŠข ( ๐ด โˆˆ โ„š โ†’ ๐ด โˆˆ โ„‚ )
24 23 ad2antrl โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โ†’ ๐ด โˆˆ โ„‚ )
25 24 exp0d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โ†’ ( ๐ด โ†‘ 0 ) = 1 )
26 25 oveq2d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ 0 ) ) = ( ๐‘ƒ pCnt 1 ) )
27 pcqcl โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โ†’ ( ๐‘ƒ pCnt ๐ด ) โˆˆ โ„ค )
28 27 zcnd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โ†’ ( ๐‘ƒ pCnt ๐ด ) โˆˆ โ„‚ )
29 28 mul02d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โ†’ ( 0 ยท ( ๐‘ƒ pCnt ๐ด ) ) = 0 )
30 22 26 29 3eqtr4d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ 0 ) ) = ( 0 ยท ( ๐‘ƒ pCnt ๐ด ) ) )
31 oveq1 โŠข ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) = ( ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) โ†’ ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) + ( ๐‘ƒ pCnt ๐ด ) ) = ( ( ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) + ( ๐‘ƒ pCnt ๐ด ) ) )
32 expp1 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ( ๐ด โ†‘ ( ๐‘ฆ + 1 ) ) = ( ( ๐ด โ†‘ ๐‘ฆ ) ยท ๐ด ) )
33 24 32 sylan โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ( ๐ด โ†‘ ( ๐‘ฆ + 1 ) ) = ( ( ๐ด โ†‘ ๐‘ฆ ) ยท ๐ด ) )
34 33 oveq2d โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ ( ๐‘ฆ + 1 ) ) ) = ( ๐‘ƒ pCnt ( ( ๐ด โ†‘ ๐‘ฆ ) ยท ๐ด ) ) )
35 simpll โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ๐‘ƒ โˆˆ โ„™ )
36 simplrl โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ๐ด โˆˆ โ„š )
37 simplrr โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ๐ด โ‰  0 )
38 nn0z โŠข ( ๐‘ฆ โˆˆ โ„•0 โ†’ ๐‘ฆ โˆˆ โ„ค )
39 38 adantl โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ๐‘ฆ โˆˆ โ„ค )
40 qexpclz โŠข ( ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 โˆง ๐‘ฆ โˆˆ โ„ค ) โ†’ ( ๐ด โ†‘ ๐‘ฆ ) โˆˆ โ„š )
41 36 37 39 40 syl3anc โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ( ๐ด โ†‘ ๐‘ฆ ) โˆˆ โ„š )
42 24 adantr โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ๐ด โˆˆ โ„‚ )
43 42 37 39 expne0d โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ( ๐ด โ†‘ ๐‘ฆ ) โ‰  0 )
44 pcqmul โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ( ๐ด โ†‘ ๐‘ฆ ) โˆˆ โ„š โˆง ( ๐ด โ†‘ ๐‘ฆ ) โ‰  0 ) โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โ†’ ( ๐‘ƒ pCnt ( ( ๐ด โ†‘ ๐‘ฆ ) ยท ๐ด ) ) = ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) + ( ๐‘ƒ pCnt ๐ด ) ) )
45 35 41 43 36 37 44 syl122anc โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ( ๐‘ƒ pCnt ( ( ๐ด โ†‘ ๐‘ฆ ) ยท ๐ด ) ) = ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) + ( ๐‘ƒ pCnt ๐ด ) ) )
46 34 45 eqtrd โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ ( ๐‘ฆ + 1 ) ) ) = ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) + ( ๐‘ƒ pCnt ๐ด ) ) )
47 nn0cn โŠข ( ๐‘ฆ โˆˆ โ„•0 โ†’ ๐‘ฆ โˆˆ โ„‚ )
48 47 adantl โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ๐‘ฆ โˆˆ โ„‚ )
49 28 adantr โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ( ๐‘ƒ pCnt ๐ด ) โˆˆ โ„‚ )
50 48 49 adddirp1d โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ( ( ๐‘ฆ + 1 ) ยท ( ๐‘ƒ pCnt ๐ด ) ) = ( ( ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) + ( ๐‘ƒ pCnt ๐ด ) ) )
51 46 50 eqeq12d โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ ( ๐‘ฆ + 1 ) ) ) = ( ( ๐‘ฆ + 1 ) ยท ( ๐‘ƒ pCnt ๐ด ) ) โ†” ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) + ( ๐‘ƒ pCnt ๐ด ) ) = ( ( ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) + ( ๐‘ƒ pCnt ๐ด ) ) ) )
52 31 51 syl5ibr โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) = ( ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ ( ๐‘ฆ + 1 ) ) ) = ( ( ๐‘ฆ + 1 ) ยท ( ๐‘ƒ pCnt ๐ด ) ) ) )
53 52 ex โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โ†’ ( ๐‘ฆ โˆˆ โ„•0 โ†’ ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) = ( ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ ( ๐‘ฆ + 1 ) ) ) = ( ( ๐‘ฆ + 1 ) ยท ( ๐‘ƒ pCnt ๐ด ) ) ) ) )
54 negeq โŠข ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) = ( ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) โ†’ - ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) = - ( ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) )
55 nnnn0 โŠข ( ๐‘ฆ โˆˆ โ„• โ†’ ๐‘ฆ โˆˆ โ„•0 )
56 expneg โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ( ๐ด โ†‘ - ๐‘ฆ ) = ( 1 / ( ๐ด โ†‘ ๐‘ฆ ) ) )
57 24 55 56 syl2an โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„• ) โ†’ ( ๐ด โ†‘ - ๐‘ฆ ) = ( 1 / ( ๐ด โ†‘ ๐‘ฆ ) ) )
58 57 oveq2d โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„• ) โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ - ๐‘ฆ ) ) = ( ๐‘ƒ pCnt ( 1 / ( ๐ด โ†‘ ๐‘ฆ ) ) ) )
59 simpll โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„• ) โ†’ ๐‘ƒ โˆˆ โ„™ )
60 55 41 sylan2 โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„• ) โ†’ ( ๐ด โ†‘ ๐‘ฆ ) โˆˆ โ„š )
61 55 43 sylan2 โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„• ) โ†’ ( ๐ด โ†‘ ๐‘ฆ ) โ‰  0 )
62 pcrec โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ( ๐ด โ†‘ ๐‘ฆ ) โˆˆ โ„š โˆง ( ๐ด โ†‘ ๐‘ฆ ) โ‰  0 ) ) โ†’ ( ๐‘ƒ pCnt ( 1 / ( ๐ด โ†‘ ๐‘ฆ ) ) ) = - ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) )
63 59 60 61 62 syl12anc โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„• ) โ†’ ( ๐‘ƒ pCnt ( 1 / ( ๐ด โ†‘ ๐‘ฆ ) ) ) = - ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) )
64 58 63 eqtrd โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„• ) โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ - ๐‘ฆ ) ) = - ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) )
65 nncn โŠข ( ๐‘ฆ โˆˆ โ„• โ†’ ๐‘ฆ โˆˆ โ„‚ )
66 mulneg1 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ( ๐‘ƒ pCnt ๐ด ) โˆˆ โ„‚ ) โ†’ ( - ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) = - ( ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) )
67 65 28 66 syl2anr โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„• ) โ†’ ( - ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) = - ( ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) )
68 64 67 eqeq12d โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„• ) โ†’ ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ - ๐‘ฆ ) ) = ( - ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) โ†” - ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) = - ( ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) ) )
69 54 68 syl5ibr โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โˆง ๐‘ฆ โˆˆ โ„• ) โ†’ ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) = ( ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ - ๐‘ฆ ) ) = ( - ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) ) )
70 69 ex โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โ†’ ( ๐‘ฆ โˆˆ โ„• โ†’ ( ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ฆ ) ) = ( ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ - ๐‘ฆ ) ) = ( - ๐‘ฆ ยท ( ๐‘ƒ pCnt ๐ด ) ) ) ) )
71 4 8 12 16 20 30 53 70 zindd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โ†’ ( ๐‘ โˆˆ โ„ค โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ ) ) = ( ๐‘ ยท ( ๐‘ƒ pCnt ๐ด ) ) ) )
72 71 3impia โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘ƒ pCnt ( ๐ด โ†‘ ๐‘ ) ) = ( ๐‘ ยท ( ๐‘ƒ pCnt ๐ด ) ) )