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 imbitrrid ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 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 imbitrrid ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 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 𝐴 ) ) )