Step | Hyp | Ref
| Expression |
1 | | oveq2 6918 |
. . . . 5
⊢ (𝑥 = 0 → (𝐴↑𝑥) = (𝐴↑0)) |
2 | 1 | oveq2d 6926 |
. . . 4
⊢ (𝑥 = 0 → (𝑃 pCnt (𝐴↑𝑥)) = (𝑃 pCnt (𝐴↑0))) |
3 | | oveq1 6917 |
. . . 4
⊢ (𝑥 = 0 → (𝑥 · (𝑃 pCnt 𝐴)) = (0 · (𝑃 pCnt 𝐴))) |
4 | 2, 3 | eqeq12d 2840 |
. . 3
⊢ (𝑥 = 0 → ((𝑃 pCnt (𝐴↑𝑥)) = (𝑥 · (𝑃 pCnt 𝐴)) ↔ (𝑃 pCnt (𝐴↑0)) = (0 · (𝑃 pCnt 𝐴)))) |
5 | | oveq2 6918 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐴↑𝑥) = (𝐴↑𝑦)) |
6 | 5 | oveq2d 6926 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑃 pCnt (𝐴↑𝑥)) = (𝑃 pCnt (𝐴↑𝑦))) |
7 | | oveq1 6917 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑥 · (𝑃 pCnt 𝐴)) = (𝑦 · (𝑃 pCnt 𝐴))) |
8 | 6, 7 | eqeq12d 2840 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝑃 pCnt (𝐴↑𝑥)) = (𝑥 · (𝑃 pCnt 𝐴)) ↔ (𝑃 pCnt (𝐴↑𝑦)) = (𝑦 · (𝑃 pCnt 𝐴)))) |
9 | | oveq2 6918 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (𝐴↑𝑥) = (𝐴↑(𝑦 + 1))) |
10 | 9 | oveq2d 6926 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (𝑃 pCnt (𝐴↑𝑥)) = (𝑃 pCnt (𝐴↑(𝑦 + 1)))) |
11 | | oveq1 6917 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (𝑥 · (𝑃 pCnt 𝐴)) = ((𝑦 + 1) · (𝑃 pCnt 𝐴))) |
12 | 10, 11 | eqeq12d 2840 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → ((𝑃 pCnt (𝐴↑𝑥)) = (𝑥 · (𝑃 pCnt 𝐴)) ↔ (𝑃 pCnt (𝐴↑(𝑦 + 1))) = ((𝑦 + 1) · (𝑃 pCnt 𝐴)))) |
13 | | oveq2 6918 |
. . . . 5
⊢ (𝑥 = -𝑦 → (𝐴↑𝑥) = (𝐴↑-𝑦)) |
14 | 13 | oveq2d 6926 |
. . . 4
⊢ (𝑥 = -𝑦 → (𝑃 pCnt (𝐴↑𝑥)) = (𝑃 pCnt (𝐴↑-𝑦))) |
15 | | oveq1 6917 |
. . . 4
⊢ (𝑥 = -𝑦 → (𝑥 · (𝑃 pCnt 𝐴)) = (-𝑦 · (𝑃 pCnt 𝐴))) |
16 | 14, 15 | eqeq12d 2840 |
. . 3
⊢ (𝑥 = -𝑦 → ((𝑃 pCnt (𝐴↑𝑥)) = (𝑥 · (𝑃 pCnt 𝐴)) ↔ (𝑃 pCnt (𝐴↑-𝑦)) = (-𝑦 · (𝑃 pCnt 𝐴)))) |
17 | | oveq2 6918 |
. . . . 5
⊢ (𝑥 = 𝑁 → (𝐴↑𝑥) = (𝐴↑𝑁)) |
18 | 17 | oveq2d 6926 |
. . . 4
⊢ (𝑥 = 𝑁 → (𝑃 pCnt (𝐴↑𝑥)) = (𝑃 pCnt (𝐴↑𝑁))) |
19 | | oveq1 6917 |
. . . 4
⊢ (𝑥 = 𝑁 → (𝑥 · (𝑃 pCnt 𝐴)) = (𝑁 · (𝑃 pCnt 𝐴))) |
20 | 18, 19 | eqeq12d 2840 |
. . 3
⊢ (𝑥 = 𝑁 → ((𝑃 pCnt (𝐴↑𝑥)) = (𝑥 · (𝑃 pCnt 𝐴)) ↔ (𝑃 pCnt (𝐴↑𝑁)) = (𝑁 · (𝑃 pCnt 𝐴)))) |
21 | | pc1 15938 |
. . . . 5
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 1) = 0) |
22 | 21 | adantr 474 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt 1) = 0) |
23 | | qcn 12092 |
. . . . . . 7
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℂ) |
24 | 23 | ad2antrl 719 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → 𝐴 ∈
ℂ) |
25 | 24 | exp0d 13303 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝐴↑0) = 1) |
26 | 25 | oveq2d 6926 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt (𝐴↑0)) = (𝑃 pCnt 1)) |
27 | | pcqcl 15939 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt 𝐴) ∈ ℤ) |
28 | 27 | zcnd 11818 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt 𝐴) ∈ ℂ) |
29 | 28 | mul02d 10560 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (0 ·
(𝑃 pCnt 𝐴)) = 0) |
30 | 22, 26, 29 | 3eqtr4d 2871 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt (𝐴↑0)) = (0 · (𝑃 pCnt 𝐴))) |
31 | | oveq1 6917 |
. . . . 5
⊢ ((𝑃 pCnt (𝐴↑𝑦)) = (𝑦 · (𝑃 pCnt 𝐴)) → ((𝑃 pCnt (𝐴↑𝑦)) + (𝑃 pCnt 𝐴)) = ((𝑦 · (𝑃 pCnt 𝐴)) + (𝑃 pCnt 𝐴))) |
32 | | expp1 13168 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℕ0)
→ (𝐴↑(𝑦 + 1)) = ((𝐴↑𝑦) · 𝐴)) |
33 | 24, 32 | sylan 575 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ (𝐴↑(𝑦 + 1)) = ((𝐴↑𝑦) · 𝐴)) |
34 | 33 | oveq2d 6926 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ (𝑃 pCnt (𝐴↑(𝑦 + 1))) = (𝑃 pCnt ((𝐴↑𝑦) · 𝐴))) |
35 | | simpll 783 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ 𝑃 ∈
ℙ) |
36 | | simplrl 795 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ 𝐴 ∈
ℚ) |
37 | | simplrr 796 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ 𝐴 ≠
0) |
38 | | nn0z 11735 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℤ) |
39 | 38 | adantl 475 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ 𝑦 ∈
ℤ) |
40 | | qexpclz 13182 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ∧ 𝑦 ∈ ℤ) → (𝐴↑𝑦) ∈ ℚ) |
41 | 36, 37, 39, 40 | syl3anc 1494 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ (𝐴↑𝑦) ∈
ℚ) |
42 | 24 | adantr 474 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ 𝐴 ∈
ℂ) |
43 | 42, 37, 39 | expne0d 13315 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ (𝐴↑𝑦) ≠ 0) |
44 | | pcqmul 15936 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ ((𝐴↑𝑦) ∈ ℚ ∧ (𝐴↑𝑦) ≠ 0) ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt ((𝐴↑𝑦) · 𝐴)) = ((𝑃 pCnt (𝐴↑𝑦)) + (𝑃 pCnt 𝐴))) |
45 | 35, 41, 43, 36, 37, 44 | syl122anc 1502 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ (𝑃 pCnt ((𝐴↑𝑦) · 𝐴)) = ((𝑃 pCnt (𝐴↑𝑦)) + (𝑃 pCnt 𝐴))) |
46 | 34, 45 | eqtrd 2861 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ (𝑃 pCnt (𝐴↑(𝑦 + 1))) = ((𝑃 pCnt (𝐴↑𝑦)) + (𝑃 pCnt 𝐴))) |
47 | | nn0cn 11636 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℂ) |
48 | 47 | adantl 475 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ 𝑦 ∈
ℂ) |
49 | | 1cnd 10358 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ 1 ∈ ℂ) |
50 | 28 | adantr 474 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ (𝑃 pCnt 𝐴) ∈
ℂ) |
51 | 48, 49, 50 | adddird 10389 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ ((𝑦 + 1) ·
(𝑃 pCnt 𝐴)) = ((𝑦 · (𝑃 pCnt 𝐴)) + (1 · (𝑃 pCnt 𝐴)))) |
52 | 50 | mulid2d 10382 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ (1 · (𝑃 pCnt
𝐴)) = (𝑃 pCnt 𝐴)) |
53 | 52 | oveq2d 6926 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ ((𝑦 · (𝑃 pCnt 𝐴)) + (1 · (𝑃 pCnt 𝐴))) = ((𝑦 · (𝑃 pCnt 𝐴)) + (𝑃 pCnt 𝐴))) |
54 | 51, 53 | eqtrd 2861 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ ((𝑦 + 1) ·
(𝑃 pCnt 𝐴)) = ((𝑦 · (𝑃 pCnt 𝐴)) + (𝑃 pCnt 𝐴))) |
55 | 46, 54 | eqeq12d 2840 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ ((𝑃 pCnt (𝐴↑(𝑦 + 1))) = ((𝑦 + 1) · (𝑃 pCnt 𝐴)) ↔ ((𝑃 pCnt (𝐴↑𝑦)) + (𝑃 pCnt 𝐴)) = ((𝑦 · (𝑃 pCnt 𝐴)) + (𝑃 pCnt 𝐴)))) |
56 | 31, 55 | syl5ibr 238 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ ((𝑃 pCnt (𝐴↑𝑦)) = (𝑦 · (𝑃 pCnt 𝐴)) → (𝑃 pCnt (𝐴↑(𝑦 + 1))) = ((𝑦 + 1) · (𝑃 pCnt 𝐴)))) |
57 | 56 | ex 403 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑦 ∈ ℕ0
→ ((𝑃 pCnt (𝐴↑𝑦)) = (𝑦 · (𝑃 pCnt 𝐴)) → (𝑃 pCnt (𝐴↑(𝑦 + 1))) = ((𝑦 + 1) · (𝑃 pCnt 𝐴))))) |
58 | | negeq 10600 |
. . . . 5
⊢ ((𝑃 pCnt (𝐴↑𝑦)) = (𝑦 · (𝑃 pCnt 𝐴)) → -(𝑃 pCnt (𝐴↑𝑦)) = -(𝑦 · (𝑃 pCnt 𝐴))) |
59 | | nnnn0 11633 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) |
60 | | expneg 13169 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℕ0)
→ (𝐴↑-𝑦) = (1 / (𝐴↑𝑦))) |
61 | 24, 59, 60 | syl2an 589 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → (𝐴↑-𝑦) = (1 / (𝐴↑𝑦))) |
62 | 61 | oveq2d 6926 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (𝐴↑-𝑦)) = (𝑃 pCnt (1 / (𝐴↑𝑦)))) |
63 | | simpll 783 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈
ℙ) |
64 | 59, 41 | sylan2 586 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → (𝐴↑𝑦) ∈ ℚ) |
65 | 59, 43 | sylan2 586 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → (𝐴↑𝑦) ≠ 0) |
66 | | pcrec 15941 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ ((𝐴↑𝑦) ∈ ℚ ∧ (𝐴↑𝑦) ≠ 0)) → (𝑃 pCnt (1 / (𝐴↑𝑦))) = -(𝑃 pCnt (𝐴↑𝑦))) |
67 | 63, 64, 65, 66 | syl12anc 870 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (1 / (𝐴↑𝑦))) = -(𝑃 pCnt (𝐴↑𝑦))) |
68 | 62, 67 | eqtrd 2861 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (𝐴↑-𝑦)) = -(𝑃 pCnt (𝐴↑𝑦))) |
69 | | nncn 11366 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
70 | | mulneg1 10797 |
. . . . . . 7
⊢ ((𝑦 ∈ ℂ ∧ (𝑃 pCnt 𝐴) ∈ ℂ) → (-𝑦 · (𝑃 pCnt 𝐴)) = -(𝑦 · (𝑃 pCnt 𝐴))) |
71 | 69, 28, 70 | syl2anr 590 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → (-𝑦 · (𝑃 pCnt 𝐴)) = -(𝑦 · (𝑃 pCnt 𝐴))) |
72 | 68, 71 | eqeq12d 2840 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → ((𝑃 pCnt (𝐴↑-𝑦)) = (-𝑦 · (𝑃 pCnt 𝐴)) ↔ -(𝑃 pCnt (𝐴↑𝑦)) = -(𝑦 · (𝑃 pCnt 𝐴)))) |
73 | 58, 72 | syl5ibr 238 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) ∧ 𝑦 ∈ ℕ) → ((𝑃 pCnt (𝐴↑𝑦)) = (𝑦 · (𝑃 pCnt 𝐴)) → (𝑃 pCnt (𝐴↑-𝑦)) = (-𝑦 · (𝑃 pCnt 𝐴)))) |
74 | 73 | ex 403 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑦 ∈ ℕ → ((𝑃 pCnt (𝐴↑𝑦)) = (𝑦 · (𝑃 pCnt 𝐴)) → (𝑃 pCnt (𝐴↑-𝑦)) = (-𝑦 · (𝑃 pCnt 𝐴))))) |
75 | 4, 8, 12, 16, 20, 30, 57, 74 | zindd 11813 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑁 ∈ ℤ → (𝑃 pCnt (𝐴↑𝑁)) = (𝑁 · (𝑃 pCnt 𝐴)))) |
76 | 75 | 3impia 1149 |
1
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ 𝑁 ∈ ℤ) → (𝑃 pCnt (𝐴↑𝑁)) = (𝑁 · (𝑃 pCnt 𝐴))) |