Step | Hyp | Ref
| Expression |
1 | | 1red 9934 |
. 2
⊢ (𝜑 → 1 ∈
ℝ) |
2 | | sumex 14266 |
. . . 4
⊢
Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ V |
3 | 2 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ V) |
4 | | sumex 14266 |
. . . 4
⊢
Σ𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ V |
5 | 4 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ V) |
6 | | rpvmasum.z |
. . . . 5
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
7 | | rpvmasum.l |
. . . . 5
⊢ 𝐿 = (ℤRHom‘𝑍) |
8 | | rpvmasum.a |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
9 | | rpvmasum2.g |
. . . . 5
⊢ 𝐺 = (DChr‘𝑁) |
10 | | rpvmasum2.d |
. . . . 5
⊢ 𝐷 = (Base‘𝐺) |
11 | | rpvmasum2.1 |
. . . . 5
⊢ 1 =
(0g‘𝐺) |
12 | | rpvmasum2.w |
. . . . . . . 8
⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} |
13 | | ssrab2 3650 |
. . . . . . . 8
⊢ {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} ⊆ (𝐷 ∖ { 1 }) |
14 | 12, 13 | eqsstri 3598 |
. . . . . . 7
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
15 | | difss 3699 |
. . . . . . 7
⊢ (𝐷 ∖ { 1 }) ⊆ 𝐷 |
16 | 14, 15 | sstri 3577 |
. . . . . 6
⊢ 𝑊 ⊆ 𝐷 |
17 | | dchrisum0.b |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
18 | 16, 17 | sseldi 3566 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
19 | 14, 17 | sseldi 3566 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝐷 ∖ { 1 })) |
20 | | eldifsni 4261 |
. . . . . 6
⊢ (𝑋 ∈ (𝐷 ∖ { 1 }) → 𝑋 ≠ 1 ) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋 ≠ 1 ) |
22 | | eqid 2610 |
. . . . 5
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) |
23 | 6, 7, 8, 9, 10, 11, 18, 21, 22 | dchrmusumlema 24982 |
. . . 4
⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦))) |
24 | 8 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑁 ∈ ℕ) |
25 | 17 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑋 ∈ 𝑊) |
26 | | dchrisum0lem1.f |
. . . . . . 7
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) |
27 | | dchrisum0.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) |
28 | 27 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝐶 ∈ (0[,)+∞)) |
29 | | dchrisum0.s |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) |
30 | 29 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , 𝐹) ⇝ 𝑆) |
31 | | dchrisum0.1 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) |
32 | 31 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) |
33 | | eqid 2610 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) = (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) |
34 | 33 | divsqrsum 24508 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) ∈ dom
⇝𝑟 |
35 | 33 | divsqrsumf 24507 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))):ℝ+⟶ℝ |
36 | | ax-resscn 9872 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
37 | | fss 5969 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))):ℝ+⟶ℝ ∧
ℝ ⊆ ℂ) → (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))):ℝ+⟶ℂ) |
38 | 35, 36, 37 | mp2an 704 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))):ℝ+⟶ℂ |
39 | 38 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))):ℝ+⟶ℂ) |
40 | | rpsup 12527 |
. . . . . . . . . . 11
⊢
sup(ℝ+, ℝ*, < ) =
+∞ |
41 | 40 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → sup(ℝ+,
ℝ*, < ) = +∞) |
42 | 39, 41 | rlimdm 14130 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) ∈ dom ⇝𝑟
↔ (𝑦 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 ·
(√‘𝑦))))
⇝𝑟 ( ⇝𝑟 ‘(𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦))))))) |
43 | 34, 42 | mpbii 222 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) ⇝𝑟 (
⇝𝑟 ‘(𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))))) |
44 | 43 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) ⇝𝑟 (
⇝𝑟 ‘(𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))))) |
45 | | simprl 790 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑐 ∈ (0[,)+∞)) |
46 | | simprrl 800 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡) |
47 | | simprrr 801 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) |
48 | 6, 7, 24, 9, 10, 11, 12, 25, 26, 28, 30, 32, 33, 44, 22, 45, 46, 47 | dchrisum0lem2 25007 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1)) |
49 | 48 | rexlimdvaa 3014 |
. . . . 5
⊢ (𝜑 → (∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1))) |
50 | 49 | exlimdv 1848 |
. . . 4
⊢ (𝜑 → (∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1))) |
51 | 23, 50 | mpd 15 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1)) |
52 | 6, 7, 8, 9, 10, 11, 12, 17, 26, 27, 29, 31 | dchrisum0lem1 25005 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1)) |
53 | 3, 5, 51, 52 | o1add2 14202 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))) ∈ 𝑂(1)) |
54 | | ovex 6577 |
. . 3
⊢
(Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ V |
55 | 54 | a1i 11 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ V) |
56 | | fzfid 12634 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘(𝑥↑2))) ∈ Fin) |
57 | | fzfid 12634 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) →
(1...(⌊‘((𝑥↑2) / 𝑚))) ∈ Fin) |
58 | 18 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → 𝑋 ∈ 𝐷) |
59 | | elfzelz 12213 |
. . . . . . . 8
⊢ (𝑚 ∈
(1...(⌊‘(𝑥↑2))) → 𝑚 ∈ ℤ) |
60 | 59 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → 𝑚 ∈ ℤ) |
61 | 9, 6, 10, 7, 58, 60 | dchrzrhcl 24770 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
62 | 61 | adantr 480 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
63 | | elfznn 12241 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(1...(⌊‘(𝑥↑2))) → 𝑚 ∈ ℕ) |
64 | 63 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → 𝑚 ∈ ℕ) |
65 | 64 | nnrpd 11746 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → 𝑚 ∈ ℝ+) |
66 | | elfznn 12241 |
. . . . . . . . 9
⊢ (𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚))) → 𝑑 ∈ ℕ) |
67 | 66 | nnrpd 11746 |
. . . . . . . 8
⊢ (𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚))) → 𝑑 ∈ ℝ+) |
68 | | rpmulcl 11731 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℝ+
∧ 𝑑 ∈
ℝ+) → (𝑚 · 𝑑) ∈
ℝ+) |
69 | 65, 67, 68 | syl2an 493 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑚 · 𝑑) ∈
ℝ+) |
70 | 69 | rpsqrtcld 13998 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘(𝑚 · 𝑑)) ∈
ℝ+) |
71 | 70 | rpcnd 11750 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘(𝑚 · 𝑑)) ∈ ℂ) |
72 | 70 | rpne0d 11753 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘(𝑚 · 𝑑)) ≠ 0) |
73 | 62, 71, 72 | divcld 10680 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) ∈ ℂ) |
74 | 57, 73 | fsumcl 14311 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) ∈ ℂ) |
75 | 56, 74 | fsumcl 14311 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) ∈ ℂ) |
76 | 75 | abscld 14023 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ ℝ) |
77 | 76 | adantrr 749 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ ℝ) |
78 | 64 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑚 ∈ ℕ) |
79 | 78 | nnrpd 11746 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑚 ∈ ℝ+) |
80 | 79 | rprege0d 11755 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑚 ∈ ℝ ∧ 0 ≤ 𝑚)) |
81 | 66 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑑 ∈ ℕ) |
82 | 81 | nnrpd 11746 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑑 ∈ ℝ+) |
83 | 82 | rprege0d 11755 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑑 ∈ ℝ ∧ 0 ≤ 𝑑)) |
84 | | sqrtmul 13848 |
. . . . . . . . . . 11
⊢ (((𝑚 ∈ ℝ ∧ 0 ≤
𝑚) ∧ (𝑑 ∈ ℝ ∧ 0 ≤
𝑑)) →
(√‘(𝑚 ·
𝑑)) = ((√‘𝑚) · (√‘𝑑))) |
85 | 80, 83, 84 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘(𝑚 · 𝑑)) = ((√‘𝑚) · (√‘𝑑))) |
86 | 85 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = ((𝑋‘(𝐿‘𝑚)) / ((√‘𝑚) · (√‘𝑑)))) |
87 | 79 | rpsqrtcld 13998 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘𝑚) ∈
ℝ+) |
88 | 87 | rpcnne0d 11757 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((√‘𝑚) ∈ ℂ ∧
(√‘𝑚) ≠
0)) |
89 | 82 | rpsqrtcld 13998 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘𝑑) ∈
ℝ+) |
90 | 89 | rpcnne0d 11757 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((√‘𝑑) ∈ ℂ ∧
(√‘𝑑) ≠
0)) |
91 | | divdiv1 10615 |
. . . . . . . . . 10
⊢ (((𝑋‘(𝐿‘𝑚)) ∈ ℂ ∧ ((√‘𝑚) ∈ ℂ ∧
(√‘𝑚) ≠ 0)
∧ ((√‘𝑑)
∈ ℂ ∧ (√‘𝑑) ≠ 0)) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = ((𝑋‘(𝐿‘𝑚)) / ((√‘𝑚) · (√‘𝑑)))) |
92 | 62, 88, 90, 91 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = ((𝑋‘(𝐿‘𝑚)) / ((√‘𝑚) · (√‘𝑑)))) |
93 | 86, 92 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) |
94 | 93 | sumeq2dv 14281 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) |
95 | 94 | sumeq2dv 14281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) |
96 | 95 | adantrr 749 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) |
97 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
98 | 97 | rpred 11748 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ) |
99 | | reflcl 12459 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ∈
ℝ) |
100 | 98, 99 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘𝑥) ∈
ℝ) |
101 | 100 | ltp1d 10833 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘𝑥) <
((⌊‘𝑥) +
1)) |
102 | | fzdisj 12239 |
. . . . . . . 8
⊢
((⌊‘𝑥)
< ((⌊‘𝑥) +
1) → ((1...(⌊‘𝑥)) ∩ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))) = ∅) |
103 | 101, 102 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((1...(⌊‘𝑥))
∩ (((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2)))) = ∅) |
104 | 103 | adantrr 749 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((1...(⌊‘𝑥))
∩ (((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2)))) = ∅) |
105 | 97 | rprege0d 11755 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤
𝑥)) |
106 | | flge0nn0 12483 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
107 | | nn0p1nn 11209 |
. . . . . . . . . 10
⊢
((⌊‘𝑥)
∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ) |
108 | 105, 106,
107 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘𝑥) + 1)
∈ ℕ) |
109 | | nnuz 11599 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
110 | 108, 109 | syl6eleq 2698 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘𝑥) + 1)
∈ (ℤ≥‘1)) |
111 | 110 | adantrr 749 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((⌊‘𝑥) + 1)
∈ (ℤ≥‘1)) |
112 | 98 | adantrr 749 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ∈
ℝ) |
113 | | 2z 11286 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
114 | | rpexpcl 12741 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝑥↑2) ∈
ℝ+) |
115 | 97, 113, 114 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑2) ∈
ℝ+) |
116 | 115 | adantrr 749 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥↑2) ∈
ℝ+) |
117 | 116 | rpred 11748 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥↑2) ∈
ℝ) |
118 | 112 | recnd 9947 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ∈
ℂ) |
119 | 118 | mulid1d 9936 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥 · 1) = 𝑥) |
120 | | simprr 792 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 1 ≤ 𝑥) |
121 | | 1red 9934 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 1 ∈
ℝ) |
122 | | rpregt0 11722 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
123 | 122 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥 ∈ ℝ ∧ 0 <
𝑥)) |
124 | | lemul2 10755 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 𝑥
∈ ℝ ∧ (𝑥
∈ ℝ ∧ 0 < 𝑥)) → (1 ≤ 𝑥 ↔ (𝑥 · 1) ≤ (𝑥 · 𝑥))) |
125 | 121, 112,
123, 124 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (1 ≤ 𝑥 ↔ (𝑥 · 1) ≤ (𝑥 · 𝑥))) |
126 | 120, 125 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥 · 1) ≤ (𝑥 · 𝑥)) |
127 | 119, 126 | eqbrtrrd 4607 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ≤ (𝑥 · 𝑥)) |
128 | 118 | sqvald 12867 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥↑2) = (𝑥 · 𝑥)) |
129 | 127, 128 | breqtrrd 4611 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ≤ (𝑥↑2)) |
130 | | flword2 12476 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ (𝑥↑2) ∈ ℝ ∧
𝑥 ≤ (𝑥↑2)) → (⌊‘(𝑥↑2)) ∈
(ℤ≥‘(⌊‘𝑥))) |
131 | 112, 117,
129, 130 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(⌊‘(𝑥↑2))
∈ (ℤ≥‘(⌊‘𝑥))) |
132 | | fzsplit2 12237 |
. . . . . . 7
⊢
((((⌊‘𝑥)
+ 1) ∈ (ℤ≥‘1) ∧ (⌊‘(𝑥↑2)) ∈
(ℤ≥‘(⌊‘𝑥))) → (1...(⌊‘(𝑥↑2))) =
((1...(⌊‘𝑥))
∪ (((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2))))) |
133 | 111, 131,
132 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(1...(⌊‘(𝑥↑2))) = ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))))) |
134 | | fzfid 12634 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(1...(⌊‘(𝑥↑2))) ∈ Fin) |
135 | 94, 74 | eqeltrrd 2689 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ) |
136 | 135 | adantlrr 753 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ) |
137 | 104, 133,
134, 136 | fsumsplit 14318 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = (Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))) |
138 | 96, 137 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = (Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))) |
139 | 138 | fveq2d 6107 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))))) |
140 | | eqle 10018 |
. . 3
⊢
(((abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ ℝ ∧
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))))) → (abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ≤ (abs‘(Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))))) |
141 | 77, 139, 140 | syl2anc 691 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ≤ (abs‘(Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))))) |
142 | 1, 53, 55, 75, 141 | o1le 14231 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1)) |