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 2737 |
. 2
⊢ (𝑏 ∈ ℕ ↦
Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦))) = (𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦))) |
8 | | rpvmasum2.w |
. . . . 5
⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} |
9 | 8 | ssrab3 3995 |
. . . 4
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
10 | | difss 4046 |
. . . 4
⊢ (𝐷 ∖ { 1 }) ⊆ 𝐷 |
11 | 9, 10 | sstri 3910 |
. . 3
⊢ 𝑊 ⊆ 𝐷 |
12 | | dchrisum0.b |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
13 | 11, 12 | sseldi 3899 |
. 2
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
14 | 1, 2, 3, 4, 5, 6, 8, 12 | dchrisum0re 26394 |
. 2
⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) |
15 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑘 = (𝑚 · 𝑑) → (√‘𝑘) = (√‘(𝑚 · 𝑑))) |
16 | 15 | oveq2d 7229 |
. . . . . . 7
⊢ (𝑘 = (𝑚 · 𝑑) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘)) = ((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
17 | | rpre 12594 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
18 | 17 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ) |
19 | 13 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → 𝑋 ∈ 𝐷) |
20 | | elrabi 3596 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} → 𝑚 ∈ ℕ) |
21 | 20 | nnzd 12281 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} → 𝑚 ∈ ℤ) |
22 | 21 | adantl 485 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → 𝑚 ∈ ℤ) |
23 | 4, 1, 5, 2, 19, 22 | dchrzrhcl 26126 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
24 | | elfznn 13141 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(1...(⌊‘𝑥))
→ 𝑘 ∈
ℕ) |
25 | 24 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ 𝑘 ∈
ℕ) |
26 | 25 | nnrpd 12626 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ 𝑘 ∈
ℝ+) |
27 | 26 | rpsqrtcld 14975 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑘)
∈ ℝ+) |
28 | 27 | rpcnd 12630 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑘)
∈ ℂ) |
29 | 28 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → (√‘𝑘) ∈ ℂ) |
30 | 27 | rpne0d 12633 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑘)
≠ 0) |
31 | 30 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → (√‘𝑘) ≠ 0) |
32 | 23, 29, 31 | divcld 11608 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘)) ∈ ℂ) |
33 | 32 | anasss 470 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘})) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘)) ∈ ℂ) |
34 | 16, 18, 33 | dvdsflsumcom 26070 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘)) = Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
35 | 1, 2, 3, 4, 5, 6, 7 | dchrisum0fval 26386 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → ((𝑏 ∈ ℕ ↦
Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) = Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} (𝑋‘(𝐿‘𝑚))) |
36 | 25, 35 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ ((𝑏 ∈ ℕ
↦ Σ𝑦 ∈
{𝑖 ∈ ℕ ∣
𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) = Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} (𝑋‘(𝐿‘𝑚))) |
37 | 36 | oveq1d 7228 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (((𝑏 ∈ ℕ
↦ Σ𝑦 ∈
{𝑖 ∈ ℕ ∣
𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘)) = (Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} (𝑋‘(𝐿‘𝑚)) / (√‘𝑘))) |
38 | | fzfid 13546 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (1...𝑘) ∈
Fin) |
39 | | dvdsssfz1 15879 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} ⊆ (1...𝑘)) |
40 | 25, 39 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ {𝑖 ∈ ℕ
∣ 𝑖 ∥ 𝑘} ⊆ (1...𝑘)) |
41 | 38, 40 | ssfid 8898 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ {𝑖 ∈ ℕ
∣ 𝑖 ∥ 𝑘} ∈ Fin) |
42 | 41, 28, 23, 30 | fsumdivc 15350 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
{𝑖 ∈ ℕ ∣
𝑖 ∥ 𝑘} (𝑋‘(𝐿‘𝑚)) / (√‘𝑘)) = Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘))) |
43 | 37, 42 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (((𝑏 ∈ ℕ
↦ Σ𝑦 ∈
{𝑖 ∈ ℕ ∣
𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘)) = Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘))) |
44 | 43 | sumeq2dv 15267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈
(1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘)) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘))) |
45 | | rprege0 12601 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
46 | 45 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤
𝑥)) |
47 | | resqrtth 14819 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
((√‘𝑥)↑2)
= 𝑥) |
48 | 46, 47 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((√‘𝑥)↑2)
= 𝑥) |
49 | 48 | fveq2d 6721 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘((√‘𝑥)↑2)) = (⌊‘𝑥)) |
50 | 49 | oveq2d 7229 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘((√‘𝑥)↑2))) = (1...(⌊‘𝑥))) |
51 | 48 | fvoveq1d 7235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘(((√‘𝑥)↑2) / 𝑚)) = (⌊‘(𝑥 / 𝑚))) |
52 | 51 | oveq2d 7229 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚))) = (1...(⌊‘(𝑥 / 𝑚)))) |
53 | 52 | sumeq1d 15265 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
54 | 53 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))) → Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
55 | 50, 54 | sumeq12dv 15270 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
56 | 34, 44, 55 | 3eqtr4d 2787 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈
(1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘)) = Σ𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
57 | 56 | mpteq2dva 5150 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑘 ∈
(1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘))) = (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))))) |
58 | | rpsqrtcl 14828 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (√‘𝑥)
∈ ℝ+) |
59 | 58 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℝ+) |
60 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(√‘𝑥)) = (𝑥 ∈ ℝ+
↦ (√‘𝑥))) |
61 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) = (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))))) |
62 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑧 = (√‘𝑥) → (𝑧↑2) = ((√‘𝑥)↑2)) |
63 | 62 | fveq2d 6721 |
. . . . . . 7
⊢ (𝑧 = (√‘𝑥) → (⌊‘(𝑧↑2)) =
(⌊‘((√‘𝑥)↑2))) |
64 | 63 | oveq2d 7229 |
. . . . . 6
⊢ (𝑧 = (√‘𝑥) →
(1...(⌊‘(𝑧↑2))) =
(1...(⌊‘((√‘𝑥)↑2)))) |
65 | 62 | fvoveq1d 7235 |
. . . . . . . . 9
⊢ (𝑧 = (√‘𝑥) → (⌊‘((𝑧↑2) / 𝑚)) = (⌊‘(((√‘𝑥)↑2) / 𝑚))) |
66 | 65 | oveq2d 7229 |
. . . . . . . 8
⊢ (𝑧 = (√‘𝑥) →
(1...(⌊‘((𝑧↑2) / 𝑚))) =
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))) |
67 | 66 | sumeq1d 15265 |
. . . . . . 7
⊢ (𝑧 = (√‘𝑥) → Σ𝑑 ∈
(1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
68 | 67 | adantr 484 |
. . . . . 6
⊢ ((𝑧 = (√‘𝑥) ∧ 𝑚 ∈ (1...(⌊‘(𝑧↑2)))) → Σ𝑑 ∈
(1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
69 | 64, 68 | sumeq12dv 15270 |
. . . . 5
⊢ (𝑧 = (√‘𝑥) → Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
70 | 59, 60, 61, 69 | fmptco 6944 |
. . . 4
⊢ (𝜑 → ((𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∘ (𝑥 ∈ ℝ+ ↦
(√‘𝑥))) =
(𝑥 ∈
ℝ+ ↦ Σ𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))))) |
71 | 57, 70 | eqtr4d 2780 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑘 ∈
(1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘))) = ((𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∘ (𝑥 ∈ ℝ+ ↦
(√‘𝑥)))) |
72 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) |
73 | 1, 2, 3, 4, 5, 6, 8, 12, 72 | dchrisum0lema 26395 |
. . . . . . 7
⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦)))) |
74 | 3 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → 𝑁 ∈ ℕ) |
75 | 12 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → 𝑋 ∈ 𝑊) |
76 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → 𝑐 ∈ (0[,)+∞)) |
77 | | simprrl 781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡) |
78 | | simprrr 782 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))) |
79 | 1, 2, 74, 4, 5, 6,
8, 75, 72, 76, 77, 78 | dchrisum0lem3 26400 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1)) |
80 | 79 | rexlimdvaa 3204 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))) → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1))) |
81 | 80 | exlimdv 1941 |
. . . . . . 7
⊢ (𝜑 → (∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))) → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1))) |
82 | 73, 81 | mpd 15 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1)) |
83 | | o1f 15090 |
. . . . . 6
⊢ ((𝑧 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1) → (𝑧 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))):dom (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))))⟶ℂ) |
84 | 82, 83 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))):dom (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))))⟶ℂ) |
85 | | sumex 15251 |
. . . . . . 7
⊢
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) ∈ V |
86 | | eqid 2737 |
. . . . . . 7
⊢ (𝑧 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) = (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
87 | 85, 86 | dmmpti 6522 |
. . . . . 6
⊢ dom
(𝑧 ∈
ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈
(1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) = ℝ+ |
88 | 87 | feq2i 6537 |
. . . . 5
⊢ ((𝑧 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))):dom (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))))⟶ℂ ↔ (𝑧 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))):ℝ+⟶ℂ) |
89 | 84, 88 | sylib 221 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))):ℝ+⟶ℂ) |
90 | | rpssre 12593 |
. . . . 5
⊢
ℝ+ ⊆ ℝ |
91 | 90 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ+
⊆ ℝ) |
92 | | resqcl 13696 |
. . . . 5
⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈
ℝ) |
93 | | 0red 10836 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → 0 ∈ ℝ) |
94 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → 𝑡 ∈ ℝ) |
95 | | simplrr 778 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (𝑡↑2) ≤ 𝑥) |
96 | 45 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) |
97 | 96 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) |
98 | 97, 47 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → ((√‘𝑥)↑2) = 𝑥) |
99 | 95, 98 | breqtrrd 5081 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (𝑡↑2) ≤ ((√‘𝑥)↑2)) |
100 | 94 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → 𝑡 ∈ ℝ) |
101 | 59 | rpred 12628 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℝ) |
102 | 101 | ad2ant2r 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → (√‘𝑥) ∈ ℝ) |
103 | 102 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (√‘𝑥) ∈ ℝ) |
104 | | simpr 488 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → 0 ≤ 𝑡) |
105 | | sqrtge0 14821 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) → 0 ≤
(√‘𝑥)) |
106 | 96, 105 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → 0 ≤ (√‘𝑥)) |
107 | 106 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → 0 ≤ (√‘𝑥)) |
108 | 100, 103,
104, 107 | le2sqd 13826 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (𝑡 ≤ (√‘𝑥) ↔ (𝑡↑2) ≤ ((√‘𝑥)↑2))) |
109 | 99, 108 | mpbird 260 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → 𝑡 ≤ (√‘𝑥)) |
110 | 94 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 𝑡 ∈ ℝ) |
111 | | 0red 10836 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 0 ∈
ℝ) |
112 | 102 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → (√‘𝑥) ∈
ℝ) |
113 | | simpr 488 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 𝑡 ≤ 0) |
114 | 106 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 0 ≤ (√‘𝑥)) |
115 | 110, 111,
112, 113, 114 | letrd 10989 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 𝑡 ≤ (√‘𝑥)) |
116 | 93, 94, 109, 115 | lecasei 10938 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → 𝑡 ≤ (√‘𝑥)) |
117 | 116 | expr 460 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → ((𝑡↑2) ≤ 𝑥 → 𝑡 ≤ (√‘𝑥))) |
118 | 117 | ralrimiva 3105 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∀𝑥 ∈ ℝ+
((𝑡↑2) ≤ 𝑥 → 𝑡 ≤ (√‘𝑥))) |
119 | | breq1 5056 |
. . . . . 6
⊢ (𝑐 = (𝑡↑2) → (𝑐 ≤ 𝑥 ↔ (𝑡↑2) ≤ 𝑥)) |
120 | 119 | rspceaimv 3542 |
. . . . 5
⊢ (((𝑡↑2) ∈ ℝ ∧
∀𝑥 ∈
ℝ+ ((𝑡↑2) ≤ 𝑥 → 𝑡 ≤ (√‘𝑥))) → ∃𝑐 ∈ ℝ ∀𝑥 ∈ ℝ+ (𝑐 ≤ 𝑥 → 𝑡 ≤ (√‘𝑥))) |
121 | 92, 118, 120 | syl2an2 686 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∃𝑐 ∈ ℝ ∀𝑥 ∈ ℝ+
(𝑐 ≤ 𝑥 → 𝑡 ≤ (√‘𝑥))) |
122 | 89, 82, 59, 91, 121 | o1compt 15148 |
. . 3
⊢ (𝜑 → ((𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∘ (𝑥 ∈ ℝ+ ↦
(√‘𝑥))) ∈
𝑂(1)) |
123 | 71, 122 | eqeltrd 2838 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑘 ∈
(1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘))) ∈ 𝑂(1)) |
124 | 1, 2, 3, 4, 5, 6, 7, 13, 14, 123 | dchrisum0fno1 26392 |
1
⊢ ¬
𝜑 |