Step | Hyp | Ref
| Expression |
1 | | 1red 10247 |
. 2
⊢ (𝜑 → 1 ∈
ℝ) |
2 | | sumex 14617 |
. . . 4
⊢
Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ V |
3 | 2 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ V) |
4 | | sumex 14617 |
. . . 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 3828 |
. . . . . . . 8
⊢ {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} ⊆ (𝐷 ∖ { 1 }) |
14 | 12, 13 | eqsstri 3776 |
. . . . . . 7
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
15 | | difss 3880 |
. . . . . . 7
⊢ (𝐷 ∖ { 1 }) ⊆ 𝐷 |
16 | 14, 15 | sstri 3753 |
. . . . . 6
⊢ 𝑊 ⊆ 𝐷 |
17 | | dchrisum0.b |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
18 | 16, 17 | sseldi 3742 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
19 | 14, 17 | sseldi 3742 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝐷 ∖ { 1 })) |
20 | | eldifsni 4466 |
. . . . . 6
⊢ (𝑋 ∈ (𝐷 ∖ { 1 }) → 𝑋 ≠ 1 ) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋 ≠ 1 ) |
22 | | eqid 2760 |
. . . . 5
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) |
23 | 6, 7, 8, 9, 10, 11, 18, 21, 22 | dchrmusumlema 25381 |
. . . 4
⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦))) |
24 | 8 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑁 ∈ ℕ) |
25 | 17 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑋 ∈ 𝑊) |
26 | | dchrisum0lem1.f |
. . . . . . 7
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) |
27 | | dchrisum0.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) |
28 | 27 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝐶 ∈ (0[,)+∞)) |
29 | | dchrisum0.s |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) |
30 | 29 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , 𝐹) ⇝ 𝑆) |
31 | | dchrisum0.1 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) |
32 | 31 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) |
33 | | eqid 2760 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) = (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) |
34 | 33 | divsqrsum 24907 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) ∈ dom
⇝𝑟 |
35 | 33 | divsqrsumf 24906 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))):ℝ+⟶ℝ |
36 | | ax-resscn 10185 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
37 | | fss 6217 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))):ℝ+⟶ℝ ∧
ℝ ⊆ ℂ) → (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))):ℝ+⟶ℂ) |
38 | 35, 36, 37 | mp2an 710 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))):ℝ+⟶ℂ |
39 | 38 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))):ℝ+⟶ℂ) |
40 | | rpsup 12859 |
. . . . . . . . . . 11
⊢
sup(ℝ+, ℝ*, < ) =
+∞ |
41 | 40 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → sup(ℝ+,
ℝ*, < ) = +∞) |
42 | 39, 41 | rlimdm 14481 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) ∈ dom ⇝𝑟
↔ (𝑦 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 ·
(√‘𝑦))))
⇝𝑟 ( ⇝𝑟 ‘(𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦))))))) |
43 | 34, 42 | mpbii 223 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) ⇝𝑟 (
⇝𝑟 ‘(𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))))) |
44 | 43 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) ⇝𝑟 (
⇝𝑟 ‘(𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))))) |
45 | | simprl 811 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑐 ∈ (0[,)+∞)) |
46 | | simprrl 823 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡) |
47 | | simprrr 824 |
. . . . . . 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 25406 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1)) |
49 | 48 | rexlimdvaa 3170 |
. . . . 5
⊢ (𝜑 → (∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1))) |
50 | 49 | exlimdv 2010 |
. . . 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 25404 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1)) |
53 | 3, 5, 51, 52 | o1add2 14553 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))) ∈ 𝑂(1)) |
54 | | ovexd 6843 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ V) |
55 | | fzfid 12966 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘(𝑥↑2))) ∈ Fin) |
56 | | fzfid 12966 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) →
(1...(⌊‘((𝑥↑2) / 𝑚))) ∈ Fin) |
57 | 18 | ad2antrr 764 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → 𝑋 ∈ 𝐷) |
58 | | elfzelz 12535 |
. . . . . . . 8
⊢ (𝑚 ∈
(1...(⌊‘(𝑥↑2))) → 𝑚 ∈ ℤ) |
59 | 58 | adantl 473 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → 𝑚 ∈ ℤ) |
60 | 9, 6, 10, 7, 57, 59 | dchrzrhcl 25169 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
61 | 60 | adantr 472 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
62 | | elfznn 12563 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(1...(⌊‘(𝑥↑2))) → 𝑚 ∈ ℕ) |
63 | 62 | adantl 473 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → 𝑚 ∈ ℕ) |
64 | 63 | nnrpd 12063 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → 𝑚 ∈ ℝ+) |
65 | | elfznn 12563 |
. . . . . . . . 9
⊢ (𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚))) → 𝑑 ∈ ℕ) |
66 | 65 | nnrpd 12063 |
. . . . . . . 8
⊢ (𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚))) → 𝑑 ∈ ℝ+) |
67 | | rpmulcl 12048 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℝ+
∧ 𝑑 ∈
ℝ+) → (𝑚 · 𝑑) ∈
ℝ+) |
68 | 64, 66, 67 | syl2an 495 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑚 · 𝑑) ∈
ℝ+) |
69 | 68 | rpsqrtcld 14349 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘(𝑚 · 𝑑)) ∈
ℝ+) |
70 | 69 | rpcnd 12067 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘(𝑚 · 𝑑)) ∈ ℂ) |
71 | 69 | rpne0d 12070 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘(𝑚 · 𝑑)) ≠ 0) |
72 | 61, 70, 71 | divcld 10993 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) ∈ ℂ) |
73 | 56, 72 | fsumcl 14663 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) ∈ ℂ) |
74 | 55, 73 | fsumcl 14663 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) ∈ ℂ) |
75 | 74 | abscld 14374 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ ℝ) |
76 | 75 | adantrr 755 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ ℝ) |
77 | 63 | adantr 472 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑚 ∈ ℕ) |
78 | 77 | nnrpd 12063 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑚 ∈ ℝ+) |
79 | 78 | rprege0d 12072 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑚 ∈ ℝ ∧ 0 ≤ 𝑚)) |
80 | 65 | adantl 473 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑑 ∈ ℕ) |
81 | 80 | nnrpd 12063 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑑 ∈ ℝ+) |
82 | 81 | rprege0d 12072 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑑 ∈ ℝ ∧ 0 ≤ 𝑑)) |
83 | | sqrtmul 14199 |
. . . . . . . . . . 11
⊢ (((𝑚 ∈ ℝ ∧ 0 ≤
𝑚) ∧ (𝑑 ∈ ℝ ∧ 0 ≤
𝑑)) →
(√‘(𝑚 ·
𝑑)) = ((√‘𝑚) · (√‘𝑑))) |
84 | 79, 82, 83 | syl2anc 696 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘(𝑚 · 𝑑)) = ((√‘𝑚) · (√‘𝑑))) |
85 | 84 | oveq2d 6829 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = ((𝑋‘(𝐿‘𝑚)) / ((√‘𝑚) · (√‘𝑑)))) |
86 | 78 | rpsqrtcld 14349 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘𝑚) ∈
ℝ+) |
87 | 86 | rpcnne0d 12074 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((√‘𝑚) ∈ ℂ ∧
(√‘𝑚) ≠
0)) |
88 | 81 | rpsqrtcld 14349 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘𝑑) ∈
ℝ+) |
89 | 88 | rpcnne0d 12074 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((√‘𝑑) ∈ ℂ ∧
(√‘𝑑) ≠
0)) |
90 | | divdiv1 10928 |
. . . . . . . . . 10
⊢ (((𝑋‘(𝐿‘𝑚)) ∈ ℂ ∧ ((√‘𝑚) ∈ ℂ ∧
(√‘𝑚) ≠ 0)
∧ ((√‘𝑑)
∈ ℂ ∧ (√‘𝑑) ≠ 0)) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = ((𝑋‘(𝐿‘𝑚)) / ((√‘𝑚) · (√‘𝑑)))) |
91 | 61, 87, 89, 90 | syl3anc 1477 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = ((𝑋‘(𝐿‘𝑚)) / ((√‘𝑚) · (√‘𝑑)))) |
92 | 85, 91 | eqtr4d 2797 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) |
93 | 92 | sumeq2dv 14632 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) |
94 | 93 | sumeq2dv 14632 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) |
95 | 94 | adantrr 755 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) |
96 | | simpr 479 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
97 | 96 | rpred 12065 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ) |
98 | | reflcl 12791 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ∈
ℝ) |
99 | 97, 98 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘𝑥) ∈
ℝ) |
100 | 99 | ltp1d 11146 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘𝑥) <
((⌊‘𝑥) +
1)) |
101 | | fzdisj 12561 |
. . . . . . . 8
⊢
((⌊‘𝑥)
< ((⌊‘𝑥) +
1) → ((1...(⌊‘𝑥)) ∩ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))) = ∅) |
102 | 100, 101 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((1...(⌊‘𝑥))
∩ (((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2)))) = ∅) |
103 | 102 | adantrr 755 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((1...(⌊‘𝑥))
∩ (((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2)))) = ∅) |
104 | 96 | rprege0d 12072 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤
𝑥)) |
105 | | flge0nn0 12815 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
106 | | nn0p1nn 11524 |
. . . . . . . . . 10
⊢
((⌊‘𝑥)
∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ) |
107 | 104, 105,
106 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘𝑥) + 1)
∈ ℕ) |
108 | | nnuz 11916 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
109 | 107, 108 | syl6eleq 2849 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘𝑥) + 1)
∈ (ℤ≥‘1)) |
110 | 109 | adantrr 755 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((⌊‘𝑥) + 1)
∈ (ℤ≥‘1)) |
111 | 97 | adantrr 755 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ∈
ℝ) |
112 | | 2z 11601 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
113 | | rpexpcl 13073 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝑥↑2) ∈
ℝ+) |
114 | 96, 112, 113 | sylancl 697 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑2) ∈
ℝ+) |
115 | 114 | adantrr 755 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥↑2) ∈
ℝ+) |
116 | 115 | rpred 12065 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥↑2) ∈
ℝ) |
117 | 111 | recnd 10260 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ∈
ℂ) |
118 | 117 | mulid1d 10249 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥 · 1) = 𝑥) |
119 | | simprr 813 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 1 ≤ 𝑥) |
120 | | 1red 10247 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 1 ∈
ℝ) |
121 | | rpregt0 12039 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
122 | 121 | ad2antrl 766 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥 ∈ ℝ ∧ 0 <
𝑥)) |
123 | | lemul2 11068 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 𝑥
∈ ℝ ∧ (𝑥
∈ ℝ ∧ 0 < 𝑥)) → (1 ≤ 𝑥 ↔ (𝑥 · 1) ≤ (𝑥 · 𝑥))) |
124 | 120, 111,
122, 123 | syl3anc 1477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (1 ≤ 𝑥 ↔ (𝑥 · 1) ≤ (𝑥 · 𝑥))) |
125 | 119, 124 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥 · 1) ≤ (𝑥 · 𝑥)) |
126 | 118, 125 | eqbrtrrd 4828 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ≤ (𝑥 · 𝑥)) |
127 | 117 | sqvald 13199 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥↑2) = (𝑥 · 𝑥)) |
128 | 126, 127 | breqtrrd 4832 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ≤ (𝑥↑2)) |
129 | | flword2 12808 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ (𝑥↑2) ∈ ℝ ∧
𝑥 ≤ (𝑥↑2)) → (⌊‘(𝑥↑2)) ∈
(ℤ≥‘(⌊‘𝑥))) |
130 | 111, 116,
128, 129 | syl3anc 1477 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(⌊‘(𝑥↑2))
∈ (ℤ≥‘(⌊‘𝑥))) |
131 | | fzsplit2 12559 |
. . . . . . 7
⊢
((((⌊‘𝑥)
+ 1) ∈ (ℤ≥‘1) ∧ (⌊‘(𝑥↑2)) ∈
(ℤ≥‘(⌊‘𝑥))) → (1...(⌊‘(𝑥↑2))) =
((1...(⌊‘𝑥))
∪ (((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2))))) |
132 | 110, 130,
131 | syl2anc 696 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(1...(⌊‘(𝑥↑2))) = ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))))) |
133 | | fzfid 12966 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(1...(⌊‘(𝑥↑2))) ∈ Fin) |
134 | 93, 73 | eqeltrrd 2840 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ) |
135 | 134 | adantlrr 759 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ) |
136 | 103, 132,
133, 135 | fsumsplit 14670 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = (Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))) |
137 | 95, 136 | eqtrd 2794 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = (Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))) |
138 | 137 | fveq2d 6356 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))))) |
139 | | eqle 10331 |
. . 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) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))))) |
140 | 76, 138, 139 | syl2anc 696 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ≤ (abs‘(Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))))) |
141 | 1, 53, 54, 74, 140 | o1le 14582 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1)) |