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 2740 |
. 2
⊢ (𝑏 ∈ ℕ ↦
Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦))) = (𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦))) |
8 | | rpvmasum2.w |
. . . . 5
⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} |
9 | 8 | ssrab3 4020 |
. . . 4
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
10 | | difss 4071 |
. . . 4
⊢ (𝐷 ∖ { 1 }) ⊆ 𝐷 |
11 | 9, 10 | sstri 3935 |
. . 3
⊢ 𝑊 ⊆ 𝐷 |
12 | | dchrisum0.b |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
13 | 11, 12 | sselid 3924 |
. 2
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
14 | 1, 2, 3, 4, 5, 6, 8, 12 | dchrisum0re 26659 |
. 2
⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) |
15 | | fveq2 6771 |
. . . . . . . 8
⊢ (𝑘 = (𝑚 · 𝑑) → (√‘𝑘) = (√‘(𝑚 · 𝑑))) |
16 | 15 | oveq2d 7287 |
. . . . . . 7
⊢ (𝑘 = (𝑚 · 𝑑) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘)) = ((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
17 | | rpre 12737 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
18 | 17 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ) |
19 | 13 | ad3antrrr 727 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → 𝑋 ∈ 𝐷) |
20 | | elrabi 3620 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} → 𝑚 ∈ ℕ) |
21 | 20 | nnzd 12424 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} → 𝑚 ∈ ℤ) |
22 | 21 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → 𝑚 ∈ ℤ) |
23 | 4, 1, 5, 2, 19, 22 | dchrzrhcl 26391 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
24 | | elfznn 13284 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(1...(⌊‘𝑥))
→ 𝑘 ∈
ℕ) |
25 | 24 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ 𝑘 ∈
ℕ) |
26 | 25 | nnrpd 12769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ 𝑘 ∈
ℝ+) |
27 | 26 | rpsqrtcld 15121 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑘)
∈ ℝ+) |
28 | 27 | rpcnd 12773 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑘)
∈ ℂ) |
29 | 28 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → (√‘𝑘) ∈ ℂ) |
30 | 27 | rpne0d 12776 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑘)
≠ 0) |
31 | 30 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → (√‘𝑘) ≠ 0) |
32 | 23, 29, 31 | divcld 11751 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘}) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘)) ∈ ℂ) |
33 | 32 | anasss 467 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘})) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘)) ∈ ℂ) |
34 | 16, 18, 33 | dvdsflsumcom 26335 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘)) = Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
35 | 1, 2, 3, 4, 5, 6, 7 | dchrisum0fval 26651 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → ((𝑏 ∈ ℕ ↦
Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) = Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} (𝑋‘(𝐿‘𝑚))) |
36 | 25, 35 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ ((𝑏 ∈ ℕ
↦ Σ𝑦 ∈
{𝑖 ∈ ℕ ∣
𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) = Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} (𝑋‘(𝐿‘𝑚))) |
37 | 36 | oveq1d 7286 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (((𝑏 ∈ ℕ
↦ Σ𝑦 ∈
{𝑖 ∈ ℕ ∣
𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘)) = (Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} (𝑋‘(𝐿‘𝑚)) / (√‘𝑘))) |
38 | | fzfid 13691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (1...𝑘) ∈
Fin) |
39 | | dvdsssfz1 16025 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} ⊆ (1...𝑘)) |
40 | 25, 39 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ {𝑖 ∈ ℕ
∣ 𝑖 ∥ 𝑘} ⊆ (1...𝑘)) |
41 | 38, 40 | ssfid 9020 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ {𝑖 ∈ ℕ
∣ 𝑖 ∥ 𝑘} ∈ Fin) |
42 | 41, 28, 23, 30 | fsumdivc 15496 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
{𝑖 ∈ ℕ ∣
𝑖 ∥ 𝑘} (𝑋‘(𝐿‘𝑚)) / (√‘𝑘)) = Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘))) |
43 | 37, 42 | eqtrd 2780 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (((𝑏 ∈ ℕ
↦ Σ𝑦 ∈
{𝑖 ∈ ℕ ∣
𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘)) = Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘))) |
44 | 43 | sumeq2dv 15413 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈
(1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘)) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑘} ((𝑋‘(𝐿‘𝑚)) / (√‘𝑘))) |
45 | | rprege0 12744 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
46 | 45 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤
𝑥)) |
47 | | resqrtth 14965 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
((√‘𝑥)↑2)
= 𝑥) |
48 | 46, 47 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((√‘𝑥)↑2)
= 𝑥) |
49 | 48 | fveq2d 6775 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘((√‘𝑥)↑2)) = (⌊‘𝑥)) |
50 | 49 | oveq2d 7287 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘((√‘𝑥)↑2))) = (1...(⌊‘𝑥))) |
51 | 48 | fvoveq1d 7293 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘(((√‘𝑥)↑2) / 𝑚)) = (⌊‘(𝑥 / 𝑚))) |
52 | 51 | oveq2d 7287 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚))) = (1...(⌊‘(𝑥 / 𝑚)))) |
53 | 52 | sumeq1d 15411 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
54 | 53 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))) → Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
55 | 50, 54 | sumeq12dv 15416 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
56 | 34, 44, 55 | 3eqtr4d 2790 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈
(1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘)) = Σ𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
57 | 56 | mpteq2dva 5179 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑘 ∈
(1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘))) = (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))))) |
58 | | rpsqrtcl 14974 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (√‘𝑥)
∈ ℝ+) |
59 | 58 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℝ+) |
60 | | eqidd 2741 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(√‘𝑥)) = (𝑥 ∈ ℝ+
↦ (√‘𝑥))) |
61 | | eqidd 2741 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) = (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))))) |
62 | | oveq1 7278 |
. . . . . . . 8
⊢ (𝑧 = (√‘𝑥) → (𝑧↑2) = ((√‘𝑥)↑2)) |
63 | 62 | fveq2d 6775 |
. . . . . . 7
⊢ (𝑧 = (√‘𝑥) → (⌊‘(𝑧↑2)) =
(⌊‘((√‘𝑥)↑2))) |
64 | 63 | oveq2d 7287 |
. . . . . 6
⊢ (𝑧 = (√‘𝑥) →
(1...(⌊‘(𝑧↑2))) =
(1...(⌊‘((√‘𝑥)↑2)))) |
65 | 62 | fvoveq1d 7293 |
. . . . . . . . 9
⊢ (𝑧 = (√‘𝑥) → (⌊‘((𝑧↑2) / 𝑚)) = (⌊‘(((√‘𝑥)↑2) / 𝑚))) |
66 | 65 | oveq2d 7287 |
. . . . . . . 8
⊢ (𝑧 = (√‘𝑥) →
(1...(⌊‘((𝑧↑2) / 𝑚))) =
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))) |
67 | 66 | sumeq1d 15411 |
. . . . . . 7
⊢ (𝑧 = (√‘𝑥) → Σ𝑑 ∈
(1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
68 | 67 | adantr 481 |
. . . . . 6
⊢ ((𝑧 = (√‘𝑥) ∧ 𝑚 ∈ (1...(⌊‘(𝑧↑2)))) → Σ𝑑 ∈
(1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
69 | 64, 68 | sumeq12dv 15416 |
. . . . 5
⊢ (𝑧 = (√‘𝑥) → Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
70 | 59, 60, 61, 69 | fmptco 6998 |
. . . 4
⊢ (𝜑 → ((𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∘ (𝑥 ∈ ℝ+ ↦
(√‘𝑥))) =
(𝑥 ∈
ℝ+ ↦ Σ𝑚 ∈
(1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈
(1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))))) |
71 | 57, 70 | eqtr4d 2783 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑘 ∈
(1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘))) = ((𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∘ (𝑥 ∈ ℝ+ ↦
(√‘𝑥)))) |
72 | | eqid 2740 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) |
73 | 1, 2, 3, 4, 5, 6, 8, 12, 72 | dchrisum0lema 26660 |
. . . . . . 7
⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦)))) |
74 | 3 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → 𝑁 ∈ ℕ) |
75 | 12 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → 𝑋 ∈ 𝑊) |
76 | | simprl 768 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → 𝑐 ∈ (0[,)+∞)) |
77 | | simprrl 778 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡) |
78 | | simprrr 779 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))) |
79 | 1, 2, 74, 4, 5, 6,
8, 75, 72, 76, 77, 78 | dchrisum0lem3 26665 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1)) |
80 | 79 | rexlimdvaa 3216 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))) → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1))) |
81 | 80 | exlimdv 1940 |
. . . . . . 7
⊢ (𝜑 → (∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))) → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1))) |
82 | 73, 81 | mpd 15 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1)) |
83 | | o1f 15236 |
. . . . . 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 15397 |
. . . . . . 7
⊢
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) ∈ V |
86 | | eqid 2740 |
. . . . . . 7
⊢ (𝑧 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) = (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) |
87 | 85, 86 | dmmpti 6575 |
. . . . . 6
⊢ dom
(𝑧 ∈
ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈
(1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) = ℝ+ |
88 | 87 | feq2i 6590 |
. . . . 5
⊢ ((𝑧 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))):dom (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))))⟶ℂ ↔ (𝑧 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))):ℝ+⟶ℂ) |
89 | 84, 88 | sylib 217 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))):ℝ+⟶ℂ) |
90 | | rpssre 12736 |
. . . . 5
⊢
ℝ+ ⊆ ℝ |
91 | 90 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ+
⊆ ℝ) |
92 | | resqcl 13842 |
. . . . 5
⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈
ℝ) |
93 | | 0red 10979 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → 0 ∈ ℝ) |
94 | | simplr 766 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → 𝑡 ∈ ℝ) |
95 | | simplrr 775 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (𝑡↑2) ≤ 𝑥) |
96 | 45 | ad2antrl 725 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) |
97 | 96 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) |
98 | 97, 47 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → ((√‘𝑥)↑2) = 𝑥) |
99 | 95, 98 | breqtrrd 5107 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (𝑡↑2) ≤ ((√‘𝑥)↑2)) |
100 | 94 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → 𝑡 ∈ ℝ) |
101 | 59 | rpred 12771 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℝ) |
102 | 101 | ad2ant2r 744 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → (√‘𝑥) ∈ ℝ) |
103 | 102 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (√‘𝑥) ∈ ℝ) |
104 | | simpr 485 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → 0 ≤ 𝑡) |
105 | | sqrtge0 14967 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) → 0 ≤
(√‘𝑥)) |
106 | 96, 105 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → 0 ≤ (√‘𝑥)) |
107 | 106 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → 0 ≤ (√‘𝑥)) |
108 | 100, 103,
104, 107 | le2sqd 13972 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (𝑡 ≤ (√‘𝑥) ↔ (𝑡↑2) ≤ ((√‘𝑥)↑2))) |
109 | 99, 108 | mpbird 256 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → 𝑡 ≤ (√‘𝑥)) |
110 | 94 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 𝑡 ∈ ℝ) |
111 | | 0red 10979 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 0 ∈
ℝ) |
112 | 102 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → (√‘𝑥) ∈
ℝ) |
113 | | simpr 485 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 𝑡 ≤ 0) |
114 | 106 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 0 ≤ (√‘𝑥)) |
115 | 110, 111,
112, 113, 114 | letrd 11132 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 𝑡 ≤ (√‘𝑥)) |
116 | 93, 94, 109, 115 | lecasei 11081 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → 𝑡 ≤ (√‘𝑥)) |
117 | 116 | expr 457 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → ((𝑡↑2) ≤ 𝑥 → 𝑡 ≤ (√‘𝑥))) |
118 | 117 | ralrimiva 3110 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∀𝑥 ∈ ℝ+
((𝑡↑2) ≤ 𝑥 → 𝑡 ≤ (√‘𝑥))) |
119 | | breq1 5082 |
. . . . . 6
⊢ (𝑐 = (𝑡↑2) → (𝑐 ≤ 𝑥 ↔ (𝑡↑2) ≤ 𝑥)) |
120 | 119 | rspceaimv 3566 |
. . . . 5
⊢ (((𝑡↑2) ∈ ℝ ∧
∀𝑥 ∈
ℝ+ ((𝑡↑2) ≤ 𝑥 → 𝑡 ≤ (√‘𝑥))) → ∃𝑐 ∈ ℝ ∀𝑥 ∈ ℝ+ (𝑐 ≤ 𝑥 → 𝑡 ≤ (√‘𝑥))) |
121 | 92, 118, 120 | syl2an2 683 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → ∃𝑐 ∈ ℝ ∀𝑥 ∈ ℝ+
(𝑐 ≤ 𝑥 → 𝑡 ≤ (√‘𝑥))) |
122 | 89, 82, 59, 91, 121 | o1compt 15294 |
. . 3
⊢ (𝜑 → ((𝑧 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∘ (𝑥 ∈ ℝ+ ↦
(√‘𝑥))) ∈
𝑂(1)) |
123 | 71, 122 | eqeltrd 2841 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑘 ∈
(1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖 ∥ 𝑏} (𝑋‘(𝐿‘𝑦)))‘𝑘) / (√‘𝑘))) ∈ 𝑂(1)) |
124 | 1, 2, 3, 4, 5, 6, 7, 13, 14, 123 | dchrisum0fno1 26657 |
1
⊢ ¬
𝜑 |