MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrvmasum2lem Structured version   Visualization version   GIF version

Theorem dchrvmasum2lem 26840
Description: Give an expression for log𝑥 remarkably similar to Σ𝑛𝑥(𝑋(𝑛)Λ(𝑛) / 𝑛) given in dchrvmasumlem1 26839. Part of Lemma 9.4.3 of [Shapiro], p. 380. (Contributed by Mario Carneiro, 4-May-2016.)
Hypotheses
Ref Expression
rpvmasum.z 𝑍 = (ℤ/nℤ‘𝑁)
rpvmasum.l 𝐿 = (ℤRHom‘𝑍)
rpvmasum.a (𝜑𝑁 ∈ ℕ)
rpvmasum.g 𝐺 = (DChr‘𝑁)
rpvmasum.d 𝐷 = (Base‘𝐺)
rpvmasum.1 1 = (0g𝐺)
dchrisum.b (𝜑𝑋𝐷)
dchrisum.n1 (𝜑𝑋1 )
dchrvmasum.a (𝜑𝐴 ∈ ℝ+)
dchrvmasum2.2 (𝜑 → 1 ≤ 𝐴)
Assertion
Ref Expression
dchrvmasum2lem (𝜑 → (log‘𝐴) = Σ𝑑 ∈ (1...(⌊‘𝐴))(((𝑋‘(𝐿𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚))))
Distinct variable groups:   1 ,𝑚   𝑚,𝑑,𝐴   𝑚,𝑁   𝜑,𝑑,𝑚   𝑚,𝑍   𝐷,𝑚   𝐿,𝑑,𝑚   𝑋,𝑑,𝑚
Allowed substitution hints:   𝐷(𝑑)   1 (𝑑)   𝐺(𝑚,𝑑)   𝑁(𝑑)   𝑍(𝑑)

Proof of Theorem dchrvmasum2lem
Dummy variables 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2fveq3 6845 . . . . . 6 (𝑛 = (𝑑 · 𝑚) → (𝑋‘(𝐿𝑛)) = (𝑋‘(𝐿‘(𝑑 · 𝑚))))
2 id 22 . . . . . 6 (𝑛 = (𝑑 · 𝑚) → 𝑛 = (𝑑 · 𝑚))
31, 2oveq12d 7372 . . . . 5 (𝑛 = (𝑑 · 𝑚) → ((𝑋‘(𝐿𝑛)) / 𝑛) = ((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)))
4 oveq2 7362 . . . . . 6 (𝑛 = (𝑑 · 𝑚) → (𝐴 / 𝑛) = (𝐴 / (𝑑 · 𝑚)))
54fveq2d 6844 . . . . 5 (𝑛 = (𝑑 · 𝑚) → (log‘(𝐴 / 𝑛)) = (log‘(𝐴 / (𝑑 · 𝑚))))
63, 5oveq12d 7372 . . . 4 (𝑛 = (𝑑 · 𝑚) → (((𝑋‘(𝐿𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛))) = (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚)))))
76oveq2d 7370 . . 3 (𝑛 = (𝑑 · 𝑚) → ((μ‘𝑑) · (((𝑋‘(𝐿𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛)))) = ((μ‘𝑑) · (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚))))))
8 dchrvmasum.a . . . 4 (𝜑𝐴 ∈ ℝ+)
98rpred 12954 . . 3 (𝜑𝐴 ∈ ℝ)
10 elrabi 3638 . . . . . . 7 (𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑛} → 𝑑 ∈ ℕ)
1110ad2antll 727 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑛})) → 𝑑 ∈ ℕ)
12 mucl 26486 . . . . . 6 (𝑑 ∈ ℕ → (μ‘𝑑) ∈ ℤ)
1311, 12syl 17 . . . . 5 ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑛})) → (μ‘𝑑) ∈ ℤ)
1413zcnd 12605 . . . 4 ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑛})) → (μ‘𝑑) ∈ ℂ)
15 rpvmasum.g . . . . . . . 8 𝐺 = (DChr‘𝑁)
16 rpvmasum.z . . . . . . . 8 𝑍 = (ℤ/nℤ‘𝑁)
17 rpvmasum.d . . . . . . . 8 𝐷 = (Base‘𝐺)
18 rpvmasum.l . . . . . . . 8 𝐿 = (ℤRHom‘𝑍)
19 dchrisum.b . . . . . . . . 9 (𝜑𝑋𝐷)
2019adantr 481 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 𝑋𝐷)
21 elfzelz 13438 . . . . . . . . 9 (𝑛 ∈ (1...(⌊‘𝐴)) → 𝑛 ∈ ℤ)
2221adantl 482 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℤ)
2315, 16, 17, 18, 20, 22dchrzrhcl 26589 . . . . . . 7 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
24 elfznn 13467 . . . . . . . . 9 (𝑛 ∈ (1...(⌊‘𝐴)) → 𝑛 ∈ ℕ)
2524adantl 482 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℕ)
2625nncnd 12166 . . . . . . 7 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℂ)
2725nnne0d 12200 . . . . . . 7 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ≠ 0)
2823, 26, 27divcld 11928 . . . . . 6 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑋‘(𝐿𝑛)) / 𝑛) ∈ ℂ)
2924nnrpd 12952 . . . . . . . . 9 (𝑛 ∈ (1...(⌊‘𝐴)) → 𝑛 ∈ ℝ+)
30 rpdivcl 12937 . . . . . . . . 9 ((𝐴 ∈ ℝ+𝑛 ∈ ℝ+) → (𝐴 / 𝑛) ∈ ℝ+)
318, 29, 30syl2an 596 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (𝐴 / 𝑛) ∈ ℝ+)
3231relogcld 25974 . . . . . . 7 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (log‘(𝐴 / 𝑛)) ∈ ℝ)
3332recnd 11180 . . . . . 6 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (log‘(𝐴 / 𝑛)) ∈ ℂ)
3428, 33mulcld 11172 . . . . 5 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (((𝑋‘(𝐿𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛))) ∈ ℂ)
3534adantrr 715 . . . 4 ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑛})) → (((𝑋‘(𝐿𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛))) ∈ ℂ)
3614, 35mulcld 11172 . . 3 ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑛})) → ((μ‘𝑑) · (((𝑋‘(𝐿𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛)))) ∈ ℂ)
377, 9, 36dvdsflsumcom 26533 . 2 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑛} ((μ‘𝑑) · (((𝑋‘(𝐿𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛)))) = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((μ‘𝑑) · (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚))))))
38 2fveq3 6845 . . . . . 6 (𝑛 = 1 → (𝑋‘(𝐿𝑛)) = (𝑋‘(𝐿‘1)))
39 id 22 . . . . . 6 (𝑛 = 1 → 𝑛 = 1)
4038, 39oveq12d 7372 . . . . 5 (𝑛 = 1 → ((𝑋‘(𝐿𝑛)) / 𝑛) = ((𝑋‘(𝐿‘1)) / 1))
41 oveq2 7362 . . . . . 6 (𝑛 = 1 → (𝐴 / 𝑛) = (𝐴 / 1))
4241fveq2d 6844 . . . . 5 (𝑛 = 1 → (log‘(𝐴 / 𝑛)) = (log‘(𝐴 / 1)))
4340, 42oveq12d 7372 . . . 4 (𝑛 = 1 → (((𝑋‘(𝐿𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛))) = (((𝑋‘(𝐿‘1)) / 1) · (log‘(𝐴 / 1))))
44 fzfid 13875 . . . 4 (𝜑 → (1...(⌊‘𝐴)) ∈ Fin)
45 fz1ssnn 13469 . . . . 5 (1...(⌊‘𝐴)) ⊆ ℕ
4645a1i 11 . . . 4 (𝜑 → (1...(⌊‘𝐴)) ⊆ ℕ)
47 dchrvmasum2.2 . . . . . . 7 (𝜑 → 1 ≤ 𝐴)
48 flge1nn 13723 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ)
499, 47, 48syl2anc 584 . . . . . 6 (𝜑 → (⌊‘𝐴) ∈ ℕ)
50 nnuz 12803 . . . . . 6 ℕ = (ℤ‘1)
5149, 50eleqtrdi 2848 . . . . 5 (𝜑 → (⌊‘𝐴) ∈ (ℤ‘1))
52 eluzfz1 13445 . . . . 5 ((⌊‘𝐴) ∈ (ℤ‘1) → 1 ∈ (1...(⌊‘𝐴)))
5351, 52syl 17 . . . 4 (𝜑 → 1 ∈ (1...(⌊‘𝐴)))
5443, 44, 46, 53, 34musumsum 26537 . . 3 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑛} ((μ‘𝑑) · (((𝑋‘(𝐿𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛)))) = (((𝑋‘(𝐿‘1)) / 1) · (log‘(𝐴 / 1))))
5515, 16, 17, 18, 19dchrzrh1 26588 . . . . . 6 (𝜑 → (𝑋‘(𝐿‘1)) = 1)
5655oveq1d 7369 . . . . 5 (𝜑 → ((𝑋‘(𝐿‘1)) / 1) = (1 / 1))
57 1div1e1 11842 . . . . 5 (1 / 1) = 1
5856, 57eqtrdi 2792 . . . 4 (𝜑 → ((𝑋‘(𝐿‘1)) / 1) = 1)
598rpcnd 12956 . . . . . 6 (𝜑𝐴 ∈ ℂ)
6059div1d 11920 . . . . 5 (𝜑 → (𝐴 / 1) = 𝐴)
6160fveq2d 6844 . . . 4 (𝜑 → (log‘(𝐴 / 1)) = (log‘𝐴))
6258, 61oveq12d 7372 . . 3 (𝜑 → (((𝑋‘(𝐿‘1)) / 1) · (log‘(𝐴 / 1))) = (1 · (log‘𝐴)))
638relogcld 25974 . . . . 5 (𝜑 → (log‘𝐴) ∈ ℝ)
6463recnd 11180 . . . 4 (𝜑 → (log‘𝐴) ∈ ℂ)
6564mulid2d 11170 . . 3 (𝜑 → (1 · (log‘𝐴)) = (log‘𝐴))
6654, 62, 653eqtrrd 2781 . 2 (𝜑 → (log‘𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑛} ((μ‘𝑑) · (((𝑋‘(𝐿𝑛)) / 𝑛) · (log‘(𝐴 / 𝑛)))))
67 fzfid 13875 . . . . 5 ((𝜑𝑑 ∈ (1...(⌊‘𝐴))) → (1...(⌊‘(𝐴 / 𝑑))) ∈ Fin)
6819adantr 481 . . . . . . 7 ((𝜑𝑑 ∈ (1...(⌊‘𝐴))) → 𝑋𝐷)
69 elfzelz 13438 . . . . . . . 8 (𝑑 ∈ (1...(⌊‘𝐴)) → 𝑑 ∈ ℤ)
7069adantl 482 . . . . . . 7 ((𝜑𝑑 ∈ (1...(⌊‘𝐴))) → 𝑑 ∈ ℤ)
7115, 16, 17, 18, 68, 70dchrzrhcl 26589 . . . . . 6 ((𝜑𝑑 ∈ (1...(⌊‘𝐴))) → (𝑋‘(𝐿𝑑)) ∈ ℂ)
72 fznnfl 13764 . . . . . . . . . . . 12 (𝐴 ∈ ℝ → (𝑑 ∈ (1...(⌊‘𝐴)) ↔ (𝑑 ∈ ℕ ∧ 𝑑𝐴)))
739, 72syl 17 . . . . . . . . . . 11 (𝜑 → (𝑑 ∈ (1...(⌊‘𝐴)) ↔ (𝑑 ∈ ℕ ∧ 𝑑𝐴)))
7473simprbda 499 . . . . . . . . . 10 ((𝜑𝑑 ∈ (1...(⌊‘𝐴))) → 𝑑 ∈ ℕ)
7574, 12syl 17 . . . . . . . . 9 ((𝜑𝑑 ∈ (1...(⌊‘𝐴))) → (μ‘𝑑) ∈ ℤ)
7675zred 12604 . . . . . . . 8 ((𝜑𝑑 ∈ (1...(⌊‘𝐴))) → (μ‘𝑑) ∈ ℝ)
7776, 74nndivred 12204 . . . . . . 7 ((𝜑𝑑 ∈ (1...(⌊‘𝐴))) → ((μ‘𝑑) / 𝑑) ∈ ℝ)
7877recnd 11180 . . . . . 6 ((𝜑𝑑 ∈ (1...(⌊‘𝐴))) → ((μ‘𝑑) / 𝑑) ∈ ℂ)
7971, 78mulcld 11172 . . . . 5 ((𝜑𝑑 ∈ (1...(⌊‘𝐴))) → ((𝑋‘(𝐿𝑑)) · ((μ‘𝑑) / 𝑑)) ∈ ℂ)
8019ad2antrr 724 . . . . . . 7 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑋𝐷)
81 elfzelz 13438 . . . . . . . 8 (𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑))) → 𝑚 ∈ ℤ)
8281adantl 482 . . . . . . 7 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑚 ∈ ℤ)
8315, 16, 17, 18, 80, 82dchrzrhcl 26589 . . . . . 6 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (𝑋‘(𝐿𝑚)) ∈ ℂ)
84 elfznn 13467 . . . . . . . . . . . 12 (𝑑 ∈ (1...(⌊‘𝐴)) → 𝑑 ∈ ℕ)
8584nnrpd 12952 . . . . . . . . . . 11 (𝑑 ∈ (1...(⌊‘𝐴)) → 𝑑 ∈ ℝ+)
86 rpdivcl 12937 . . . . . . . . . . 11 ((𝐴 ∈ ℝ+𝑑 ∈ ℝ+) → (𝐴 / 𝑑) ∈ ℝ+)
878, 85, 86syl2an 596 . . . . . . . . . 10 ((𝜑𝑑 ∈ (1...(⌊‘𝐴))) → (𝐴 / 𝑑) ∈ ℝ+)
88 elfznn 13467 . . . . . . . . . . 11 (𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑))) → 𝑚 ∈ ℕ)
8988nnrpd 12952 . . . . . . . . . 10 (𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑))) → 𝑚 ∈ ℝ+)
90 rpdivcl 12937 . . . . . . . . . 10 (((𝐴 / 𝑑) ∈ ℝ+𝑚 ∈ ℝ+) → ((𝐴 / 𝑑) / 𝑚) ∈ ℝ+)
9187, 89, 90syl2an 596 . . . . . . . . 9 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝐴 / 𝑑) / 𝑚) ∈ ℝ+)
9291relogcld 25974 . . . . . . . 8 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (log‘((𝐴 / 𝑑) / 𝑚)) ∈ ℝ)
9388adantl 482 . . . . . . . 8 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑚 ∈ ℕ)
9492, 93nndivred 12204 . . . . . . 7 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚) ∈ ℝ)
9594recnd 11180 . . . . . 6 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚) ∈ ℂ)
9683, 95mulcld 11172 . . . . 5 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝑋‘(𝐿𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚)) ∈ ℂ)
9767, 79, 96fsummulc2 15666 . . . 4 ((𝜑𝑑 ∈ (1...(⌊‘𝐴))) → (((𝑋‘(𝐿𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚))) = Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))(((𝑋‘(𝐿𝑑)) · ((μ‘𝑑) / 𝑑)) · ((𝑋‘(𝐿𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚))))
9871adantr 481 . . . . . . . 8 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (𝑋‘(𝐿𝑑)) ∈ ℂ)
9976adantr 481 . . . . . . . . 9 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (μ‘𝑑) ∈ ℝ)
10099recnd 11180 . . . . . . . 8 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (μ‘𝑑) ∈ ℂ)
10174nnrpd 12952 . . . . . . . . . 10 ((𝜑𝑑 ∈ (1...(⌊‘𝐴))) → 𝑑 ∈ ℝ+)
102101adantr 481 . . . . . . . . 9 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑑 ∈ ℝ+)
103102rpcnne0d 12963 . . . . . . . 8 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (𝑑 ∈ ℂ ∧ 𝑑 ≠ 0))
104 div12 11832 . . . . . . . 8 (((𝑋‘(𝐿𝑑)) ∈ ℂ ∧ (μ‘𝑑) ∈ ℂ ∧ (𝑑 ∈ ℂ ∧ 𝑑 ≠ 0)) → ((𝑋‘(𝐿𝑑)) · ((μ‘𝑑) / 𝑑)) = ((μ‘𝑑) · ((𝑋‘(𝐿𝑑)) / 𝑑)))
10598, 100, 103, 104syl3anc 1371 . . . . . . 7 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝑋‘(𝐿𝑑)) · ((μ‘𝑑) / 𝑑)) = ((μ‘𝑑) · ((𝑋‘(𝐿𝑑)) / 𝑑)))
10692recnd 11180 . . . . . . . 8 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (log‘((𝐴 / 𝑑) / 𝑚)) ∈ ℂ)
10793nnrpd 12952 . . . . . . . . 9 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑚 ∈ ℝ+)
108107rpcnne0d 12963 . . . . . . . 8 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
109 div12 11832 . . . . . . . 8 (((𝑋‘(𝐿𝑚)) ∈ ℂ ∧ (log‘((𝐴 / 𝑑) / 𝑚)) ∈ ℂ ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → ((𝑋‘(𝐿𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚)) = ((log‘((𝐴 / 𝑑) / 𝑚)) · ((𝑋‘(𝐿𝑚)) / 𝑚)))
11083, 106, 108, 109syl3anc 1371 . . . . . . 7 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝑋‘(𝐿𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚)) = ((log‘((𝐴 / 𝑑) / 𝑚)) · ((𝑋‘(𝐿𝑚)) / 𝑚)))
111105, 110oveq12d 7372 . . . . . 6 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((𝑋‘(𝐿𝑑)) · ((μ‘𝑑) / 𝑑)) · ((𝑋‘(𝐿𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚))) = (((μ‘𝑑) · ((𝑋‘(𝐿𝑑)) / 𝑑)) · ((log‘((𝐴 / 𝑑) / 𝑚)) · ((𝑋‘(𝐿𝑚)) / 𝑚))))
112102rpcnd 12956 . . . . . . . . . 10 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑑 ∈ ℂ)
113102rpne0d 12959 . . . . . . . . . 10 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑑 ≠ 0)
11498, 112, 113divcld 11928 . . . . . . . . 9 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝑋‘(𝐿𝑑)) / 𝑑) ∈ ℂ)
11593nncnd 12166 . . . . . . . . . 10 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑚 ∈ ℂ)
11693nnne0d 12200 . . . . . . . . . 10 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑚 ≠ 0)
11783, 115, 116divcld 11928 . . . . . . . . 9 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝑋‘(𝐿𝑚)) / 𝑚) ∈ ℂ)
118114, 117mulcld 11172 . . . . . . . 8 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((𝑋‘(𝐿𝑑)) / 𝑑) · ((𝑋‘(𝐿𝑚)) / 𝑚)) ∈ ℂ)
119100, 106, 118mulassd 11175 . . . . . . 7 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((μ‘𝑑) · (log‘((𝐴 / 𝑑) / 𝑚))) · (((𝑋‘(𝐿𝑑)) / 𝑑) · ((𝑋‘(𝐿𝑚)) / 𝑚))) = ((μ‘𝑑) · ((log‘((𝐴 / 𝑑) / 𝑚)) · (((𝑋‘(𝐿𝑑)) / 𝑑) · ((𝑋‘(𝐿𝑚)) / 𝑚)))))
120100, 114, 106, 117mul4d 11364 . . . . . . 7 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((μ‘𝑑) · ((𝑋‘(𝐿𝑑)) / 𝑑)) · ((log‘((𝐴 / 𝑑) / 𝑚)) · ((𝑋‘(𝐿𝑚)) / 𝑚))) = (((μ‘𝑑) · (log‘((𝐴 / 𝑑) / 𝑚))) · (((𝑋‘(𝐿𝑑)) / 𝑑) · ((𝑋‘(𝐿𝑚)) / 𝑚))))
12169ad2antlr 725 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝑑 ∈ ℤ)
12215, 16, 17, 18, 80, 121, 82dchrzrhmul 26590 . . . . . . . . . . . 12 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (𝑋‘(𝐿‘(𝑑 · 𝑚))) = ((𝑋‘(𝐿𝑑)) · (𝑋‘(𝐿𝑚))))
123122oveq1d 7369 . . . . . . . . . . 11 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) = (((𝑋‘(𝐿𝑑)) · (𝑋‘(𝐿𝑚))) / (𝑑 · 𝑚)))
124 divmuldiv 11852 . . . . . . . . . . . 12 ((((𝑋‘(𝐿𝑑)) ∈ ℂ ∧ (𝑋‘(𝐿𝑚)) ∈ ℂ) ∧ ((𝑑 ∈ ℂ ∧ 𝑑 ≠ 0) ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))) → (((𝑋‘(𝐿𝑑)) / 𝑑) · ((𝑋‘(𝐿𝑚)) / 𝑚)) = (((𝑋‘(𝐿𝑑)) · (𝑋‘(𝐿𝑚))) / (𝑑 · 𝑚)))
12598, 83, 103, 108, 124syl22anc 837 . . . . . . . . . . 11 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((𝑋‘(𝐿𝑑)) / 𝑑) · ((𝑋‘(𝐿𝑚)) / 𝑚)) = (((𝑋‘(𝐿𝑑)) · (𝑋‘(𝐿𝑚))) / (𝑑 · 𝑚)))
126123, 125eqtr4d 2779 . . . . . . . . . 10 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) = (((𝑋‘(𝐿𝑑)) / 𝑑) · ((𝑋‘(𝐿𝑚)) / 𝑚)))
12759ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → 𝐴 ∈ ℂ)
128 divdiv1 11863 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ (𝑑 ∈ ℂ ∧ 𝑑 ≠ 0) ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → ((𝐴 / 𝑑) / 𝑚) = (𝐴 / (𝑑 · 𝑚)))
129127, 103, 108, 128syl3anc 1371 . . . . . . . . . . . 12 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((𝐴 / 𝑑) / 𝑚) = (𝐴 / (𝑑 · 𝑚)))
130129eqcomd 2742 . . . . . . . . . . 11 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (𝐴 / (𝑑 · 𝑚)) = ((𝐴 / 𝑑) / 𝑚))
131130fveq2d 6844 . . . . . . . . . 10 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (log‘(𝐴 / (𝑑 · 𝑚))) = (log‘((𝐴 / 𝑑) / 𝑚)))
132126, 131oveq12d 7372 . . . . . . . . 9 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚)))) = ((((𝑋‘(𝐿𝑑)) / 𝑑) · ((𝑋‘(𝐿𝑚)) / 𝑚)) · (log‘((𝐴 / 𝑑) / 𝑚))))
133118, 106mulcomd 11173 . . . . . . . . 9 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((((𝑋‘(𝐿𝑑)) / 𝑑) · ((𝑋‘(𝐿𝑚)) / 𝑚)) · (log‘((𝐴 / 𝑑) / 𝑚))) = ((log‘((𝐴 / 𝑑) / 𝑚)) · (((𝑋‘(𝐿𝑑)) / 𝑑) · ((𝑋‘(𝐿𝑚)) / 𝑚))))
134132, 133eqtrd 2776 . . . . . . . 8 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚)))) = ((log‘((𝐴 / 𝑑) / 𝑚)) · (((𝑋‘(𝐿𝑑)) / 𝑑) · ((𝑋‘(𝐿𝑚)) / 𝑚))))
135134oveq2d 7370 . . . . . . 7 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → ((μ‘𝑑) · (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚))))) = ((μ‘𝑑) · ((log‘((𝐴 / 𝑑) / 𝑚)) · (((𝑋‘(𝐿𝑑)) / 𝑑) · ((𝑋‘(𝐿𝑚)) / 𝑚)))))
136119, 120, 1353eqtr4d 2786 . . . . . 6 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((μ‘𝑑) · ((𝑋‘(𝐿𝑑)) / 𝑑)) · ((log‘((𝐴 / 𝑑) / 𝑚)) · ((𝑋‘(𝐿𝑚)) / 𝑚))) = ((μ‘𝑑) · (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚))))))
137111, 136eqtrd 2776 . . . . 5 (((𝜑𝑑 ∈ (1...(⌊‘𝐴))) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))) → (((𝑋‘(𝐿𝑑)) · ((μ‘𝑑) / 𝑑)) · ((𝑋‘(𝐿𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚))) = ((μ‘𝑑) · (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚))))))
138137sumeq2dv 15585 . . . 4 ((𝜑𝑑 ∈ (1...(⌊‘𝐴))) → Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))(((𝑋‘(𝐿𝑑)) · ((μ‘𝑑) / 𝑑)) · ((𝑋‘(𝐿𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚))) = Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((μ‘𝑑) · (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚))))))
13997, 138eqtrd 2776 . . 3 ((𝜑𝑑 ∈ (1...(⌊‘𝐴))) → (((𝑋‘(𝐿𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚))) = Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((μ‘𝑑) · (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚))))))
140139sumeq2dv 15585 . 2 (𝜑 → Σ𝑑 ∈ (1...(⌊‘𝐴))(((𝑋‘(𝐿𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚))) = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((μ‘𝑑) · (((𝑋‘(𝐿‘(𝑑 · 𝑚))) / (𝑑 · 𝑚)) · (log‘(𝐴 / (𝑑 · 𝑚))))))
14137, 66, 1403eqtr4d 2786 1 (𝜑 → (log‘𝐴) = Σ𝑑 ∈ (1...(⌊‘𝐴))(((𝑋‘(𝐿𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wne 2942  {crab 3406  wss 3909   class class class wbr 5104  cfv 6494  (class class class)co 7354  cc 11046  cr 11047  0cc0 11048  1c1 11049   · cmul 11053  cle 11187   / cdiv 11809  cn 12150  cz 12496  cuz 12760  +crp 12912  ...cfz 13421  cfl 13692  Σcsu 15567  cdvds 16133  Basecbs 17080  0gc0g 17318  ℤRHomczrh 20896  ℤ/nczn 20899  logclog 25906  μcmu 26440  DChrcdchr 26576
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7669  ax-inf2 9574  ax-cnex 11104  ax-resscn 11105  ax-1cn 11106  ax-icn 11107  ax-addcl 11108  ax-addrcl 11109  ax-mulcl 11110  ax-mulrcl 11111  ax-mulcom 11112  ax-addass 11113  ax-mulass 11114  ax-distr 11115  ax-i2m1 11116  ax-1ne0 11117  ax-1rid 11118  ax-rnegex 11119  ax-rrecex 11120  ax-cnre 11121  ax-pre-lttri 11122  ax-pre-lttrn 11123  ax-pre-ltadd 11124  ax-pre-mulgt0 11125  ax-pre-sup 11126  ax-addf 11127  ax-mulf 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4865  df-int 4907  df-iun 4955  df-iin 4956  df-disj 5070  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5530  df-eprel 5536  df-po 5544  df-so 5545  df-fr 5587  df-se 5588  df-we 5589  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6252  df-ord 6319  df-on 6320  df-lim 6321  df-suc 6322  df-iota 6446  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-isom 6503  df-riota 7310  df-ov 7357  df-oprab 7358  df-mpo 7359  df-of 7614  df-om 7800  df-1st 7918  df-2nd 7919  df-supp 8090  df-tpos 8154  df-frecs 8209  df-wrecs 8240  df-recs 8314  df-rdg 8353  df-1o 8409  df-2o 8410  df-oadd 8413  df-er 8645  df-ec 8647  df-qs 8651  df-map 8764  df-pm 8765  df-ixp 8833  df-en 8881  df-dom 8882  df-sdom 8883  df-fin 8884  df-fsupp 9303  df-fi 9344  df-sup 9375  df-inf 9376  df-oi 9443  df-dju 9834  df-card 9872  df-pnf 11188  df-mnf 11189  df-xr 11190  df-ltxr 11191  df-le 11192  df-sub 11384  df-neg 11385  df-div 11810  df-nn 12151  df-2 12213  df-3 12214  df-4 12215  df-5 12216  df-6 12217  df-7 12218  df-8 12219  df-9 12220  df-n0 12411  df-xnn0 12483  df-z 12497  df-dec 12616  df-uz 12761  df-q 12871  df-rp 12913  df-xneg 13030  df-xadd 13031  df-xmul 13032  df-ioo 13265  df-ioc 13266  df-ico 13267  df-icc 13268  df-fz 13422  df-fzo 13565  df-fl 13694  df-mod 13772  df-seq 13904  df-exp 13965  df-fac 14171  df-bc 14200  df-hash 14228  df-shft 14949  df-cj 14981  df-re 14982  df-im 14983  df-sqrt 15117  df-abs 15118  df-limsup 15350  df-clim 15367  df-rlim 15368  df-sum 15568  df-ef 15947  df-sin 15949  df-cos 15950  df-pi 15952  df-dvds 16134  df-gcd 16372  df-prm 16545  df-pc 16706  df-struct 17016  df-sets 17033  df-slot 17051  df-ndx 17063  df-base 17081  df-ress 17110  df-plusg 17143  df-mulr 17144  df-starv 17145  df-sca 17146  df-vsca 17147  df-ip 17148  df-tset 17149  df-ple 17150  df-ds 17152  df-unif 17153  df-hom 17154  df-cco 17155  df-rest 17301  df-topn 17302  df-0g 17320  df-gsum 17321  df-topgen 17322  df-pt 17323  df-prds 17326  df-xrs 17381  df-qtop 17386  df-imas 17387  df-qus 17388  df-xps 17389  df-mre 17463  df-mrc 17464  df-acs 17466  df-mgm 18494  df-sgrp 18543  df-mnd 18554  df-mhm 18598  df-submnd 18599  df-grp 18748  df-minusg 18749  df-sbg 18750  df-mulg 18869  df-subg 18921  df-nsg 18922  df-eqg 18923  df-ghm 19002  df-cntz 19093  df-cmn 19560  df-abl 19561  df-mgp 19893  df-ur 19910  df-ring 19962  df-cring 19963  df-oppr 20045  df-dvdsr 20066  df-unit 20067  df-rnghom 20142  df-subrg 20216  df-lmod 20320  df-lss 20389  df-lsp 20429  df-sra 20629  df-rgmod 20630  df-lidl 20631  df-rsp 20632  df-2idl 20698  df-psmet 20784  df-xmet 20785  df-met 20786  df-bl 20787  df-mopn 20788  df-fbas 20789  df-fg 20790  df-cnfld 20793  df-zring 20866  df-zrh 20900  df-zn 20903  df-top 22239  df-topon 22256  df-topsp 22278  df-bases 22292  df-cld 22366  df-ntr 22367  df-cls 22368  df-nei 22445  df-lp 22483  df-perf 22484  df-cn 22574  df-cnp 22575  df-haus 22662  df-tx 22909  df-hmeo 23102  df-fil 23193  df-fm 23285  df-flim 23286  df-flf 23287  df-xms 23669  df-ms 23670  df-tms 23671  df-cncf 24237  df-limc 25226  df-dv 25227  df-log 25908  df-mu 26446  df-dchr 26577
This theorem is referenced by:  dchrvmasum2if  26841
  Copyright terms: Public domain W3C validator