Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑛 = (𝑑 · 𝑚) → (𝐿‘𝑛) = (𝐿‘(𝑑 · 𝑚))) |
2 | 1 | fveq2d 6107 |
. . . . . 6
⊢ (𝑛 = (𝑑 · 𝑚) → (𝑋‘(𝐿‘𝑛)) = (𝑋‘(𝐿‘(𝑑 · 𝑚)))) |
3 | | id 22 |
. . . . . 6
⊢ (𝑛 = (𝑑 · 𝑚) → 𝑛 = (𝑑 · 𝑚)) |
4 | 2, 3 | oveq12d 6567 |
. . . . 5
⊢ (𝑛 = (𝑑 · 𝑚) → ((𝑋‘(𝐿‘𝑛)) / 𝑛) = ((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚))) |
5 | | oveq2 6557 |
. . . . . 6
⊢ (𝑛 = (𝑑 · 𝑚) → (𝐴 / 𝑛) = (𝐴 / (𝑑 · 𝑚))) |
6 | 5 | fveq2d 6107 |
. . . . 5
⊢ (𝑛 = (𝑑 · 𝑚) → (log‘(𝐴 / 𝑛)) = (log‘(𝐴 / (𝑑 · 𝑚)))) |
7 | 4, 6 | oveq12d 6567 |
. . . 4
⊢ (𝑛 = (𝑑 · 𝑚) → (((𝑋‘(𝐿‘𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛))) = (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚))))) |
8 | 7 | oveq2d 6565 |
. . 3
⊢ (𝑛 = (𝑑 · 𝑚) → ((μ‘𝑑) · (((𝑋‘(𝐿‘𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛)))) = ((μ‘𝑑) · (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚)))))) |
9 | | dchrvmasum.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
10 | 9 | rpred 11748 |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) |
11 | | elrabi 3328 |
. . . . . . 7
⊢ (𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} → 𝑑 ∈ ℕ) |
12 | 11 | ad2antll 761 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛})) → 𝑑 ∈ ℕ) |
13 | | mucl 24667 |
. . . . . 6
⊢ (𝑑 ∈ ℕ →
(μ‘𝑑) ∈
ℤ) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛})) → (μ‘𝑑) ∈ ℤ) |
15 | 14 | zcnd 11359 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛})) → (μ‘𝑑) ∈ ℂ) |
16 | | rpvmasum.g |
. . . . . . . 8
⊢ 𝐺 = (DChr‘𝑁) |
17 | | rpvmasum.z |
. . . . . . . 8
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
18 | | rpvmasum.d |
. . . . . . . 8
⊢ 𝐷 = (Base‘𝐺) |
19 | | rpvmasum.l |
. . . . . . . 8
⊢ 𝐿 = (ℤRHom‘𝑍) |
20 | | dchrisum.b |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
21 | 20 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑋 ∈ 𝐷) |
22 | | elfzelz 12213 |
. . . . . . . . 9
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℤ) |
23 | 22 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℤ) |
24 | 16, 17, 18, 19, 21, 23 | dchrzrhcl 24770 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
25 | | elfznn 12241 |
. . . . . . . . 9
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℕ) |
26 | 25 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℕ) |
27 | 26 | nncnd 10913 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℂ) |
28 | 26 | nnne0d 10942 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ≠ 0) |
29 | 24, 27, 28 | divcld 10680 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑋‘(𝐿‘𝑛)) / 𝑛) ∈ ℂ) |
30 | 25 | nnrpd 11746 |
. . . . . . . . 9
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℝ+) |
31 | | rpdivcl 11732 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝐴 / 𝑛) ∈
ℝ+) |
32 | 9, 30, 31 | syl2an 493 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝐴 / 𝑛) ∈
ℝ+) |
33 | 32 | relogcld 24173 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (log‘(𝐴 / 𝑛)) ∈ ℝ) |
34 | 33 | recnd 9947 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (log‘(𝐴 / 𝑛)) ∈ ℂ) |
35 | 29, 34 | mulcld 9939 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (((𝑋‘(𝐿‘𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛))) ∈ ℂ) |
36 | 35 | adantrr 749 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛})) → (((𝑋‘(𝐿‘𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛))) ∈ ℂ) |
37 | 15, 36 | mulcld 9939 |
. . 3
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛})) → ((μ‘𝑑) · (((𝑋‘(𝐿‘𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛)))) ∈ ℂ) |
38 | 8, 10, 37 | dvdsflsumcom 24714 |
. 2
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ((μ‘𝑑) · (((𝑋‘(𝐿‘𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛)))) = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((μ‘𝑑) · (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚)))))) |
39 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑛 = 1 → (𝐿‘𝑛) = (𝐿‘1)) |
40 | 39 | fveq2d 6107 |
. . . . . 6
⊢ (𝑛 = 1 → (𝑋‘(𝐿‘𝑛)) = (𝑋‘(𝐿‘1))) |
41 | | id 22 |
. . . . . 6
⊢ (𝑛 = 1 → 𝑛 = 1) |
42 | 40, 41 | oveq12d 6567 |
. . . . 5
⊢ (𝑛 = 1 → ((𝑋‘(𝐿‘𝑛)) / 𝑛) = ((𝑋‘(𝐿‘1)) / 1)) |
43 | | oveq2 6557 |
. . . . . 6
⊢ (𝑛 = 1 → (𝐴 / 𝑛) = (𝐴 / 1)) |
44 | 43 | fveq2d 6107 |
. . . . 5
⊢ (𝑛 = 1 → (log‘(𝐴 / 𝑛)) = (log‘(𝐴 / 1))) |
45 | 42, 44 | oveq12d 6567 |
. . . 4
⊢ (𝑛 = 1 → (((𝑋‘(𝐿‘𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛))) = (((𝑋‘(𝐿‘1)) / 1) · (log‘(𝐴 / 1)))) |
46 | | fzfid 12634 |
. . . 4
⊢ (𝜑 → (1...(⌊‘𝐴)) ∈ Fin) |
47 | 25 | ssriv 3572 |
. . . . 5
⊢
(1...(⌊‘𝐴)) ⊆ ℕ |
48 | 47 | a1i 11 |
. . . 4
⊢ (𝜑 → (1...(⌊‘𝐴)) ⊆
ℕ) |
49 | | dchrvmasum2.2 |
. . . . . . 7
⊢ (𝜑 → 1 ≤ 𝐴) |
50 | | flge1nn 12484 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(⌊‘𝐴) ∈
ℕ) |
51 | 10, 49, 50 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (⌊‘𝐴) ∈
ℕ) |
52 | | nnuz 11599 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
53 | 51, 52 | syl6eleq 2698 |
. . . . 5
⊢ (𝜑 → (⌊‘𝐴) ∈
(ℤ≥‘1)) |
54 | | eluzfz1 12219 |
. . . . 5
⊢
((⌊‘𝐴)
∈ (ℤ≥‘1) → 1 ∈
(1...(⌊‘𝐴))) |
55 | 53, 54 | syl 17 |
. . . 4
⊢ (𝜑 → 1 ∈
(1...(⌊‘𝐴))) |
56 | 45, 46, 48, 55, 35 | musumsum 24718 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ((μ‘𝑑) · (((𝑋‘(𝐿‘𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛)))) = (((𝑋‘(𝐿‘1)) / 1) · (log‘(𝐴 / 1)))) |
57 | 16, 17, 18, 19, 20 | dchrzrh1 24769 |
. . . . . 6
⊢ (𝜑 → (𝑋‘(𝐿‘1)) = 1) |
58 | 57 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 → ((𝑋‘(𝐿‘1)) / 1) = (1 / 1)) |
59 | | 1div1e1 10596 |
. . . . 5
⊢ (1 / 1) =
1 |
60 | 58, 59 | syl6eq 2660 |
. . . 4
⊢ (𝜑 → ((𝑋‘(𝐿‘1)) / 1) = 1) |
61 | 9 | rpcnd 11750 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
62 | 61 | div1d 10672 |
. . . . 5
⊢ (𝜑 → (𝐴 / 1) = 𝐴) |
63 | 62 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (log‘(𝐴 / 1)) = (log‘𝐴)) |
64 | 60, 63 | oveq12d 6567 |
. . 3
⊢ (𝜑 → (((𝑋‘(𝐿‘1)) / 1) · (log‘(𝐴 / 1))) = (1 ·
(log‘𝐴))) |
65 | 9 | relogcld 24173 |
. . . . 5
⊢ (𝜑 → (log‘𝐴) ∈
ℝ) |
66 | 65 | recnd 9947 |
. . . 4
⊢ (𝜑 → (log‘𝐴) ∈
ℂ) |
67 | 66 | mulid2d 9937 |
. . 3
⊢ (𝜑 → (1 ·
(log‘𝐴)) =
(log‘𝐴)) |
68 | 56, 64, 67 | 3eqtrrd 2649 |
. 2
⊢ (𝜑 → (log‘𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ((μ‘𝑑) · (((𝑋‘(𝐿‘𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛))))) |
69 | | fzfid 12634 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (1...(⌊‘(𝐴 / 𝑑))) ∈ Fin) |
70 | 20 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → 𝑋 ∈ 𝐷) |
71 | | elfzelz 12213 |
. . . . . . . 8
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
→ 𝑑 ∈
ℤ) |
72 | 71 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → 𝑑 ∈ ℤ) |
73 | 16, 17, 18, 19, 70, 72 | dchrzrhcl 24770 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (𝑋‘(𝐿‘𝑑)) ∈ ℂ) |
74 | | fznnfl 12523 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ → (𝑑 ∈
(1...(⌊‘𝐴))
↔ (𝑑 ∈ ℕ
∧ 𝑑 ≤ 𝐴))) |
75 | 10, 74 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑑 ∈ (1...(⌊‘𝐴)) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴))) |
76 | 75 | simprbda 651 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → 𝑑 ∈ ℕ) |
77 | 76, 13 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (μ‘𝑑) ∈ ℤ) |
78 | 77 | zred 11358 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (μ‘𝑑) ∈ ℝ) |
79 | 78, 76 | nndivred 10946 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → ((μ‘𝑑) / 𝑑) ∈ ℝ) |
80 | 79 | recnd 9947 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → ((μ‘𝑑) / 𝑑) ∈ ℂ) |
81 | 73, 80 | mulcld 9939 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → ((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) ∈ ℂ) |
82 | 20 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑋 ∈ 𝐷) |
83 | | elfzelz 12213 |
. . . . . . . 8
⊢ (𝑚 ∈
(1...(⌊‘(𝐴 /
𝑑))) → 𝑚 ∈
ℤ) |
84 | 83 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑚 ∈ ℤ) |
85 | 16, 17, 18, 19, 82, 84 | dchrzrhcl 24770 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
86 | | elfznn 12241 |
. . . . . . . . . . . 12
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
→ 𝑑 ∈
ℕ) |
87 | 86 | nnrpd 11746 |
. . . . . . . . . . 11
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
→ 𝑑 ∈
ℝ+) |
88 | | rpdivcl 11732 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
ℝ+) → (𝐴 / 𝑑) ∈
ℝ+) |
89 | 9, 87, 88 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (𝐴 / 𝑑) ∈
ℝ+) |
90 | | elfznn 12241 |
. . . . . . . . . . 11
⊢ (𝑚 ∈
(1...(⌊‘(𝐴 /
𝑑))) → 𝑚 ∈
ℕ) |
91 | 90 | nnrpd 11746 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(1...(⌊‘(𝐴 /
𝑑))) → 𝑚 ∈
ℝ+) |
92 | | rpdivcl 11732 |
. . . . . . . . . 10
⊢ (((𝐴 / 𝑑) ∈ ℝ+ ∧ 𝑚 ∈ ℝ+)
→ ((𝐴 / 𝑑) / 𝑚) ∈
ℝ+) |
93 | 89, 91, 92 | syl2an 493 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝐴 / 𝑑) / 𝑚) ∈
ℝ+) |
94 | 93 | relogcld 24173 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (log‘((𝐴 / 𝑑) / 𝑚)) ∈ ℝ) |
95 | 90 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑚 ∈ ℕ) |
96 | 94, 95 | nndivred 10946 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚) ∈ ℝ) |
97 | 96 | recnd 9947 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚) ∈ ℂ) |
98 | 85, 97 | mulcld 9939 |
. . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝑋‘(𝐿‘𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚)) ∈ ℂ) |
99 | 69, 81, 98 | fsummulc2 14358 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿‘𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚))) = Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · ((𝑋‘(𝐿‘𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚)))) |
100 | 73 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (𝑋‘(𝐿‘𝑑)) ∈ ℂ) |
101 | 78 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (μ‘𝑑) ∈ ℝ) |
102 | 101 | recnd 9947 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (μ‘𝑑) ∈ ℂ) |
103 | 76 | nnrpd 11746 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → 𝑑 ∈ ℝ+) |
104 | 103 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑑 ∈ ℝ+) |
105 | 104 | rpcnne0d 11757 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (𝑑 ∈ ℂ ∧ 𝑑 ≠ 0)) |
106 | | div12 10586 |
. . . . . . . 8
⊢ (((𝑋‘(𝐿‘𝑑)) ∈ ℂ ∧ (μ‘𝑑) ∈ ℂ ∧ (𝑑 ∈ ℂ ∧ 𝑑 ≠ 0)) → ((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) = ((μ‘𝑑) · ((𝑋‘(𝐿‘𝑑)) / 𝑑))) |
107 | 100, 102,
105, 106 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) = ((μ‘𝑑) · ((𝑋‘(𝐿‘𝑑)) / 𝑑))) |
108 | 94 | recnd 9947 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (log‘((𝐴 / 𝑑) / 𝑚)) ∈ ℂ) |
109 | 95 | nnrpd 11746 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑚 ∈ ℝ+) |
110 | 109 | rpcnne0d 11757 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) |
111 | | div12 10586 |
. . . . . . . 8
⊢ (((𝑋‘(𝐿‘𝑚)) ∈ ℂ ∧ (log‘((𝐴 / 𝑑) / 𝑚)) ∈ ℂ ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → ((𝑋‘(𝐿‘𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚)) = ((log‘((𝐴 / 𝑑) / 𝑚)) · ((𝑋‘(𝐿‘𝑚)) / 𝑚))) |
112 | 85, 108, 110, 111 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝑋‘(𝐿‘𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚)) = ((log‘((𝐴 / 𝑑) / 𝑚)) · ((𝑋‘(𝐿‘𝑚)) / 𝑚))) |
113 | 107, 112 | oveq12d 6567 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · ((𝑋‘(𝐿‘𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚))) = (((μ‘𝑑) · ((𝑋‘(𝐿‘𝑑)) / 𝑑)) · ((log‘((𝐴 / 𝑑) / 𝑚)) · ((𝑋‘(𝐿‘𝑚)) / 𝑚)))) |
114 | 104 | rpcnd 11750 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑑 ∈ ℂ) |
115 | 104 | rpne0d 11753 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑑 ≠ 0) |
116 | 100, 114,
115 | divcld 10680 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝑋‘(𝐿‘𝑑)) / 𝑑) ∈ ℂ) |
117 | 95 | nncnd 10913 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑚 ∈ ℂ) |
118 | 95 | nnne0d 10942 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑚 ≠ 0) |
119 | 85, 117, 118 | divcld 10680 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝑋‘(𝐿‘𝑚)) / 𝑚) ∈ ℂ) |
120 | 116, 119 | mulcld 9939 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((𝑋‘(𝐿‘𝑑)) / 𝑑) · ((𝑋‘(𝐿‘𝑚)) / 𝑚)) ∈ ℂ) |
121 | 102, 108,
120 | mulassd 9942 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((μ‘𝑑) · (log‘((𝐴 / 𝑑) / 𝑚))) · (((𝑋‘(𝐿‘𝑑)) / 𝑑) · ((𝑋‘(𝐿‘𝑚)) / 𝑚))) = ((μ‘𝑑) · ((log‘((𝐴 / 𝑑) / 𝑚)) · (((𝑋‘(𝐿‘𝑑)) / 𝑑) · ((𝑋‘(𝐿‘𝑚)) / 𝑚))))) |
122 | 102, 116,
108, 119 | mul4d 10127 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((μ‘𝑑) · ((𝑋‘(𝐿‘𝑑)) / 𝑑)) · ((log‘((𝐴 / 𝑑) / 𝑚)) · ((𝑋‘(𝐿‘𝑚)) / 𝑚))) = (((μ‘𝑑) · (log‘((𝐴 / 𝑑) / 𝑚))) · (((𝑋‘(𝐿‘𝑑)) / 𝑑) · ((𝑋‘(𝐿‘𝑚)) / 𝑚)))) |
123 | 71 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑑 ∈ ℤ) |
124 | 16, 17, 18, 19, 82, 123, 84 | dchrzrhmul 24771 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (𝑋‘(𝐿‘(𝑑 · 𝑚))) = ((𝑋‘(𝐿‘𝑑)) · (𝑋‘(𝐿‘𝑚)))) |
125 | 124 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) = (((𝑋‘(𝐿‘𝑑)) · (𝑋‘(𝐿‘𝑚))) / (𝑑 · 𝑚))) |
126 | | divmuldiv 10604 |
. . . . . . . . . . . 12
⊢ ((((𝑋‘(𝐿‘𝑑)) ∈ ℂ ∧ (𝑋‘(𝐿‘𝑚)) ∈ ℂ) ∧ ((𝑑 ∈ ℂ ∧ 𝑑 ≠ 0) ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))) → (((𝑋‘(𝐿‘𝑑)) / 𝑑) · ((𝑋‘(𝐿‘𝑚)) / 𝑚)) = (((𝑋‘(𝐿‘𝑑)) · (𝑋‘(𝐿‘𝑚))) / (𝑑 · 𝑚))) |
127 | 100, 85, 105, 110, 126 | syl22anc 1319 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((𝑋‘(𝐿‘𝑑)) / 𝑑) · ((𝑋‘(𝐿‘𝑚)) / 𝑚)) = (((𝑋‘(𝐿‘𝑑)) · (𝑋‘(𝐿‘𝑚))) / (𝑑 · 𝑚))) |
128 | 125, 127 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) = (((𝑋‘(𝐿‘𝑑)) / 𝑑) · ((𝑋‘(𝐿‘𝑚)) / 𝑚))) |
129 | 61 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝐴 ∈ ℂ) |
130 | | divdiv1 10615 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ (𝑑 ∈ ℂ ∧ 𝑑 ≠ 0) ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → ((𝐴 / 𝑑) / 𝑚) = (𝐴 / (𝑑 · 𝑚))) |
131 | 129, 105,
110, 130 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝐴 / 𝑑) / 𝑚) = (𝐴 / (𝑑 · 𝑚))) |
132 | 131 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (𝐴 / (𝑑 · 𝑚)) = ((𝐴 / 𝑑) / 𝑚)) |
133 | 132 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (log‘(𝐴 / (𝑑 · 𝑚))) = (log‘((𝐴 / 𝑑) / 𝑚))) |
134 | 128, 133 | oveq12d 6567 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚)))) = ((((𝑋‘(𝐿‘𝑑)) / 𝑑) · ((𝑋‘(𝐿‘𝑚)) / 𝑚)) · (log‘((𝐴 / 𝑑) / 𝑚)))) |
135 | 120, 108 | mulcomd 9940 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((((𝑋‘(𝐿‘𝑑)) / 𝑑) · ((𝑋‘(𝐿‘𝑚)) / 𝑚)) · (log‘((𝐴 / 𝑑) / 𝑚))) = ((log‘((𝐴 / 𝑑) / 𝑚)) · (((𝑋‘(𝐿‘𝑑)) / 𝑑) · ((𝑋‘(𝐿‘𝑚)) / 𝑚)))) |
136 | 134, 135 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚)))) = ((log‘((𝐴 / 𝑑) / 𝑚)) · (((𝑋‘(𝐿‘𝑑)) / 𝑑) · ((𝑋‘(𝐿‘𝑚)) / 𝑚)))) |
137 | 136 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((μ‘𝑑) · (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚))))) = ((μ‘𝑑) · ((log‘((𝐴 / 𝑑) / 𝑚)) · (((𝑋‘(𝐿‘𝑑)) / 𝑑) · ((𝑋‘(𝐿‘𝑚)) / 𝑚))))) |
138 | 121, 122,
137 | 3eqtr4d 2654 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((μ‘𝑑) · ((𝑋‘(𝐿‘𝑑)) / 𝑑)) · ((log‘((𝐴 / 𝑑) / 𝑚)) · ((𝑋‘(𝐿‘𝑚)) / 𝑚))) = ((μ‘𝑑) · (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚)))))) |
139 | 113, 138 | eqtrd 2644 |
. . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · ((𝑋‘(𝐿‘𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚))) = ((μ‘𝑑) · (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚)))))) |
140 | 139 | sumeq2dv 14281 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · ((𝑋‘(𝐿‘𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚))) = Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((μ‘𝑑) · (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚)))))) |
141 | 99, 140 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ∈ (1...(⌊‘𝐴))) → (((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿‘𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚))) = Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((μ‘𝑑) · (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚)))))) |
142 | 141 | sumeq2dv 14281 |
. 2
⊢ (𝜑 → Σ𝑑 ∈ (1...(⌊‘𝐴))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿‘𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚))) = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((μ‘𝑑) · (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚)))))) |
143 | 38, 68, 142 | 3eqtr4d 2654 |
1
⊢ (𝜑 → (log‘𝐴) = Σ𝑑 ∈ (1...(⌊‘𝐴))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿‘𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚)))) |