Step | Hyp | Ref
| Expression |
1 | | elin 3796 |
. . . . . 6
⊢ (𝑝 ∈ ((1...𝐴) ∩ ℙ) ↔ (𝑝 ∈ (1...𝐴) ∧ 𝑝 ∈ ℙ)) |
2 | 1 | baib 944 |
. . . . 5
⊢ (𝑝 ∈ (1...𝐴) → (𝑝 ∈ ((1...𝐴) ∩ ℙ) ↔ 𝑝 ∈ ℙ)) |
3 | 2 | ifbid 4108 |
. . . 4
⊢ (𝑝 ∈ (1...𝐴) → if(𝑝 ∈ ((1...𝐴) ∩ ℙ), (log‘(𝑝↑(𝑝 pCnt 𝐴))), 0) = if(𝑝 ∈ ℙ, (log‘(𝑝↑(𝑝 pCnt 𝐴))), 0)) |
4 | | fvif 6204 |
. . . . 5
⊢
(log‘if(𝑝
∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1)) = if(𝑝 ∈ ℙ, (log‘(𝑝↑(𝑝 pCnt 𝐴))), (log‘1)) |
5 | | log1 24332 |
. . . . . 6
⊢
(log‘1) = 0 |
6 | | ifeq2 4091 |
. . . . . 6
⊢
((log‘1) = 0 → if(𝑝 ∈ ℙ, (log‘(𝑝↑(𝑝 pCnt 𝐴))), (log‘1)) = if(𝑝 ∈ ℙ, (log‘(𝑝↑(𝑝 pCnt 𝐴))), 0)) |
7 | 5, 6 | ax-mp 5 |
. . . . 5
⊢ if(𝑝 ∈ ℙ,
(log‘(𝑝↑(𝑝 pCnt 𝐴))), (log‘1)) = if(𝑝 ∈ ℙ, (log‘(𝑝↑(𝑝 pCnt 𝐴))), 0) |
8 | 4, 7 | eqtri 2644 |
. . . 4
⊢
(log‘if(𝑝
∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1)) = if(𝑝 ∈ ℙ, (log‘(𝑝↑(𝑝 pCnt 𝐴))), 0) |
9 | 3, 8 | syl6eqr 2674 |
. . 3
⊢ (𝑝 ∈ (1...𝐴) → if(𝑝 ∈ ((1...𝐴) ∩ ℙ), (log‘(𝑝↑(𝑝 pCnt 𝐴))), 0) = (log‘if(𝑝 ∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1))) |
10 | 9 | sumeq2i 14429 |
. 2
⊢
Σ𝑝 ∈
(1...𝐴)if(𝑝 ∈ ((1...𝐴) ∩ ℙ), (log‘(𝑝↑(𝑝 pCnt 𝐴))), 0) = Σ𝑝 ∈ (1...𝐴)(log‘if(𝑝 ∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1)) |
11 | | inss1 3833 |
. . . 4
⊢
((1...𝐴) ∩
ℙ) ⊆ (1...𝐴) |
12 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → 𝑝 ∈ ((1...𝐴) ∩ ℙ)) |
13 | 11, 12 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → 𝑝 ∈ (1...𝐴)) |
14 | | elfznn 12370 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (1...𝐴) → 𝑝 ∈ ℕ) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ) |
16 | | inss2 3834 |
. . . . . . . . . . 11
⊢
((1...𝐴) ∩
ℙ) ⊆ ℙ |
17 | 16, 12 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ) |
18 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → 𝐴 ∈ ℕ) |
19 | 17, 18 | pccld 15555 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
20 | 15, 19 | nnexpcld 13030 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (𝑝↑(𝑝 pCnt 𝐴)) ∈ ℕ) |
21 | 20 | nnrpd 11870 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (𝑝↑(𝑝 pCnt 𝐴)) ∈
ℝ+) |
22 | 21 | relogcld 24369 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (log‘(𝑝↑(𝑝 pCnt 𝐴))) ∈ ℝ) |
23 | 22 | recnd 10068 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (log‘(𝑝↑(𝑝 pCnt 𝐴))) ∈ ℂ) |
24 | 23 | ralrimiva 2966 |
. . . 4
⊢ (𝐴 ∈ ℕ →
∀𝑝 ∈
((1...𝐴) ∩
ℙ)(log‘(𝑝↑(𝑝 pCnt 𝐴))) ∈ ℂ) |
25 | | fzfi 12771 |
. . . . . 6
⊢
(1...𝐴) ∈
Fin |
26 | 25 | olci 406 |
. . . . 5
⊢
((1...𝐴) ⊆
(ℤ≥‘1) ∨ (1...𝐴) ∈ Fin) |
27 | | sumss2 14457 |
. . . . 5
⊢
(((((1...𝐴) ∩
ℙ) ⊆ (1...𝐴)
∧ ∀𝑝 ∈
((1...𝐴) ∩
ℙ)(log‘(𝑝↑(𝑝 pCnt 𝐴))) ∈ ℂ) ∧ ((1...𝐴) ⊆
(ℤ≥‘1) ∨ (1...𝐴) ∈ Fin)) → Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)(log‘(𝑝↑(𝑝 pCnt 𝐴))) = Σ𝑝 ∈ (1...𝐴)if(𝑝 ∈ ((1...𝐴) ∩ ℙ), (log‘(𝑝↑(𝑝 pCnt 𝐴))), 0)) |
28 | 26, 27 | mpan2 707 |
. . . 4
⊢
((((1...𝐴) ∩
ℙ) ⊆ (1...𝐴)
∧ ∀𝑝 ∈
((1...𝐴) ∩
ℙ)(log‘(𝑝↑(𝑝 pCnt 𝐴))) ∈ ℂ) → Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)(log‘(𝑝↑(𝑝 pCnt 𝐴))) = Σ𝑝 ∈ (1...𝐴)if(𝑝 ∈ ((1...𝐴) ∩ ℙ), (log‘(𝑝↑(𝑝 pCnt 𝐴))), 0)) |
29 | 11, 24, 28 | sylancr 695 |
. . 3
⊢ (𝐴 ∈ ℕ →
Σ𝑝 ∈ ((1...𝐴) ∩
ℙ)(log‘(𝑝↑(𝑝 pCnt 𝐴))) = Σ𝑝 ∈ (1...𝐴)if(𝑝 ∈ ((1...𝐴) ∩ ℙ), (log‘(𝑝↑(𝑝 pCnt 𝐴))), 0)) |
30 | 15 | nnrpd 11870 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ+) |
31 | 19 | nn0zd 11480 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (𝑝 pCnt 𝐴) ∈ ℤ) |
32 | | relogexp 24342 |
. . . . 5
⊢ ((𝑝 ∈ ℝ+
∧ (𝑝 pCnt 𝐴) ∈ ℤ) →
(log‘(𝑝↑(𝑝 pCnt 𝐴))) = ((𝑝 pCnt 𝐴) · (log‘𝑝))) |
33 | 30, 31, 32 | syl2anc 693 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (log‘(𝑝↑(𝑝 pCnt 𝐴))) = ((𝑝 pCnt 𝐴) · (log‘𝑝))) |
34 | 33 | sumeq2dv 14433 |
. . 3
⊢ (𝐴 ∈ ℕ →
Σ𝑝 ∈ ((1...𝐴) ∩
ℙ)(log‘(𝑝↑(𝑝 pCnt 𝐴))) = Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)((𝑝 pCnt 𝐴) · (log‘𝑝))) |
35 | 29, 34 | eqtr3d 2658 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑝 ∈ (1...𝐴)if(𝑝 ∈ ((1...𝐴) ∩ ℙ), (log‘(𝑝↑(𝑝 pCnt 𝐴))), 0) = Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)((𝑝 pCnt 𝐴) · (log‘𝑝))) |
36 | 14 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ (1...𝐴)) → 𝑝 ∈ ℕ) |
37 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑛 = 𝑝 → (𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ)) |
38 | | id 22 |
. . . . . . . . 9
⊢ (𝑛 = 𝑝 → 𝑛 = 𝑝) |
39 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑛 = 𝑝 → (𝑛 pCnt 𝐴) = (𝑝 pCnt 𝐴)) |
40 | 38, 39 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑛 = 𝑝 → (𝑛↑(𝑛 pCnt 𝐴)) = (𝑝↑(𝑝 pCnt 𝐴))) |
41 | 37, 40 | ifbieq1d 4109 |
. . . . . . 7
⊢ (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1) = if(𝑝 ∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1)) |
42 | 41 | fveq2d 6195 |
. . . . . 6
⊢ (𝑛 = 𝑝 → (log‘if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1)) = (log‘if(𝑝 ∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1))) |
43 | | eqid 2622 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦
(log‘if(𝑛 ∈
ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1))) = (𝑛 ∈ ℕ ↦ (log‘if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1))) |
44 | | fvex 6201 |
. . . . . 6
⊢
(log‘if(𝑝
∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1)) ∈ V |
45 | 42, 43, 44 | fvmpt 6282 |
. . . . 5
⊢ (𝑝 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(log‘if(𝑛 ∈
ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1)))‘𝑝) = (log‘if(𝑝 ∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1))) |
46 | 36, 45 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ (1...𝐴)) → ((𝑛 ∈ ℕ ↦ (log‘if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1)))‘𝑝) = (log‘if(𝑝 ∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1))) |
47 | | elnnuz 11724 |
. . . . 5
⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈
(ℤ≥‘1)) |
48 | 47 | biimpi 206 |
. . . 4
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
(ℤ≥‘1)) |
49 | 36 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ (1...𝐴)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℕ) |
50 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ (1...𝐴)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ) |
51 | | simpll 790 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ (1...𝐴)) ∧ 𝑝 ∈ ℙ) → 𝐴 ∈ ℕ) |
52 | 50, 51 | pccld 15555 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ (1...𝐴)) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
53 | 49, 52 | nnexpcld 13030 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ (1...𝐴)) ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt 𝐴)) ∈ ℕ) |
54 | | 1nn 11031 |
. . . . . . . . 9
⊢ 1 ∈
ℕ |
55 | 54 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ (1...𝐴)) ∧ ¬ 𝑝 ∈ ℙ) → 1 ∈
ℕ) |
56 | 53, 55 | ifclda 4120 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ (1...𝐴)) → if(𝑝 ∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1) ∈ ℕ) |
57 | 56 | nnrpd 11870 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ (1...𝐴)) → if(𝑝 ∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1) ∈
ℝ+) |
58 | 57 | relogcld 24369 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ (1...𝐴)) → (log‘if(𝑝 ∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1)) ∈ ℝ) |
59 | 58 | recnd 10068 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ (1...𝐴)) → (log‘if(𝑝 ∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1)) ∈ ℂ) |
60 | 46, 48, 59 | fsumser 14461 |
. . 3
⊢ (𝐴 ∈ ℕ →
Σ𝑝 ∈ (1...𝐴)(log‘if(𝑝 ∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1)) = (seq1( + , (𝑛 ∈ ℕ ↦ (log‘if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1))))‘𝐴)) |
61 | | rpmulcl 11855 |
. . . . 5
⊢ ((𝑝 ∈ ℝ+
∧ 𝑚 ∈
ℝ+) → (𝑝 · 𝑚) ∈
ℝ+) |
62 | 61 | adantl 482 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ (𝑝 ∈ ℝ+
∧ 𝑚 ∈
ℝ+)) → (𝑝 · 𝑚) ∈
ℝ+) |
63 | | eqid 2622 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1)) |
64 | | ovex 6678 |
. . . . . . . 8
⊢ (𝑝↑(𝑝 pCnt 𝐴)) ∈ V |
65 | | 1ex 10035 |
. . . . . . . 8
⊢ 1 ∈
V |
66 | 64, 65 | ifex 4156 |
. . . . . . 7
⊢ if(𝑝 ∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1) ∈ V |
67 | 41, 63, 66 | fvmpt 6282 |
. . . . . 6
⊢ (𝑝 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1)) |
68 | 36, 67 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ (1...𝐴)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1)) |
69 | 68, 57 | eqeltrd 2701 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ (1...𝐴)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1))‘𝑝) ∈
ℝ+) |
70 | | relogmul 24338 |
. . . . 5
⊢ ((𝑝 ∈ ℝ+
∧ 𝑚 ∈
ℝ+) → (log‘(𝑝 · 𝑚)) = ((log‘𝑝) + (log‘𝑚))) |
71 | 70 | adantl 482 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ (𝑝 ∈ ℝ+
∧ 𝑚 ∈
ℝ+)) → (log‘(𝑝 · 𝑚)) = ((log‘𝑝) + (log‘𝑚))) |
72 | 68 | fveq2d 6195 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ (1...𝐴)) → (log‘((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1))‘𝑝)) = (log‘if(𝑝 ∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1))) |
73 | 72, 46 | eqtr4d 2659 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ (1...𝐴)) → (log‘((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1))‘𝑝)) = ((𝑛 ∈ ℕ ↦ (log‘if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1)))‘𝑝)) |
74 | 62, 69, 48, 71, 73 | seqhomo 12848 |
. . 3
⊢ (𝐴 ∈ ℕ →
(log‘(seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1)))‘𝐴)) = (seq1( + , (𝑛 ∈ ℕ ↦ (log‘if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1))))‘𝐴)) |
75 | 63 | pcprod 15599 |
. . . 4
⊢ (𝐴 ∈ ℕ → (seq1(
· , (𝑛 ∈
ℕ ↦ if(𝑛 ∈
ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1)))‘𝐴) = 𝐴) |
76 | 75 | fveq2d 6195 |
. . 3
⊢ (𝐴 ∈ ℕ →
(log‘(seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝐴)), 1)))‘𝐴)) = (log‘𝐴)) |
77 | 60, 74, 76 | 3eqtr2d 2662 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑝 ∈ (1...𝐴)(log‘if(𝑝 ∈ ℙ, (𝑝↑(𝑝 pCnt 𝐴)), 1)) = (log‘𝐴)) |
78 | 10, 35, 77 | 3eqtr3a 2680 |
1
⊢ (𝐴 ∈ ℕ →
Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)((𝑝 pCnt 𝐴) · (log‘𝑝)) = (log‘𝐴)) |