Step | Hyp | Ref
| Expression |
1 | | rpvmasum.z |
. 2
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
2 | | rpvmasum.l |
. 2
⊢ 𝐿 = (ℤRHom‘𝑍) |
3 | | rpvmasum.a |
. 2
⊢ (𝜑 → 𝑁 ∈ ℕ) |
4 | | rpvmasum2.g |
. 2
⊢ 𝐺 = (DChr‘𝑁) |
5 | | rpvmasum2.d |
. 2
⊢ 𝐷 = (Base‘𝐺) |
6 | | rpvmasum2.1 |
. 2
⊢ 1 =
(0g‘𝐺) |
7 | | eqid 2610 |
. 2
⊢ (𝑏 ∈ ℕ ↦
Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦))) = (𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦))) |
8 | | rpvmasum2.w |
. . . . 5
⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} |
9 | | ssrab2 3650 |
. . . . 5
⊢ {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} ⊆ (𝐷 ∖ { 1 }) |
10 | 8, 9 | eqsstri 3598 |
. . . 4
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
11 | | difss 3699 |
. . . 4
⊢ (𝐷 ∖ { 1 }) ⊆ 𝐷 |
12 | 10, 11 | sstri 3577 |
. . 3
⊢ 𝑊 ⊆ 𝐷 |
13 | | dchrisum0.b |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
14 | 12, 13 | sseldi 3566 |
. 2
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
15 | 1, 2, 3, 4, 5, 6, 8, 13 | dchrisum0re 25002 |
. 2
⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) |
16 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = (𝑚 · 𝑑) → (√‘𝑘) = (√‘(𝑚 · 𝑑))) |
17 | 16 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑘 = (𝑚 · 𝑑) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘)) = ((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
18 | | rpre 11715 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
19 | 18 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ) |
20 | 14 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → 𝑋 ∈ 𝐷) |
21 | | elrabi 3328 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} → 𝑚 ∈ ℕ) |
22 | 21 | nnzd 11357 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} → 𝑚 ∈ ℤ) |
23 | 22 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → 𝑚 ∈ ℤ) |
24 | 4, 1, 5, 2, 20, 23 | dchrzrhcl 24770 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
25 | | elfznn 12241 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(1...(⌊‘𝑥))
→ 𝑘 ∈
ℕ) |
26 | 25 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ 𝑘 ∈
ℕ) |
27 | 26 | nnrpd 11746 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ 𝑘 ∈
ℝ+) |
28 | 27 | rpsqrtcld 13998 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑘)
∈ ℝ+) |
29 | 28 | rpcnd 11750 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑘)
∈ ℂ) |
30 | 29 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → (√‘𝑘) ∈ ℂ) |
31 | 28 | rpne0d 11753 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑘)
≠ 0) |
32 | 31 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → (√‘𝑘) ≠ 0) |
33 | 24, 30, 32 | divcld 10680 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘)) ∈ ℂ) |
34 | 33 | anasss 677 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘})) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘)) ∈ ℂ) |
35 | 17, 19, 34 | dvdsflsumcom 24714 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘)) = Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
36 | 1, 2, 3, 4, 5, 6, 7 | dchrisum0fval 24994 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → ((𝑏 ∈ ℕ ↦
Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) = Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} (𝑋‘(𝐿‘𝑚))) |
37 | 26, 36 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ ((𝑏 ∈ ℕ
↦ Σ𝑦 ∈
{𝑖 ∈ ℕ ∣
𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) = Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} (𝑋‘(𝐿‘𝑚))) |
38 | 37 | oveq1d 6564 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (((𝑏 ∈ ℕ
↦ Σ𝑦 ∈
{𝑖 ∈ ℕ ∣
𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘)) = (Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} (𝑋‘(𝐿‘𝑚)) / (√‘𝑘))) |
39 | | fzfid 12634 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (1...𝑘) ∈
Fin) |
40 | | dvdsssfz1 14878 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} ⊆ (1...𝑘)) |
41 | 26, 40 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ {𝑖 ∈ ℕ
∣ 𝑖 ∥ 𝑘} ⊆ (1...𝑘)) |
42 | | ssfi 8065 |
. . . . . . . . . 10
⊢
(((1...𝑘) ∈ Fin
∧ {𝑖 ∈ ℕ
∣ 𝑖 ∥ 𝑘} ⊆ (1...𝑘)) → {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} ∈ Fin) |
43 | 39, 41, 42 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ {𝑖 ∈ ℕ
∣ 𝑖 ∥ 𝑘} ∈ Fin) |
44 | 43, 29, 24, 31 | fsumdivc 14360 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
{𝑖 ∈ ℕ ∣
𝑖 ∥ 𝑘} (𝑋‘(𝐿‘𝑚)) / (√‘𝑘)) = Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘))) |
45 | 38, 44 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (((𝑏 ∈ ℕ
↦ Σ𝑦 ∈
{𝑖 ∈ ℕ ∣
𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘)) = Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘))) |
46 | 45 | sumeq2dv 14281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈
(1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘)) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘))) |
47 | | rprege0 11723 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
48 | 47 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤
𝑥)) |
49 | | resqrtth 13844 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
((√‘𝑥)↑2)
= 𝑥) |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((√‘𝑥)↑2)
= 𝑥) |
51 | 50 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘((√‘𝑥)↑2)) = (⌊‘𝑥)) |
52 | 51 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘((√‘𝑥)↑2))) = (1...(⌊‘𝑥))) |
53 | 50 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(((√‘𝑥)↑2)
/ 𝑚) = (𝑥 / 𝑚)) |
54 | 53 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘(((√‘𝑥)↑2) / 𝑚)) = (⌊‘(𝑥 / 𝑚))) |
55 | 54 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚))) = (1...(⌊‘(𝑥 / 𝑚)))) |
56 | 55 | sumeq1d 14279 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
57 | 56 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))) → Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
58 | 52, 57 | sumeq12dv 14284 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
59 | 35, 46, 58 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈
(1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘)) = Σ𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
60 | 59 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑘 ∈
(1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘))) = (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))))) |
61 | | rpsqrtcl 13853 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (√‘𝑥)
∈ ℝ+) |
62 | 61 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℝ+) |
63 | | eqidd 2611 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(√‘𝑥)) = (𝑥 ∈ ℝ+
↦ (√‘𝑥))) |
64 | | eqidd 2611 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) = (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))))) |
65 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑧 = (√‘𝑥) → (𝑧↑2) = ((√‘𝑥)↑2)) |
66 | 65 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑧 = (√‘𝑥) → (⌊‘(𝑧↑2)) =
(⌊‘((√‘𝑥)↑2))) |
67 | 66 | oveq2d 6565 |
. . . . . 6
⊢ (𝑧 = (√‘𝑥) →
(1...(⌊‘(𝑧↑2))) =
(1...(⌊‘((√‘𝑥)↑2)))) |
68 | 65 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑧 = (√‘𝑥) → ((𝑧↑2) / 𝑚) = (((√‘𝑥)↑2) / 𝑚)) |
69 | 68 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑧 = (√‘𝑥) → (⌊‘((𝑧↑2) / 𝑚)) = (⌊‘(((√‘𝑥)↑2) / 𝑚))) |
70 | 69 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑧 = (√‘𝑥) →
(1...(⌊‘((𝑧↑2) / 𝑚))) =
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))) |
71 | 70 | sumeq1d 14279 |
. . . . . . 7
⊢ (𝑧 = (√‘𝑥) → Σ𝑑 ∈
(1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
72 | 71 | adantr 480 |
. . . . . 6
⊢ ((𝑧 = (√‘𝑥) ∧ 𝑚 ∈ (1...(⌊‘(𝑧↑2)))) → Σ𝑑 ∈
(1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
73 | 67, 72 | sumeq12dv 14284 |
. . . . 5
⊢ (𝑧 = (√‘𝑥) → Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
74 | 62, 63, 64, 73 | fmptco 6303 |
. . . 4
⊢ (𝜑 → ((𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∘ (𝑥 ∈ ℝ+ ↦
(√‘𝑥))) =
(𝑥 ∈
ℝ+ ↦ Σ𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))))) |
75 | 60, 74 | eqtr4d 2647 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑘 ∈
(1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘))) = ((𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∘ (𝑥 ∈ ℝ+ ↦
(√‘𝑥)))) |
76 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) |
77 | 1, 2, 3, 4, 5, 6, 8, 13, 76 | dchrisum0lema 25003 |
. . . . . . 7
⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦)))) |
78 | 3 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → 𝑁 ∈ ℕ) |
79 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → 𝑋 ∈ 𝑊) |
80 | | simprl 790 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → 𝑐 ∈ (0[,)+∞)) |
81 | | simprrl 800 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡) |
82 | | simprrr 801 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))) |
83 | 1, 2, 78, 4, 5, 6,
8, 79, 76, 80, 81, 82 | dchrisum0lem3 25008 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1)) |
84 | 83 | rexlimdvaa 3014 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))) → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1))) |
85 | 84 | exlimdv 1848 |
. . . . . . 7
⊢ (𝜑 → (∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))) → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1))) |
86 | 77, 85 | mpd 15 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1)) |
87 | | o1f 14108 |
. . . . . 6
⊢ ((𝑧 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1) → (𝑧 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))):dom (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))))⟶ℂ) |
88 | 86, 87 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))):dom (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))))⟶ℂ) |
89 | | sumex 14266 |
. . . . . . 7
⊢
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) ∈ V |
90 | | eqid 2610 |
. . . . . . 7
⊢ (𝑧 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) = (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
91 | 89, 90 | dmmpti 5936 |
. . . . . 6
⊢ dom
(𝑧 ∈
ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈
(1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) = ℝ+ |
92 | 91 | feq2i 5950 |
. . . . 5
⊢ ((𝑧 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))):dom (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))))⟶ℂ ↔ (𝑧 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))):ℝ+⟶ℂ) |
93 | 88, 92 | sylib 207 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))):ℝ+⟶ℂ) |
94 | | rpssre 11719 |
. . . . 5
⊢
ℝ+ ⊆ ℝ |
95 | 94 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ+
⊆ ℝ) |
96 | | resqcl 12793 |
. . . . . 6
⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈
ℝ) |
97 | 96 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ) |
98 | | 0red 9920 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → 0 ∈ ℝ) |
99 | | simplr 788 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → 𝑡 ∈ ℝ) |
100 | | simplrr 797 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (𝑡↑2) ≤ 𝑥) |
101 | 47 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) |
102 | 101 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) |
103 | 102, 49 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → ((√‘𝑥)↑2) = 𝑥) |
104 | 100, 103 | breqtrrd 4611 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (𝑡↑2) ≤ ((√‘𝑥)↑2)) |
105 | 99 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → 𝑡 ∈ ℝ) |
106 | 62 | rpred 11748 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℝ) |
107 | 106 | ad2ant2r 779 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → (√‘𝑥) ∈ ℝ) |
108 | 107 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (√‘𝑥) ∈ ℝ) |
109 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → 0 ≤ 𝑡) |
110 | | sqrtge0 13846 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) → 0 ≤
(√‘𝑥)) |
111 | 101, 110 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → 0 ≤ (√‘𝑥)) |
112 | 111 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → 0 ≤ (√‘𝑥)) |
113 | 105, 108,
109, 112 | le2sqd 12906 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (𝑡 ≤ (√‘𝑥) ↔ (𝑡↑2) ≤ ((√‘𝑥)↑2))) |
114 | 104, 113 | mpbird 246 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → 𝑡 ≤ (√‘𝑥)) |
115 | 99 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 𝑡 ∈ ℝ) |
116 | | 0red 9920 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 0 ∈
ℝ) |
117 | 107 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → (√‘𝑥) ∈
ℝ) |
118 | | simpr 476 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 𝑡 ≤ 0) |
119 | 111 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 0 ≤ (√‘𝑥)) |
120 | 115, 116,
117, 118, 119 | letrd 10073 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 𝑡 ≤ (√‘𝑥)) |
121 | 98, 99, 114, 120 | lecasei 10022 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → 𝑡 ≤ (√‘𝑥)) |
122 | 121 | expr 641 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → ((𝑡↑2) ≤ 𝑥 → 𝑡 ≤ (√‘𝑥))) |
123 | 122 | ralrimiva 2949 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∀𝑥 ∈ ℝ+
((𝑡↑2) ≤ 𝑥 → 𝑡 ≤ (√‘𝑥))) |
124 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑐 = (𝑡↑2) → (𝑐 ≤ 𝑥 ↔ (𝑡↑2) ≤ 𝑥)) |
125 | 124 | imbi1d 330 |
. . . . . . 7
⊢ (𝑐 = (𝑡↑2) → ((𝑐 ≤ 𝑥 → 𝑡 ≤ (√‘𝑥)) ↔ ((𝑡↑2) ≤ 𝑥 → 𝑡 ≤ (√‘𝑥)))) |
126 | 125 | ralbidv 2969 |
. . . . . 6
⊢ (𝑐 = (𝑡↑2) → (∀𝑥 ∈ ℝ+ (𝑐 ≤ 𝑥 → 𝑡 ≤ (√‘𝑥)) ↔ ∀𝑥 ∈ ℝ+ ((𝑡↑2) ≤ 𝑥 → 𝑡 ≤ (√‘𝑥)))) |
127 | 126 | rspcev 3282 |
. . . . 5
⊢ (((𝑡↑2) ∈ ℝ ∧
∀𝑥 ∈
ℝ+ ((𝑡↑2) ≤ 𝑥 → 𝑡 ≤ (√‘𝑥))) → ∃𝑐 ∈ ℝ ∀𝑥 ∈ ℝ+ (𝑐 ≤ 𝑥 → 𝑡 ≤ (√‘𝑥))) |
128 | 97, 123, 127 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∃𝑐 ∈ ℝ ∀𝑥 ∈ ℝ+
(𝑐 ≤ 𝑥 → 𝑡 ≤ (√‘𝑥))) |
129 | 93, 86, 62, 95, 128 | o1compt 14166 |
. . 3
⊢ (𝜑 → ((𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∘ (𝑥 ∈ ℝ+ ↦
(√‘𝑥))) ∈
𝑂(1)) |
130 | 75, 129 | eqeltrd 2688 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑘 ∈
(1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘))) ∈ 𝑂(1)) |
131 | 1, 2, 3, 4, 5, 6, 7, 14, 15, 130 | dchrisum0fno1 25000 |
1
⊢ ¬
𝜑 |