Proof of Theorem dchrisum0lem2
Step | Hyp | Ref
| Expression |
1 | | 2cnd 11093 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈
ℂ) |
2 | | rpcn 11841 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
3 | 2 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
4 | | fzfid 12772 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘𝑥))
∈ Fin) |
5 | | rpvmasum2.g |
. . . . . . 7
⊢ 𝐺 = (DChr‘𝑁) |
6 | | rpvmasum.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
7 | | rpvmasum2.d |
. . . . . . 7
⊢ 𝐷 = (Base‘𝐺) |
8 | | rpvmasum.l |
. . . . . . 7
⊢ 𝐿 = (ℤRHom‘𝑍) |
9 | | rpvmasum2.w |
. . . . . . . . . . 11
⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} |
10 | | ssrab2 3687 |
. . . . . . . . . . 11
⊢ {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} ⊆ (𝐷 ∖ { 1 }) |
11 | 9, 10 | eqsstri 3635 |
. . . . . . . . . 10
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
12 | | dchrisum0.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
13 | 11, 12 | sseldi 3601 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ (𝐷 ∖ { 1 })) |
14 | 13 | eldifad 3586 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
15 | 14 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑋 ∈ 𝐷) |
16 | | elfzelz 12342 |
. . . . . . . 8
⊢ (𝑚 ∈
(1...(⌊‘𝑥))
→ 𝑚 ∈
ℤ) |
17 | 16 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑚 ∈
ℤ) |
18 | 5, 6, 7, 8, 15, 17 | dchrzrhcl 24970 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
19 | | elfznn 12370 |
. . . . . . . . 9
⊢ (𝑚 ∈
(1...(⌊‘𝑥))
→ 𝑚 ∈
ℕ) |
20 | 19 | nnrpd 11870 |
. . . . . . . 8
⊢ (𝑚 ∈
(1...(⌊‘𝑥))
→ 𝑚 ∈
ℝ+) |
21 | 20 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑚 ∈
ℝ+) |
22 | 21 | rpcnd 11874 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑚 ∈
ℂ) |
23 | 21 | rpne0d 11877 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑚 ≠
0) |
24 | 18, 22, 23 | divcld 10801 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((𝑋‘(𝐿‘𝑚)) / 𝑚) ∈ ℂ) |
25 | 4, 24 | fsumcl 14464 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚) ∈ ℂ) |
26 | 3, 25 | mulcld 10060 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 · Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)) ∈ ℂ) |
27 | | rpssre 11843 |
. . . . 5
⊢
ℝ+ ⊆ ℝ |
28 | | 2cn 11091 |
. . . . 5
⊢ 2 ∈
ℂ |
29 | | o1const 14350 |
. . . . 5
⊢
((ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ) →
(𝑥 ∈
ℝ+ ↦ 2) ∈ 𝑂(1)) |
30 | 27, 28, 29 | mp2an 708 |
. . . 4
⊢ (𝑥 ∈ ℝ+
↦ 2) ∈ 𝑂(1) |
31 | 30 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ 2) ∈
𝑂(1)) |
32 | 27 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ+
⊆ ℝ) |
33 | | 1red 10055 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ) |
34 | | dchrisum0lem2.e |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ (0[,)+∞)) |
35 | | elrege0 12278 |
. . . . . 6
⊢ (𝐸 ∈ (0[,)+∞) ↔
(𝐸 ∈ ℝ ∧ 0
≤ 𝐸)) |
36 | 35 | simplbi 476 |
. . . . 5
⊢ (𝐸 ∈ (0[,)+∞) →
𝐸 ∈
ℝ) |
37 | 34, 36 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ ℝ) |
38 | 3, 25 | absmuld 14193 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘(𝑥 ·
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚))) = ((abs‘𝑥) · (abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)))) |
39 | | rprege0 11847 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
40 | 39 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤
𝑥)) |
41 | | absid 14036 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) → (abs‘𝑥) = 𝑥) |
42 | 40, 41 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘𝑥) = 𝑥) |
43 | 42 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((abs‘𝑥) ·
(abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚))) = (𝑥 · (abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)))) |
44 | 38, 43 | eqtrd 2656 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘(𝑥 ·
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚))) = (𝑥 · (abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)))) |
45 | 44 | adantrr 753 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘(𝑥 ·
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚))) = (𝑥 · (abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)))) |
46 | 25 | adantrr 753 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚) ∈ ℂ) |
47 | 46 | subid1d 10381 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚) − 0) = Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)) |
48 | 19 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑚 ∈
ℕ) |
49 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑚 → (𝐿‘𝑎) = (𝐿‘𝑚)) |
50 | 49 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑚 → (𝑋‘(𝐿‘𝑎)) = (𝑋‘(𝐿‘𝑚))) |
51 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑚 → 𝑎 = 𝑚) |
52 | 50, 51 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑚 → ((𝑋‘(𝐿‘𝑎)) / 𝑎) = ((𝑋‘(𝐿‘𝑚)) / 𝑚)) |
53 | | dchrisum0lem2.k |
. . . . . . . . . . . . . 14
⊢ 𝐾 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) |
54 | | ovex 6678 |
. . . . . . . . . . . . . 14
⊢ ((𝑋‘(𝐿‘𝑎)) / 𝑎) ∈ V |
55 | 52, 53, 54 | fvmpt3i 6287 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ → (𝐾‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / 𝑚)) |
56 | 48, 55 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝐾‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / 𝑚)) |
57 | 56 | adantlrr 757 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝐾‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / 𝑚)) |
58 | | rpregt0 11846 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
59 | 58 | ad2antrl 764 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥 ∈ ℝ ∧ 0 <
𝑥)) |
60 | 59 | simpld 475 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ∈
ℝ) |
61 | | simprr 796 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 1 ≤ 𝑥) |
62 | | flge1nn 12622 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ) |
63 | 60, 61, 62 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(⌊‘𝑥) ∈
ℕ) |
64 | | nnuz 11723 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
65 | 63, 64 | syl6eleq 2711 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(⌊‘𝑥) ∈
(ℤ≥‘1)) |
66 | 24 | adantlrr 757 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((𝑋‘(𝐿‘𝑚)) / 𝑚) ∈ ℂ) |
67 | 57, 65, 66 | fsumser 14461 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚) = (seq1( + , 𝐾)‘(⌊‘𝑥))) |
68 | | rpvmasum.a |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℕ) |
69 | | rpvmasum2.1 |
. . . . . . . . . . . . . 14
⊢ 1 =
(0g‘𝐺) |
70 | | eldifsni 4320 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ (𝐷 ∖ { 1 }) → 𝑋 ≠ 1 ) |
71 | 13, 70 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ≠ 1 ) |
72 | | dchrisum0lem2.t |
. . . . . . . . . . . . . 14
⊢ (𝜑 → seq1( + , 𝐾) ⇝ 𝑇) |
73 | | dchrisum0lem2.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 / 𝑦)) |
74 | 6, 8, 68, 5, 7, 69, 14, 71, 53, 34, 72, 73, 9 | dchrvmaeq0 25193 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 ∈ 𝑊 ↔ 𝑇 = 0)) |
75 | 12, 74 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 = 0) |
76 | 75 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑇 = 0) |
77 | 76 | eqcomd 2628 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 0 = 𝑇) |
78 | 67, 77 | oveq12d 6668 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚) − 0) = ((seq1( + , 𝐾)‘(⌊‘𝑥)) − 𝑇)) |
79 | 47, 78 | eqtr3d 2658 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚) = ((seq1( + , 𝐾)‘(⌊‘𝑥)) − 𝑇)) |
80 | 79 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)) = (abs‘((seq1( + , 𝐾)‘(⌊‘𝑥)) − 𝑇))) |
81 | | 1re 10039 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
82 | | elicopnf 12269 |
. . . . . . . . . 10
⊢ (1 ∈
ℝ → (𝑥 ∈
(1[,)+∞) ↔ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥))) |
83 | 81, 82 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 1
≤ 𝑥)) |
84 | 60, 61, 83 | sylanbrc 698 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ∈
(1[,)+∞)) |
85 | 73 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → ∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 / 𝑦)) |
86 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → (⌊‘𝑦) = (⌊‘𝑥)) |
87 | 86 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (seq1( + , 𝐾)‘(⌊‘𝑦)) = (seq1( + , 𝐾)‘(⌊‘𝑥))) |
88 | 87 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → ((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇) = ((seq1( + , 𝐾)‘(⌊‘𝑥)) − 𝑇)) |
89 | 88 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) = (abs‘((seq1( + , 𝐾)‘(⌊‘𝑥)) − 𝑇))) |
90 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝐸 / 𝑦) = (𝐸 / 𝑥)) |
91 | 89, 90 | breq12d 4666 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 / 𝑦) ↔ (abs‘((seq1( + , 𝐾)‘(⌊‘𝑥)) − 𝑇)) ≤ (𝐸 / 𝑥))) |
92 | 91 | rspcv 3305 |
. . . . . . . 8
⊢ (𝑥 ∈ (1[,)+∞) →
(∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 / 𝑦) → (abs‘((seq1( + , 𝐾)‘(⌊‘𝑥)) − 𝑇)) ≤ (𝐸 / 𝑥))) |
93 | 84, 85, 92 | sylc 65 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘((seq1( + , 𝐾)‘(⌊‘𝑥)) − 𝑇)) ≤ (𝐸 / 𝑥)) |
94 | 80, 93 | eqbrtrd 4675 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)) ≤ (𝐸 / 𝑥)) |
95 | 46 | abscld 14175 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)) ∈ ℝ) |
96 | 37 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝐸 ∈
ℝ) |
97 | | lemuldiv2 10904 |
. . . . . . 7
⊢
(((abs‘Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)) ∈ ℝ ∧ 𝐸 ∈ ℝ ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → ((𝑥 · (abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚))) ≤ 𝐸 ↔ (abs‘Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)) ≤ (𝐸 / 𝑥))) |
98 | 95, 96, 59, 97 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → ((𝑥 ·
(abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚))) ≤ 𝐸 ↔ (abs‘Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)) ≤ (𝐸 / 𝑥))) |
99 | 94, 98 | mpbird 247 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥 ·
(abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚))) ≤ 𝐸) |
100 | 45, 99 | eqbrtrd 4675 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘(𝑥 ·
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚))) ≤ 𝐸) |
101 | 32, 26, 33, 37, 100 | elo1d 14267 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚))) ∈ 𝑂(1)) |
102 | 1, 26, 31, 101 | o1mul2 14355 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (2
· (𝑥 ·
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)))) ∈ 𝑂(1)) |
103 | | fzfid 12772 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (1...(⌊‘((𝑥↑2) / 𝑚))) ∈ Fin) |
104 | 21 | rpsqrtcld 14150 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑚)
∈ ℝ+) |
105 | 104 | rpcnd 11874 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑚)
∈ ℂ) |
106 | 104 | rpne0d 11877 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑚)
≠ 0) |
107 | 18, 105, 106 | divcld 10801 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
108 | 107 | adantr 481 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
∧ 𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
109 | | elfznn 12370 |
. . . . . . . . . 10
⊢ (𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚))) → 𝑑 ∈ ℕ) |
110 | 109 | adantl 482 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
∧ 𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑑 ∈ ℕ) |
111 | 110 | nnrpd 11870 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
∧ 𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑑 ∈ ℝ+) |
112 | 111 | rpsqrtcld 14150 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
∧ 𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘𝑑) ∈
ℝ+) |
113 | 112 | rpcnd 11874 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
∧ 𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘𝑑) ∈ ℂ) |
114 | 112 | rpne0d 11877 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
∧ 𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘𝑑) ≠ 0) |
115 | 108, 113,
114 | divcld 10801 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
∧ 𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ) |
116 | 103, 115 | fsumcl 14464 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ Σ𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ) |
117 | 4, 116 | fsumcl 14464 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ) |
118 | | mulcl 10020 |
. . . 4
⊢ ((2
∈ ℂ ∧ (𝑥
· Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)) ∈ ℂ) → (2 · (𝑥 · Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚))) ∈ ℂ) |
119 | 28, 26, 118 | sylancr 695 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2
· (𝑥 ·
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚))) ∈ ℂ) |
120 | | 2re 11090 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
121 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
122 | | 2z 11409 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
123 | | rpexpcl 12879 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝑥↑2) ∈
ℝ+) |
124 | 121, 122,
123 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑2) ∈
ℝ+) |
125 | | rpdivcl 11856 |
. . . . . . . . . . . . 13
⊢ (((𝑥↑2) ∈
ℝ+ ∧ 𝑚
∈ ℝ+) → ((𝑥↑2) / 𝑚) ∈
ℝ+) |
126 | 124, 20, 125 | syl2an 494 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((𝑥↑2) / 𝑚) ∈
ℝ+) |
127 | 126 | rpsqrtcld 14150 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘((𝑥↑2) / 𝑚)) ∈
ℝ+) |
128 | 127 | rpred 11872 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘((𝑥↑2) / 𝑚)) ∈ ℝ) |
129 | | remulcl 10021 |
. . . . . . . . . 10
⊢ ((2
∈ ℝ ∧ (√‘((𝑥↑2) / 𝑚)) ∈ ℝ) → (2 ·
(√‘((𝑥↑2)
/ 𝑚))) ∈
ℝ) |
130 | 120, 128,
129 | sylancr 695 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (2 · (√‘((𝑥↑2) / 𝑚))) ∈ ℝ) |
131 | 130 | recnd 10068 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (2 · (√‘((𝑥↑2) / 𝑚))) ∈ ℂ) |
132 | 107, 131 | mulcld 10060 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (2 ·
(√‘((𝑥↑2)
/ 𝑚)))) ∈
ℂ) |
133 | 4, 116, 132 | fsumsub 14520 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) − (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (2 ·
(√‘((𝑥↑2)
/ 𝑚))))) = (Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) − Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (2 ·
(√‘((𝑥↑2)
/ 𝑚)))))) |
134 | 112 | rpcnne0d 11881 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
∧ 𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))) → ((√‘𝑑) ∈ ℂ ∧
(√‘𝑑) ≠
0)) |
135 | | reccl 10692 |
. . . . . . . . . . 11
⊢
(((√‘𝑑)
∈ ℂ ∧ (√‘𝑑) ≠ 0) → (1 / (√‘𝑑)) ∈
ℂ) |
136 | 134, 135 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
∧ 𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))) → (1 / (√‘𝑑)) ∈
ℂ) |
137 | 103, 136 | fsumcl 14464 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ Σ𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))(1 / (√‘𝑑)) ∈ ℂ) |
138 | 107, 137,
131 | subdid 10486 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(1 / (√‘𝑑)) − (2 · (√‘((𝑥↑2) / 𝑚))))) = ((((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(1 / (√‘𝑑))) − (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (2 ·
(√‘((𝑥↑2)
/ 𝑚)))))) |
139 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ((𝑥↑2) / 𝑚) → (⌊‘𝑦) = (⌊‘((𝑥↑2) / 𝑚))) |
140 | 139 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ((𝑥↑2) / 𝑚) → (1...(⌊‘𝑦)) = (1...(⌊‘((𝑥↑2) / 𝑚)))) |
141 | 140 | sumeq1d 14431 |
. . . . . . . . . . . 12
⊢ (𝑦 = ((𝑥↑2) / 𝑚) → Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) = Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(1 / (√‘𝑑))) |
142 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ((𝑥↑2) / 𝑚) → (√‘𝑦) = (√‘((𝑥↑2) / 𝑚))) |
143 | 142 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑦 = ((𝑥↑2) / 𝑚) → (2 · (√‘𝑦)) = (2 ·
(√‘((𝑥↑2)
/ 𝑚)))) |
144 | 141, 143 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑦 = ((𝑥↑2) / 𝑚) → (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 ·
(√‘𝑦))) =
(Σ𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))(1 / (√‘𝑑)) − (2 · (√‘((𝑥↑2) / 𝑚))))) |
145 | | dchrisum0lem2.h |
. . . . . . . . . . 11
⊢ 𝐻 = (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) |
146 | | ovex 6678 |
. . . . . . . . . . 11
⊢
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦))) ∈ V |
147 | 144, 145,
146 | fvmpt3i 6287 |
. . . . . . . . . 10
⊢ (((𝑥↑2) / 𝑚) ∈ ℝ+ → (𝐻‘((𝑥↑2) / 𝑚)) = (Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(1 / (√‘𝑑)) − (2 · (√‘((𝑥↑2) / 𝑚))))) |
148 | 126, 147 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝐻‘((𝑥↑2) / 𝑚)) = (Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(1 / (√‘𝑑)) − (2 · (√‘((𝑥↑2) / 𝑚))))) |
149 | 148 | oveq2d 6666 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) = (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(1 / (√‘𝑑)) − (2 · (√‘((𝑥↑2) / 𝑚)))))) |
150 | 108, 113,
114 | divrecd 10804 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
∧ 𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (1 / (√‘𝑑)))) |
151 | 150 | sumeq2dv 14433 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ Σ𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (1 / (√‘𝑑)))) |
152 | 103, 107,
136 | fsummulc2 14516 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(1 / (√‘𝑑))) = Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (1 / (√‘𝑑)))) |
153 | 151, 152 | eqtr4d 2659 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ Σ𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(1 / (√‘𝑑)))) |
154 | 153 | oveq1d 6665 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) − (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (2 ·
(√‘((𝑥↑2)
/ 𝑚))))) = ((((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(1 / (√‘𝑑))) − (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (2 ·
(√‘((𝑥↑2)
/ 𝑚)))))) |
155 | 138, 149,
154 | 3eqtr4d 2666 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) = (Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) − (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (2 ·
(√‘((𝑥↑2)
/ 𝑚)))))) |
156 | 155 | sumeq2dv 14433 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) = Σ𝑚 ∈ (1...(⌊‘𝑥))(Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) − (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (2 ·
(√‘((𝑥↑2)
/ 𝑚)))))) |
157 | | mulcl 10020 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ) → (2 · 𝑥) ∈ ℂ) |
158 | 28, 3, 157 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2
· 𝑥) ∈
ℂ) |
159 | 4, 158, 24 | fsummulc2 14516 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2
· 𝑥) ·
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘𝑥))((2 · 𝑥) · ((𝑋‘(𝐿‘𝑚)) / 𝑚))) |
160 | 1, 3, 25 | mulassd 10063 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2
· 𝑥) ·
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)) = (2 · (𝑥 · Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)))) |
161 | 158 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (2 · 𝑥)
∈ ℂ) |
162 | 161, 107,
105, 106 | div12d 10837 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((2 · 𝑥)
· (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑚))) = (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((2 · 𝑥) / (√‘𝑚)))) |
163 | 104 | rpcnne0d 11881 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑚)
∈ ℂ ∧ (√‘𝑚) ≠ 0)) |
164 | | divdiv1 10736 |
. . . . . . . . . . . . 13
⊢ (((𝑋‘(𝐿‘𝑚)) ∈ ℂ ∧ ((√‘𝑚) ∈ ℂ ∧
(√‘𝑚) ≠ 0)
∧ ((√‘𝑚)
∈ ℂ ∧ (√‘𝑚) ≠ 0)) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑚)) = ((𝑋‘(𝐿‘𝑚)) / ((√‘𝑚) · (√‘𝑚)))) |
165 | 18, 163, 163, 164 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑚)) = ((𝑋‘(𝐿‘𝑚)) / ((√‘𝑚) · (√‘𝑚)))) |
166 | 21 | rprege0d 11879 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝑚 ∈ ℝ
∧ 0 ≤ 𝑚)) |
167 | | remsqsqrt 13997 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℝ ∧ 0 ≤
𝑚) →
((√‘𝑚) ·
(√‘𝑚)) = 𝑚) |
168 | 166, 167 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑚)
· (√‘𝑚))
= 𝑚) |
169 | 168 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((𝑋‘(𝐿‘𝑚)) / ((√‘𝑚) · (√‘𝑚))) = ((𝑋‘(𝐿‘𝑚)) / 𝑚)) |
170 | 165, 169 | eqtr2d 2657 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((𝑋‘(𝐿‘𝑚)) / 𝑚) = (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑚))) |
171 | 170 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((2 · 𝑥)
· ((𝑋‘(𝐿‘𝑚)) / 𝑚)) = ((2 · 𝑥) · (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑚)))) |
172 | 124 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝑥↑2) ∈
ℝ+) |
173 | 172 | rprege0d 11879 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((𝑥↑2) ∈
ℝ ∧ 0 ≤ (𝑥↑2))) |
174 | | sqrtdiv 14006 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥↑2) ∈ ℝ ∧ 0
≤ (𝑥↑2)) ∧
𝑚 ∈
ℝ+) → (√‘((𝑥↑2) / 𝑚)) = ((√‘(𝑥↑2)) / (√‘𝑚))) |
175 | 173, 21, 174 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘((𝑥↑2) / 𝑚)) = ((√‘(𝑥↑2)) / (√‘𝑚))) |
176 | 39 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
177 | | sqrtsq 14010 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(√‘(𝑥↑2))
= 𝑥) |
178 | 176, 177 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘(𝑥↑2)) = 𝑥) |
179 | 178 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((√‘(𝑥↑2)) / (√‘𝑚)) = (𝑥 / (√‘𝑚))) |
180 | 175, 179 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘((𝑥↑2) / 𝑚)) = (𝑥 / (√‘𝑚))) |
181 | 180 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (2 · (√‘((𝑥↑2) / 𝑚))) = (2 · (𝑥 / (√‘𝑚)))) |
182 | | 2cnd 11093 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 2 ∈ ℂ) |
183 | 3 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℂ) |
184 | | divass 10703 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ ∧ ((√‘𝑚) ∈ ℂ ∧ (√‘𝑚) ≠ 0)) → ((2 ·
𝑥) / (√‘𝑚)) = (2 · (𝑥 / (√‘𝑚)))) |
185 | 182, 183,
163, 184 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((2 · 𝑥) /
(√‘𝑚)) = (2
· (𝑥 /
(√‘𝑚)))) |
186 | 181, 185 | eqtr4d 2659 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (2 · (√‘((𝑥↑2) / 𝑚))) = ((2 · 𝑥) / (√‘𝑚))) |
187 | 186 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (2 ·
(√‘((𝑥↑2)
/ 𝑚)))) = (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((2 · 𝑥) / (√‘𝑚)))) |
188 | 162, 171,
187 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((2 · 𝑥)
· ((𝑋‘(𝐿‘𝑚)) / 𝑚)) = (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (2 ·
(√‘((𝑥↑2)
/ 𝑚))))) |
189 | 188 | sumeq2dv 14433 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))((2
· 𝑥) ·
((𝑋‘(𝐿‘𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (2 ·
(√‘((𝑥↑2)
/ 𝑚))))) |
190 | 159, 160,
189 | 3eqtr3d 2664 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2
· (𝑥 ·
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚))) = Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (2 ·
(√‘((𝑥↑2)
/ 𝑚))))) |
191 | 190 | oveq2d 6666 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) − (2 · (𝑥 · Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)))) = (Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) − Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (2 ·
(√‘((𝑥↑2)
/ 𝑚)))))) |
192 | 133, 156,
191 | 3eqtr4d 2666 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) = (Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) − (2 · (𝑥 · Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚))))) |
193 | 192 | mpteq2dva 4744 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) − (2 · (𝑥 · Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)))))) |
194 | | dchrisum0lem1.f |
. . . . 5
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) |
195 | | dchrisum0.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) |
196 | | dchrisum0.s |
. . . . 5
⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) |
197 | | dchrisum0.1 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) |
198 | | dchrisum0lem2.u |
. . . . 5
⊢ (𝜑 → 𝐻 ⇝𝑟 𝑈) |
199 | 6, 8, 68, 5, 7, 69, 9, 12, 194, 195, 196, 197, 145, 198 | dchrisum0lem2a 25206 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚)))) ∈ 𝑂(1)) |
200 | 193, 199 | eqeltrrd 2702 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) − (2 · (𝑥 · Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚))))) ∈ 𝑂(1)) |
201 | 117, 119,
200 | o1dif 14360 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1) ↔ (𝑥 ∈ ℝ+
↦ (2 · (𝑥
· Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / 𝑚)))) ∈ 𝑂(1))) |
202 | 102, 201 | mpbird 247 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1)) |