| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7439 | . . . . 5
⊢ (𝑥 = 0 → (𝐴↑𝑥) = (𝐴↑0)) | 
| 2 | 1 | oveq2d 7447 | . . . 4
⊢ (𝑥 = 0 → (𝑃 pCnt (𝐴↑𝑥)) = (𝑃 pCnt (𝐴↑0))) | 
| 3 |  | oveq1 7438 | . . . 4
⊢ (𝑥 = 0 → (𝑥 · (𝑃 pCnt 𝐴)) = (0 · (𝑃 pCnt 𝐴))) | 
| 4 | 2, 3 | eqeq12d 2753 | . . 3
⊢ (𝑥 = 0 → ((𝑃 pCnt (𝐴↑𝑥)) = (𝑥 · (𝑃 pCnt 𝐴)) ↔ (𝑃 pCnt (𝐴↑0)) = (0 · (𝑃 pCnt 𝐴)))) | 
| 5 |  | oveq2 7439 | . . . . 5
⊢ (𝑥 = 𝑦 → (𝐴↑𝑥) = (𝐴↑𝑦)) | 
| 6 | 5 | oveq2d 7447 | . . . 4
⊢ (𝑥 = 𝑦 → (𝑃 pCnt (𝐴↑𝑥)) = (𝑃 pCnt (𝐴↑𝑦))) | 
| 7 |  | oveq1 7438 | . . . 4
⊢ (𝑥 = 𝑦 → (𝑥 · (𝑃 pCnt 𝐴)) = (𝑦 · (𝑃 pCnt 𝐴))) | 
| 8 | 6, 7 | eqeq12d 2753 | . . 3
⊢ (𝑥 = 𝑦 → ((𝑃 pCnt (𝐴↑𝑥)) = (𝑥 · (𝑃 pCnt 𝐴)) ↔ (𝑃 pCnt (𝐴↑𝑦)) = (𝑦 · (𝑃 pCnt 𝐴)))) | 
| 9 |  | oveq2 7439 | . . . . 5
⊢ (𝑥 = (𝑦 + 1) → (𝐴↑𝑥) = (𝐴↑(𝑦 + 1))) | 
| 10 | 9 | oveq2d 7447 | . . . 4
⊢ (𝑥 = (𝑦 + 1) → (𝑃 pCnt (𝐴↑𝑥)) = (𝑃 pCnt (𝐴↑(𝑦 + 1)))) | 
| 11 |  | oveq1 7438 | . . . 4
⊢ (𝑥 = (𝑦 + 1) → (𝑥 · (𝑃 pCnt 𝐴)) = ((𝑦 + 1) · (𝑃 pCnt 𝐴))) | 
| 12 | 10, 11 | eqeq12d 2753 | . . 3
⊢ (𝑥 = (𝑦 + 1) → ((𝑃 pCnt (𝐴↑𝑥)) = (𝑥 · (𝑃 pCnt 𝐴)) ↔ (𝑃 pCnt (𝐴↑(𝑦 + 1))) = ((𝑦 + 1) · (𝑃 pCnt 𝐴)))) | 
| 13 |  | oveq2 7439 | . . . . 5
⊢ (𝑥 = -𝑦 → (𝐴↑𝑥) = (𝐴↑-𝑦)) | 
| 14 | 13 | oveq2d 7447 | . . . 4
⊢ (𝑥 = -𝑦 → (𝑃 pCnt (𝐴↑𝑥)) = (𝑃 pCnt (𝐴↑-𝑦))) | 
| 15 |  | oveq1 7438 | . . . 4
⊢ (𝑥 = -𝑦 → (𝑥 · (𝑃 pCnt 𝐴)) = (-𝑦 · (𝑃 pCnt 𝐴))) | 
| 16 | 14, 15 | eqeq12d 2753 | . . 3
⊢ (𝑥 = -𝑦 → ((𝑃 pCnt (𝐴↑𝑥)) = (𝑥 · (𝑃 pCnt 𝐴)) ↔ (𝑃 pCnt (𝐴↑-𝑦)) = (-𝑦 · (𝑃 pCnt 𝐴)))) | 
| 17 |  | oveq2 7439 | . . . . 5
⊢ (𝑥 = 𝑁 → (𝐴↑𝑥) = (𝐴↑𝑁)) | 
| 18 | 17 | oveq2d 7447 | . . . 4
⊢ (𝑥 = 𝑁 → (𝑃 pCnt (𝐴↑𝑥)) = (𝑃 pCnt (𝐴↑𝑁))) | 
| 19 |  | oveq1 7438 | . . . 4
⊢ (𝑥 = 𝑁 → (𝑥 · (𝑃 pCnt 𝐴)) = (𝑁 · (𝑃 pCnt 𝐴))) | 
| 20 | 18, 19 | eqeq12d 2753 | . . 3
⊢ (𝑥 = 𝑁 → ((𝑃 pCnt (𝐴↑𝑥)) = (𝑥 · (𝑃 pCnt 𝐴)) ↔ (𝑃 pCnt (𝐴↑𝑁)) = (𝑁 · (𝑃 pCnt 𝐴)))) | 
| 21 |  | pc1 16893 | . . . . 5
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 1) = 0) | 
| 22 | 21 | adantr 480 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt 1) = 0) | 
| 23 |  | qcn 13005 | . . . . . . 7
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℂ) | 
| 24 | 23 | ad2antrl 728 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → 𝐴 ∈
ℂ) | 
| 25 | 24 | exp0d 14180 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝐴↑0) = 1) | 
| 26 | 25 | oveq2d 7447 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt (𝐴↑0)) = (𝑃 pCnt 1)) | 
| 27 |  | pcqcl 16894 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt 𝐴) ∈ ℤ) | 
| 28 | 27 | zcnd 12723 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt 𝐴) ∈ ℂ) | 
| 29 | 28 | mul02d 11459 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (0 ·
(𝑃 pCnt 𝐴)) = 0) | 
| 30 | 22, 26, 29 | 3eqtr4d 2787 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt (𝐴↑0)) = (0 · (𝑃 pCnt 𝐴))) | 
| 31 |  | oveq1 7438 | . . . . 5
⊢ ((𝑃 pCnt (𝐴↑𝑦)) = (𝑦 · (𝑃 pCnt 𝐴)) → ((𝑃 pCnt (𝐴↑𝑦)) + (𝑃 pCnt 𝐴)) = ((𝑦 · (𝑃 pCnt 𝐴)) + (𝑃 pCnt 𝐴))) | 
| 32 |  | expp1 14109 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℕ0)
→ (𝐴↑(𝑦 + 1)) = ((𝐴↑𝑦) · 𝐴)) | 
| 33 | 24, 32 | sylan 580 | . . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ (𝐴↑(𝑦 + 1)) = ((𝐴↑𝑦) · 𝐴)) | 
| 34 | 33 | oveq2d 7447 | . . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ (𝑃 pCnt (𝐴↑(𝑦 + 1))) = (𝑃 pCnt ((𝐴↑𝑦) · 𝐴))) | 
| 35 |  | simpll 767 | . . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ 𝑃 ∈
ℙ) | 
| 36 |  | simplrl 777 | . . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ 𝐴 ∈
ℚ) | 
| 37 |  | simplrr 778 | . . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ 𝐴 ≠
0) | 
| 38 |  | nn0z 12638 | . . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℤ) | 
| 39 | 38 | adantl 481 | . . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ 𝑦 ∈
ℤ) | 
| 40 |  | qexpclz 14122 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ∧ 𝑦 ∈ ℤ) → (𝐴↑𝑦) ∈ ℚ) | 
| 41 | 36, 37, 39, 40 | syl3anc 1373 | . . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ (𝐴↑𝑦) ∈
ℚ) | 
| 42 | 24 | adantr 480 | . . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ 𝐴 ∈
ℂ) | 
| 43 | 42, 37, 39 | expne0d 14192 | . . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ (𝐴↑𝑦) ≠ 0) | 
| 44 |  | pcqmul 16891 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ ((𝐴↑𝑦) ∈ ℚ ∧ (𝐴↑𝑦) ≠ 0) ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt ((𝐴↑𝑦) · 𝐴)) = ((𝑃 pCnt (𝐴↑𝑦)) + (𝑃 pCnt 𝐴))) | 
| 45 | 35, 41, 43, 36, 37, 44 | syl122anc 1381 | . . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ (𝑃 pCnt ((𝐴↑𝑦) · 𝐴)) = ((𝑃 pCnt (𝐴↑𝑦)) + (𝑃 pCnt 𝐴))) | 
| 46 | 34, 45 | eqtrd 2777 | . . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ (𝑃 pCnt (𝐴↑(𝑦 + 1))) = ((𝑃 pCnt (𝐴↑𝑦)) + (𝑃 pCnt 𝐴))) | 
| 47 |  | nn0cn 12536 | . . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℂ) | 
| 48 | 47 | adantl 481 | . . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ 𝑦 ∈
ℂ) | 
| 49 | 28 | adantr 480 | . . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ (𝑃 pCnt 𝐴) ∈
ℂ) | 
| 50 | 48, 49 | adddirp1d 11287 | . . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ ((𝑦 + 1) ·
(𝑃 pCnt 𝐴)) = ((𝑦 · (𝑃 pCnt 𝐴)) + (𝑃 pCnt 𝐴))) | 
| 51 | 46, 50 | eqeq12d 2753 | . . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ ((𝑃 pCnt (𝐴↑(𝑦 + 1))) = ((𝑦 + 1) · (𝑃 pCnt 𝐴)) ↔ ((𝑃 pCnt (𝐴↑𝑦)) + (𝑃 pCnt 𝐴)) = ((𝑦 · (𝑃 pCnt 𝐴)) + (𝑃 pCnt 𝐴)))) | 
| 52 | 31, 51 | imbitrrid 246 | . . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ ((𝑃 pCnt (𝐴↑𝑦)) = (𝑦 · (𝑃 pCnt 𝐴)) → (𝑃 pCnt (𝐴↑(𝑦 + 1))) = ((𝑦 + 1) · (𝑃 pCnt 𝐴)))) | 
| 53 | 52 | ex 412 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑦 ∈ ℕ0
→ ((𝑃 pCnt (𝐴↑𝑦)) = (𝑦 · (𝑃 pCnt 𝐴)) → (𝑃 pCnt (𝐴↑(𝑦 + 1))) = ((𝑦 + 1) · (𝑃 pCnt 𝐴))))) | 
| 54 |  | negeq 11500 | . . . . 5
⊢ ((𝑃 pCnt (𝐴↑𝑦)) = (𝑦 · (𝑃 pCnt 𝐴)) → -(𝑃 pCnt (𝐴↑𝑦)) = -(𝑦 · (𝑃 pCnt 𝐴))) | 
| 55 |  | nnnn0 12533 | . . . . . . . . 9
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) | 
| 56 |  | expneg 14110 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℕ0)
→ (𝐴↑-𝑦) = (1 / (𝐴↑𝑦))) | 
| 57 | 24, 55, 56 | syl2an 596 | . . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → (𝐴↑-𝑦) = (1 / (𝐴↑𝑦))) | 
| 58 | 57 | oveq2d 7447 | . . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (𝐴↑-𝑦)) = (𝑃 pCnt (1 / (𝐴↑𝑦)))) | 
| 59 |  | simpll 767 | . . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℙ) | 
| 60 | 55, 41 | sylan2 593 | . . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → (𝐴↑𝑦) ∈ ℚ) | 
| 61 | 55, 43 | sylan2 593 | . . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → (𝐴↑𝑦) ≠ 0) | 
| 62 |  | pcrec 16896 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ ((𝐴↑𝑦) ∈ ℚ ∧ (𝐴↑𝑦) ≠ 0)) → (𝑃 pCnt (1 / (𝐴↑𝑦))) = -(𝑃 pCnt (𝐴↑𝑦))) | 
| 63 | 59, 60, 61, 62 | syl12anc 837 | . . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (1 / (𝐴↑𝑦))) = -(𝑃 pCnt (𝐴↑𝑦))) | 
| 64 | 58, 63 | eqtrd 2777 | . . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (𝐴↑-𝑦)) = -(𝑃 pCnt (𝐴↑𝑦))) | 
| 65 |  | nncn 12274 | . . . . . . 7
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) | 
| 66 |  | mulneg1 11699 | . . . . . . 7
⊢ ((𝑦 ∈ ℂ ∧ (𝑃 pCnt 𝐴) ∈ ℂ) → (-𝑦 · (𝑃 pCnt 𝐴)) = -(𝑦 · (𝑃 pCnt 𝐴))) | 
| 67 | 65, 28, 66 | syl2anr 597 | . . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → (-𝑦 · (𝑃 pCnt 𝐴)) = -(𝑦 · (𝑃 pCnt 𝐴))) | 
| 68 | 64, 67 | eqeq12d 2753 | . . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → ((𝑃 pCnt (𝐴↑-𝑦)) = (-𝑦 · (𝑃 pCnt 𝐴)) ↔ -(𝑃 pCnt (𝐴↑𝑦)) = -(𝑦 · (𝑃 pCnt 𝐴)))) | 
| 69 | 54, 68 | imbitrrid 246 | . . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → ((𝑃 pCnt (𝐴↑𝑦)) = (𝑦 · (𝑃 pCnt 𝐴)) → (𝑃 pCnt (𝐴↑-𝑦)) = (-𝑦 · (𝑃 pCnt 𝐴)))) | 
| 70 | 69 | ex 412 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑦 ∈ ℕ → ((𝑃 pCnt (𝐴↑𝑦)) = (𝑦 · (𝑃 pCnt 𝐴)) → (𝑃 pCnt (𝐴↑-𝑦)) = (-𝑦 · (𝑃 pCnt 𝐴))))) | 
| 71 | 4, 8, 12, 16, 20, 30, 53, 70 | zindd 12719 | . 2
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑁 ∈ ℤ → (𝑃 pCnt (𝐴↑𝑁)) = (𝑁 · (𝑃 pCnt 𝐴)))) | 
| 72 | 71 | 3impia 1118 | 1
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ 𝑁 ∈ ℤ) → (𝑃 pCnt (𝐴↑𝑁)) = (𝑁 · (𝑃 pCnt 𝐴))) |