Step | Hyp | Ref
| Expression |
1 | | 1red 10377 |
. 2
⊢ (𝜑 → 1 ∈
ℝ) |
2 | | sumex 14826 |
. . . 4
⊢
Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ V |
3 | 2 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ V) |
4 | | sumex 14826 |
. . . 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 3908 |
. . . . . . . 8
⊢ {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} ⊆ (𝐷 ∖ { 1 }) |
14 | 12, 13 | eqsstri 3854 |
. . . . . . 7
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
15 | | difss 3960 |
. . . . . . 7
⊢ (𝐷 ∖ { 1 }) ⊆ 𝐷 |
16 | 14, 15 | sstri 3830 |
. . . . . 6
⊢ 𝑊 ⊆ 𝐷 |
17 | | dchrisum0.b |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
18 | 16, 17 | sseldi 3819 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
19 | 14, 17 | sseldi 3819 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝐷 ∖ { 1 })) |
20 | | eldifsni 4553 |
. . . . . 6
⊢ (𝑋 ∈ (𝐷 ∖ { 1 }) → 𝑋 ≠ 1 ) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋 ≠ 1 ) |
22 | | eqid 2778 |
. . . . 5
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) |
23 | 6, 7, 8, 9, 10, 11, 18, 21, 22 | dchrmusumlema 25634 |
. . . 4
⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦))) |
24 | 8 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑁 ∈ ℕ) |
25 | 17 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑋 ∈ 𝑊) |
26 | | dchrisum0lem1.f |
. . . . . . 7
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) |
27 | | dchrisum0.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) |
28 | 27 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝐶 ∈ (0[,)+∞)) |
29 | | dchrisum0.s |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) |
30 | 29 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , 𝐹) ⇝ 𝑆) |
31 | | dchrisum0.1 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) |
32 | 31 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) |
33 | | eqid 2778 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) = (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) |
34 | 33 | divsqrsum 25160 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) ∈ dom
⇝𝑟 |
35 | 33 | divsqrsumf 25159 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))):ℝ+⟶ℝ |
36 | | ax-resscn 10329 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
37 | | fss 6304 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))):ℝ+⟶ℝ ∧
ℝ ⊆ ℂ) → (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))):ℝ+⟶ℂ) |
38 | 35, 36, 37 | mp2an 682 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))):ℝ+⟶ℂ |
39 | 38 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))):ℝ+⟶ℂ) |
40 | | rpsup 12984 |
. . . . . . . . . . 11
⊢
sup(ℝ+, ℝ*, < ) =
+∞ |
41 | 40 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → sup(ℝ+,
ℝ*, < ) = +∞) |
42 | 39, 41 | rlimdm 14690 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) ∈ dom ⇝𝑟
↔ (𝑦 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 ·
(√‘𝑦))))
⇝𝑟 ( ⇝𝑟 ‘(𝑦 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦))))))) |
43 | 34, 42 | mpbii 225 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) ⇝𝑟 (
⇝𝑟 ‘(𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))))) |
44 | 43 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) ⇝𝑟 (
⇝𝑟 ‘(𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))))) |
45 | | simprl 761 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑐 ∈ (0[,)+∞)) |
46 | | simprrl 771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡) |
47 | | simprrr 772 |
. . . . . . 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 25659 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1)) |
49 | 48 | rexlimdvaa 3214 |
. . . . 5
⊢ (𝜑 → (∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1))) |
50 | 49 | exlimdv 1976 |
. . . 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 25657 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1)) |
53 | 3, 5, 51, 52 | o1add2 14762 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))) ∈ 𝑂(1)) |
54 | | ovexd 6956 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ V) |
55 | | fzfid 13091 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘(𝑥↑2))) ∈ Fin) |
56 | | fzfid 13091 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) →
(1...(⌊‘((𝑥↑2) / 𝑚))) ∈ Fin) |
57 | 18 | ad2antrr 716 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → 𝑋 ∈ 𝐷) |
58 | | elfzelz 12659 |
. . . . . . . 8
⊢ (𝑚 ∈
(1...(⌊‘(𝑥↑2))) → 𝑚 ∈ ℤ) |
59 | 58 | adantl 475 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → 𝑚 ∈ ℤ) |
60 | 9, 6, 10, 7, 57, 59 | dchrzrhcl 25422 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
61 | 60 | adantr 474 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
62 | | elfznn 12687 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(1...(⌊‘(𝑥↑2))) → 𝑚 ∈ ℕ) |
63 | 62 | adantl 475 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → 𝑚 ∈ ℕ) |
64 | 63 | nnrpd 12179 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → 𝑚 ∈ ℝ+) |
65 | | elfznn 12687 |
. . . . . . . . 9
⊢ (𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚))) → 𝑑 ∈ ℕ) |
66 | 65 | nnrpd 12179 |
. . . . . . . 8
⊢ (𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚))) → 𝑑 ∈ ℝ+) |
67 | | rpmulcl 12162 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℝ+
∧ 𝑑 ∈
ℝ+) → (𝑚 · 𝑑) ∈
ℝ+) |
68 | 64, 66, 67 | syl2an 589 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑚 · 𝑑) ∈
ℝ+) |
69 | 68 | rpsqrtcld 14558 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘(𝑚 · 𝑑)) ∈
ℝ+) |
70 | 69 | rpcnd 12183 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘(𝑚 · 𝑑)) ∈ ℂ) |
71 | 69 | rpne0d 12186 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘(𝑚 · 𝑑)) ≠ 0) |
72 | 61, 70, 71 | divcld 11151 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) ∈ ℂ) |
73 | 56, 72 | fsumcl 14871 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) ∈ ℂ) |
74 | 55, 73 | fsumcl 14871 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) ∈ ℂ) |
75 | 74 | abscld 14583 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ ℝ) |
76 | 75 | adantrr 707 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ ℝ) |
77 | 63 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑚 ∈ ℕ) |
78 | 77 | nnrpd 12179 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑚 ∈ ℝ+) |
79 | 78 | rprege0d 12188 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑚 ∈ ℝ ∧ 0 ≤ 𝑚)) |
80 | 65 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑑 ∈ ℕ) |
81 | 80 | nnrpd 12179 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑑 ∈ ℝ+) |
82 | 81 | rprege0d 12188 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑑 ∈ ℝ ∧ 0 ≤ 𝑑)) |
83 | | sqrtmul 14407 |
. . . . . . . . . . 11
⊢ (((𝑚 ∈ ℝ ∧ 0 ≤
𝑚) ∧ (𝑑 ∈ ℝ ∧ 0 ≤
𝑑)) →
(√‘(𝑚 ·
𝑑)) = ((√‘𝑚) · (√‘𝑑))) |
84 | 79, 82, 83 | syl2anc 579 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘(𝑚 · 𝑑)) = ((√‘𝑚) · (√‘𝑑))) |
85 | 84 | oveq2d 6938 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = ((𝑋‘(𝐿‘𝑚)) / ((√‘𝑚) · (√‘𝑑)))) |
86 | 78 | rpsqrtcld 14558 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘𝑚) ∈
ℝ+) |
87 | 86 | rpcnne0d 12190 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((√‘𝑚) ∈ ℂ ∧
(√‘𝑚) ≠
0)) |
88 | 81 | rpsqrtcld 14558 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘𝑑) ∈
ℝ+) |
89 | 88 | rpcnne0d 12190 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((√‘𝑑) ∈ ℂ ∧
(√‘𝑑) ≠
0)) |
90 | | divdiv1 11086 |
. . . . . . . . . 10
⊢ (((𝑋‘(𝐿‘𝑚)) ∈ ℂ ∧ ((√‘𝑚) ∈ ℂ ∧
(√‘𝑚) ≠ 0)
∧ ((√‘𝑑)
∈ ℂ ∧ (√‘𝑑) ≠ 0)) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = ((𝑋‘(𝐿‘𝑚)) / ((√‘𝑚) · (√‘𝑑)))) |
91 | 61, 87, 89, 90 | syl3anc 1439 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = ((𝑋‘(𝐿‘𝑚)) / ((√‘𝑚) · (√‘𝑑)))) |
92 | 85, 91 | eqtr4d 2817 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) |
93 | 92 | sumeq2dv 14841 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) |
94 | 93 | sumeq2dv 14841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) |
95 | 94 | adantrr 707 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) |
96 | | simpr 479 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
97 | 96 | rpred 12181 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ) |
98 | | reflcl 12916 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ∈
ℝ) |
99 | 97, 98 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘𝑥) ∈
ℝ) |
100 | 99 | ltp1d 11308 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘𝑥) <
((⌊‘𝑥) +
1)) |
101 | | fzdisj 12685 |
. . . . . . . 8
⊢
((⌊‘𝑥)
< ((⌊‘𝑥) +
1) → ((1...(⌊‘𝑥)) ∩ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))) = ∅) |
102 | 100, 101 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((1...(⌊‘𝑥))
∩ (((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2)))) = ∅) |
103 | 102 | adantrr 707 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((1...(⌊‘𝑥))
∩ (((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2)))) = ∅) |
104 | 96 | rprege0d 12188 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤
𝑥)) |
105 | | flge0nn0 12940 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
106 | | nn0p1nn 11683 |
. . . . . . . . . 10
⊢
((⌊‘𝑥)
∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ) |
107 | 104, 105,
106 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘𝑥) + 1)
∈ ℕ) |
108 | | nnuz 12029 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
109 | 107, 108 | syl6eleq 2869 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘𝑥) + 1)
∈ (ℤ≥‘1)) |
110 | 109 | adantrr 707 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((⌊‘𝑥) + 1)
∈ (ℤ≥‘1)) |
111 | 97 | adantrr 707 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ∈
ℝ) |
112 | | 2z 11761 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
113 | | rpexpcl 13197 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝑥↑2) ∈
ℝ+) |
114 | 96, 112, 113 | sylancl 580 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑2) ∈
ℝ+) |
115 | 114 | adantrr 707 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥↑2) ∈
ℝ+) |
116 | 115 | rpred 12181 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥↑2) ∈
ℝ) |
117 | 111 | recnd 10405 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ∈
ℂ) |
118 | 117 | mulid1d 10394 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥 · 1) = 𝑥) |
119 | | simprr 763 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 1 ≤ 𝑥) |
120 | | 1red 10377 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 1 ∈
ℝ) |
121 | | rpregt0 12153 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
122 | 121 | ad2antrl 718 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥 ∈ ℝ ∧ 0 <
𝑥)) |
123 | | lemul2 11230 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 𝑥
∈ ℝ ∧ (𝑥
∈ ℝ ∧ 0 < 𝑥)) → (1 ≤ 𝑥 ↔ (𝑥 · 1) ≤ (𝑥 · 𝑥))) |
124 | 120, 111,
122, 123 | syl3anc 1439 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (1 ≤ 𝑥 ↔ (𝑥 · 1) ≤ (𝑥 · 𝑥))) |
125 | 119, 124 | mpbid 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥 · 1) ≤ (𝑥 · 𝑥)) |
126 | 118, 125 | eqbrtrrd 4910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ≤ (𝑥 · 𝑥)) |
127 | 117 | sqvald 13324 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (𝑥↑2) = (𝑥 · 𝑥)) |
128 | 126, 127 | breqtrrd 4914 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ≤ (𝑥↑2)) |
129 | | flword2 12933 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ (𝑥↑2) ∈ ℝ ∧
𝑥 ≤ (𝑥↑2)) → (⌊‘(𝑥↑2)) ∈
(ℤ≥‘(⌊‘𝑥))) |
130 | 111, 116,
128, 129 | syl3anc 1439 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(⌊‘(𝑥↑2))
∈ (ℤ≥‘(⌊‘𝑥))) |
131 | | fzsplit2 12683 |
. . . . . . 7
⊢
((((⌊‘𝑥)
+ 1) ∈ (ℤ≥‘1) ∧ (⌊‘(𝑥↑2)) ∈
(ℤ≥‘(⌊‘𝑥))) → (1...(⌊‘(𝑥↑2))) =
((1...(⌊‘𝑥))
∪ (((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2))))) |
132 | 110, 130,
131 | syl2anc 579 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(1...(⌊‘(𝑥↑2))) = ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))))) |
133 | | fzfid 13091 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(1...(⌊‘(𝑥↑2))) ∈ Fin) |
134 | 93, 73 | eqeltrrd 2860 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ) |
135 | 134 | adantlrr 711 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑚 ∈
(1...(⌊‘(𝑥↑2)))) → Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ) |
136 | 103, 132,
133, 135 | fsumsplit 14878 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = (Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))) |
137 | 95, 136 | eqtrd 2814 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = (Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))) |
138 | 137 | fveq2d 6450 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))))) |
139 | | eqle 10478 |
. . 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 579 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ≤ (abs‘(Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))))) |
141 | 1, 53, 54, 74, 140 | o1le 14791 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1)) |