Metamath Proof Explorer

Theorem mulog2sumlem3

Description: Lemma for mulog2sum . (Contributed by Mario Carneiro, 13-May-2016)

Ref Expression
Hypotheses logdivsum.1 ⊢F=y∈ℝ+⟼∑i=1ylog⁡ii−log⁡y22
mulog2sumlem.1 ⊢φ→F⇝ℝL
Assertion mulog2sumlem3 ⊢φ→x∈ℝ+⟼∑n=1xμ⁡nn⁢log⁡xn2−2⁢log⁡x∈𝑂⁡1

Proof

Step Hyp Ref Expression
1 logdivsum.1 ⊢F=y∈ℝ+⟼∑i=1ylog⁡ii−log⁡y22
2 mulog2sumlem.1 ⊢φ→F⇝ℝL
3 2cn ⊢2∈ℂ
4 3 a1i ⊢φ∧x∈ℝ+→2∈ℂ
5 fzfid ⊢φ∧x∈ℝ+→1…x∈Fin
6 elfznn ⊢n∈1…x→n∈ℕ
7 6 adantl ⊢φ∧x∈ℝ+∧n∈1…x→n∈ℕ
8 mucl ⊢n∈ℕ→μ⁡n∈ℤ
9 7 8 syl ⊢φ∧x∈ℝ+∧n∈1…x→μ⁡n∈ℤ
10 9 zred ⊢φ∧x∈ℝ+∧n∈1…x→μ⁡n∈ℝ
11 10 7 nndivred ⊢φ∧x∈ℝ+∧n∈1…x→μ⁡nn∈ℝ
12 11 recnd ⊢φ∧x∈ℝ+∧n∈1…x→μ⁡nn∈ℂ
13 simpr ⊢φ∧x∈ℝ+→x∈ℝ+
14 6 nnrpd ⊢n∈1…x→n∈ℝ+
15 rpdivcl ⊢x∈ℝ+∧n∈ℝ+→xn∈ℝ+
16 13 14 15 syl2an ⊢φ∧x∈ℝ+∧n∈1…x→xn∈ℝ+
17 16 relogcld ⊢φ∧x∈ℝ+∧n∈1…x→log⁡xn∈ℝ
18 17 recnd ⊢φ∧x∈ℝ+∧n∈1…x→log⁡xn∈ℂ
19 18 sqcld ⊢φ∧x∈ℝ+∧n∈1…x→log⁡xn2∈ℂ
20 19 halfcld ⊢φ∧x∈ℝ+∧n∈1…x→log⁡xn22∈ℂ
21 12 20 mulcld ⊢φ∧x∈ℝ+∧n∈1…x→μ⁡nn⁢log⁡xn22∈ℂ
22 5 21 fsumcl ⊢φ∧x∈ℝ+→∑n=1xμ⁡nn⁢log⁡xn22∈ℂ
23 relogcl ⊢x∈ℝ+→log⁡x∈ℝ
24 23 adantl ⊢φ∧x∈ℝ+→log⁡x∈ℝ
25 24 recnd ⊢φ∧x∈ℝ+→log⁡x∈ℂ
26 4 22 25 subdid ⊢φ∧x∈ℝ+→2⁢∑n=1xμ⁡nn⁢log⁡xn22−log⁡x=2⁢∑n=1xμ⁡nn⁢log⁡xn22−2⁢log⁡x
27 5 4 21 fsummulc2 ⊢φ∧x∈ℝ+→2⁢∑n=1xμ⁡nn⁢log⁡xn22=∑n=1x2⁢μ⁡nn⁢log⁡xn22
28 3 a1i ⊢φ∧x∈ℝ+∧n∈1…x→2∈ℂ
29 28 12 20 mul12d ⊢φ∧x∈ℝ+∧n∈1…x→2⁢μ⁡nn⁢log⁡xn22=μ⁡nn⁢2⁢log⁡xn22
30 2ne0 ⊢2≠0
31 30 a1i ⊢φ∧x∈ℝ+∧n∈1…x→2≠0
32 19 28 31 divcan2d ⊢φ∧x∈ℝ+∧n∈1…x→2⁢log⁡xn22=log⁡xn2
33 32 oveq2d ⊢φ∧x∈ℝ+∧n∈1…x→μ⁡nn⁢2⁢log⁡xn22=μ⁡nn⁢log⁡xn2
34 29 33 eqtrd ⊢φ∧x∈ℝ+∧n∈1…x→2⁢μ⁡nn⁢log⁡xn22=μ⁡nn⁢log⁡xn2
35 34 sumeq2dv ⊢φ∧x∈ℝ+→∑n=1x2⁢μ⁡nn⁢log⁡xn22=∑n=1xμ⁡nn⁢log⁡xn2
36 27 35 eqtrd ⊢φ∧x∈ℝ+→2⁢∑n=1xμ⁡nn⁢log⁡xn22=∑n=1xμ⁡nn⁢log⁡xn2
37 36 oveq1d ⊢φ∧x∈ℝ+→2⁢∑n=1xμ⁡nn⁢log⁡xn22−2⁢log⁡x=∑n=1xμ⁡nn⁢log⁡xn2−2⁢log⁡x
38 26 37 eqtrd ⊢φ∧x∈ℝ+→2⁢∑n=1xμ⁡nn⁢log⁡xn22−log⁡x=∑n=1xμ⁡nn⁢log⁡xn2−2⁢log⁡x
39 38 mpteq2dva ⊢φ→x∈ℝ+⟼2⁢∑n=1xμ⁡nn⁢log⁡xn22−log⁡x=x∈ℝ+⟼∑n=1xμ⁡nn⁢log⁡xn2−2⁢log⁡x
40 22 25 subcld ⊢φ∧x∈ℝ+→∑n=1xμ⁡nn⁢log⁡xn22−log⁡x∈ℂ
41 rpssre ⊢ℝ+⊆ℝ
42 o1const ⊢ℝ+⊆ℝ∧2∈ℂ→x∈ℝ+⟼2∈𝑂⁡1
43 41 3 42 mp2an ⊢x∈ℝ+⟼2∈𝑂⁡1
44 43 a1i ⊢φ→x∈ℝ+⟼2∈𝑂⁡1
45 emre ⊢γ∈ℝ
46 45 recni ⊢γ∈ℂ
47 mulcl ⊢γ∈ℂ∧log⁡xn∈ℂ→γ⁢log⁡xn∈ℂ
48 46 18 47 sylancr ⊢φ∧x∈ℝ+∧n∈1…x→γ⁢log⁡xn∈ℂ
49 rlimcl ⊢F⇝ℝL→L∈ℂ
50 2 49 syl ⊢φ→L∈ℂ
51 50 ad2antrr ⊢φ∧x∈ℝ+∧n∈1…x→L∈ℂ
52 48 51 subcld ⊢φ∧x∈ℝ+∧n∈1…x→γ⁢log⁡xn−L∈ℂ
53 20 52 addcld ⊢φ∧x∈ℝ+∧n∈1…x→log⁡xn22+γ⁢log⁡xn-L∈ℂ
54 12 53 mulcld ⊢φ∧x∈ℝ+∧n∈1…x→μ⁡nn⁢log⁡xn22+γ⁢log⁡xn-L∈ℂ
55 5 54 fsumcl ⊢φ∧x∈ℝ+→∑n=1xμ⁡nn⁢log⁡xn22+γ⁢log⁡xn-L∈ℂ
56 12 52 mulcld ⊢φ∧x∈ℝ+∧n∈1…x→μ⁡nn⁢γ⁢log⁡xn−L∈ℂ
57 5 56 fsumcl ⊢φ∧x∈ℝ+→∑n=1xμ⁡nn⁢γ⁢log⁡xn−L∈ℂ
58 55 25 57 sub32d ⊢φ∧x∈ℝ+→∑n=1xμ⁡nn⁢log⁡xn22+γ⁢log⁡xn-L-log⁡x-∑n=1xμ⁡nn⁢γ⁢log⁡xn−L=∑n=1xμ⁡nn⁢log⁡xn22+γ⁢log⁡xn-L-∑n=1xμ⁡nn⁢γ⁢log⁡xn−L-log⁡x
59 5 54 56 fsumsub ⊢φ∧x∈ℝ+→∑n=1xμ⁡nn⁢log⁡xn22+γ⁢log⁡xn-L−μ⁡nn⁢γ⁢log⁡xn−L=∑n=1xμ⁡nn⁢log⁡xn22+γ⁢log⁡xn-L−∑n=1xμ⁡nn⁢γ⁢log⁡xn−L
60 12 53 52 subdid ⊢φ∧x∈ℝ+∧n∈1…x→μ⁡nn⁢log⁡xn22+γ⁢log⁡xn−L-γ⁢log⁡xn−L=μ⁡nn⁢log⁡xn22+γ⁢log⁡xn-L−μ⁡nn⁢γ⁢log⁡xn−L
61 20 52 pncand ⊢φ∧x∈ℝ+∧n∈1…x→log⁡xn22+γ⁢log⁡xn−L-γ⁢log⁡xn−L=log⁡xn22
62 61 oveq2d ⊢φ∧x∈ℝ+∧n∈1…x→μ⁡nn⁢log⁡xn22+γ⁢log⁡xn−L-γ⁢log⁡xn−L=μ⁡nn⁢log⁡xn22
63 60 62 eqtr3d ⊢φ∧x∈ℝ+∧n∈1…x→μ⁡nn⁢log⁡xn22+γ⁢log⁡xn-L−μ⁡nn⁢γ⁢log⁡xn−L=μ⁡nn⁢log⁡xn22
64 63 sumeq2dv ⊢φ∧x∈ℝ+→∑n=1xμ⁡nn⁢log⁡xn22+γ⁢log⁡xn-L−μ⁡nn⁢γ⁢log⁡xn−L=∑n=1xμ⁡nn⁢log⁡xn22
65 59 64 eqtr3d ⊢φ∧x∈ℝ+→∑n=1xμ⁡nn⁢log⁡xn22+γ⁢log⁡xn-L−∑n=1xμ⁡nn⁢γ⁢log⁡xn−L=∑n=1xμ⁡nn⁢log⁡xn22
66 65 oveq1d ⊢φ∧x∈ℝ+→∑n=1xμ⁡nn⁢log⁡xn22+γ⁢log⁡xn-L-∑n=1xμ⁡nn⁢γ⁢log⁡xn−L-log⁡x=∑n=1xμ⁡nn⁢log⁡xn22−log⁡x
67 58 66 eqtrd ⊢φ∧x∈ℝ+→∑n=1xμ⁡nn⁢log⁡xn22+γ⁢log⁡xn-L-log⁡x-∑n=1xμ⁡nn⁢γ⁢log⁡xn−L=∑n=1xμ⁡nn⁢log⁡xn22−log⁡x
68 67 mpteq2dva ⊢φ→x∈ℝ+⟼∑n=1xμ⁡nn⁢log⁡xn22+γ⁢log⁡xn-L-log⁡x-∑n=1xμ⁡nn⁢γ⁢log⁡xn−L=x∈ℝ+⟼∑n=1xμ⁡nn⁢log⁡xn22−log⁡x
69 55 25 subcld ⊢φ∧x∈ℝ+→∑n=1xμ⁡nn⁢log⁡xn22+γ⁢log⁡xn-L−log⁡x∈ℂ
70 eqid ⊢log⁡xn22+γ⁢log⁡xn-L=log⁡xn22+γ⁢log⁡xn-L
71 eqid ⊢12+γ+L+∑m=12log⁡emm=12+γ+L+∑m=12log⁡emm
72 1 2 70 71 mulog2sumlem2 ⊢φ→x∈ℝ+⟼∑n=1xμ⁡nn⁢log⁡xn22+γ⁢log⁡xn-L−log⁡x∈𝑂⁡1
73 46 a1i ⊢φ∧x∈ℝ+→γ∈ℂ
74 12 18 mulcld ⊢φ∧x∈ℝ+∧n∈1…x→μ⁡nn⁢log⁡xn∈ℂ
75 5 73 74 fsummulc2 ⊢φ∧x∈ℝ+→γ⁢∑n=1xμ⁡nn⁢log⁡xn=∑n=1xγ⁢μ⁡nn⁢log⁡xn
76 50 adantr ⊢φ∧x∈ℝ+→L∈ℂ
77 5 76 12 fsummulc1 ⊢φ∧x∈ℝ+→∑n=1xμ⁡nn⁢L=∑n=1xμ⁡nn⁢L
78 75 77 oveq12d ⊢φ∧x∈ℝ+→γ⁢∑n=1xμ⁡nn⁢log⁡xn−∑n=1xμ⁡nn⁢L=∑n=1xγ⁢μ⁡nn⁢log⁡xn−∑n=1xμ⁡nn⁢L
79 mulcl ⊢γ∈ℂ∧μ⁡nn⁢log⁡xn∈ℂ→γ⁢μ⁡nn⁢log⁡xn∈ℂ
80 46 74 79 sylancr ⊢φ∧x∈ℝ+∧n∈1…x→γ⁢μ⁡nn⁢log⁡xn∈ℂ
81 12 51 mulcld ⊢φ∧x∈ℝ+∧n∈1…x→μ⁡nn⁢L∈ℂ
82 5 80 81 fsumsub ⊢φ∧x∈ℝ+→∑n=1xγ⁢μ⁡nn⁢log⁡xn−μ⁡nn⁢L=∑n=1xγ⁢μ⁡nn⁢log⁡xn−∑n=1xμ⁡nn⁢L
83 46 a1i ⊢φ∧x∈ℝ+∧n∈1…x→γ∈ℂ
84 83 12 18 mul12d ⊢φ∧x∈ℝ+∧n∈1…x→γ⁢μ⁡nn⁢log⁡xn=μ⁡nn⁢γ⁢log⁡xn
85 84 oveq1d ⊢φ∧x∈ℝ+∧n∈1…x→γ⁢μ⁡nn⁢log⁡xn−μ⁡nn⁢L=μ⁡nn⁢γ⁢log⁡xn−μ⁡nn⁢L
86 12 48 51 subdid ⊢φ∧x∈ℝ+∧n∈1…x→μ⁡nn⁢γ⁢log⁡xn−L=μ⁡nn⁢γ⁢log⁡xn−μ⁡nn⁢L
87 85 86 eqtr4d ⊢φ∧x∈ℝ+∧n∈1…x→γ⁢μ⁡nn⁢log⁡xn−μ⁡nn⁢L=μ⁡nn⁢γ⁢log⁡xn−L
88 87 sumeq2dv ⊢φ∧x∈ℝ+→∑n=1xγ⁢μ⁡nn⁢log⁡xn−μ⁡nn⁢L=∑n=1xμ⁡nn⁢γ⁢log⁡xn−L
89 78 82 88 3eqtr2d ⊢φ∧x∈ℝ+→γ⁢∑n=1xμ⁡nn⁢log⁡xn−∑n=1xμ⁡nn⁢L=∑n=1xμ⁡nn⁢γ⁢log⁡xn−L
90 89 mpteq2dva ⊢φ→x∈ℝ+⟼γ⁢∑n=1xμ⁡nn⁢log⁡xn−∑n=1xμ⁡nn⁢L=x∈ℝ+⟼∑n=1xμ⁡nn⁢γ⁢log⁡xn−L
91 5 74 fsumcl ⊢φ∧x∈ℝ+→∑n=1xμ⁡nn⁢log⁡xn∈ℂ
92 mulcl ⊢γ∈ℂ∧∑n=1xμ⁡nn⁢log⁡xn∈ℂ→γ⁢∑n=1xμ⁡nn⁢log⁡xn∈ℂ
93 46 91 92 sylancr ⊢φ∧x∈ℝ+→γ⁢∑n=1xμ⁡nn⁢log⁡xn∈ℂ
94 5 12 fsumcl ⊢φ∧x∈ℝ+→∑n=1xμ⁡nn∈ℂ
95 94 76 mulcld ⊢φ∧x∈ℝ+→∑n=1xμ⁡nn⁢L∈ℂ
96 46 a1i ⊢φ→γ∈ℂ
97 o1const ⊢ℝ+⊆ℝ∧γ∈ℂ→x∈ℝ+⟼γ∈𝑂⁡1
98 41 96 97 sylancr ⊢φ→x∈ℝ+⟼γ∈𝑂⁡1
99 mulogsum ⊢x∈ℝ+⟼∑n=1xμ⁡nn⁢log⁡xn∈𝑂⁡1
100 99 a1i ⊢φ→x∈ℝ+⟼∑n=1xμ⁡nn⁢log⁡xn∈𝑂⁡1
101 73 91 98 100 o1mul2 ⊢φ→x∈ℝ+⟼γ⁢∑n=1xμ⁡nn⁢log⁡xn∈𝑂⁡1
102 mudivsum ⊢x∈ℝ+⟼∑n=1xμ⁡nn∈𝑂⁡1
103 102 a1i ⊢φ→x∈ℝ+⟼∑n=1xμ⁡nn∈𝑂⁡1
104 o1const ⊢ℝ+⊆ℝ∧L∈ℂ→x∈ℝ+⟼L∈𝑂⁡1
105 41 50 104 sylancr ⊢φ→x∈ℝ+⟼L∈𝑂⁡1
106 94 76 103 105 o1mul2 ⊢φ→x∈ℝ+⟼∑n=1xμ⁡nn⁢L∈𝑂⁡1
107 93 95 101 106 o1sub2 ⊢φ→x∈ℝ+⟼γ⁢∑n=1xμ⁡nn⁢log⁡xn−∑n=1xμ⁡nn⁢L∈𝑂⁡1
108 90 107 eqeltrrd ⊢φ→x∈ℝ+⟼∑n=1xμ⁡nn⁢γ⁢log⁡xn−L∈𝑂⁡1
109 69 57 72 108 o1sub2 ⊢φ→x∈ℝ+⟼∑n=1xμ⁡nn⁢log⁡xn22+γ⁢log⁡xn-L-log⁡x-∑n=1xμ⁡nn⁢γ⁢log⁡xn−L∈𝑂⁡1
110 68 109 eqeltrrd ⊢φ→x∈ℝ+⟼∑n=1xμ⁡nn⁢log⁡xn22−log⁡x∈𝑂⁡1
111 4 40 44 110 o1mul2 ⊢φ→x∈ℝ+⟼2⁢∑n=1xμ⁡nn⁢log⁡xn22−log⁡x∈𝑂⁡1
112 39 111 eqeltrrd ⊢φ→x∈ℝ+⟼∑n=1xμ⁡nn⁢log⁡xn2−2⁢log⁡x∈𝑂⁡1