Proof of Theorem dchrisum0lem1b
Step | Hyp | Ref
| Expression |
1 | | fzfid 12634 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑))) ∈ Fin) |
2 | | ssun2 3739 |
. . . . . . 7
⊢
(((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑))) ⊆ ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) |
3 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
4 | 3 | rprege0d 11755 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤
𝑥)) |
5 | | flge0nn0 12483 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘𝑥) ∈
ℕ0) |
7 | | nn0p1nn 11209 |
. . . . . . . . . . 11
⊢
((⌊‘𝑥)
∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ) |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘𝑥) + 1)
∈ ℕ) |
9 | 8 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((⌊‘𝑥) +
1) ∈ ℕ) |
10 | | nnuz 11599 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
11 | 9, 10 | syl6eleq 2698 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((⌊‘𝑥) +
1) ∈ (ℤ≥‘1)) |
12 | | dchrisum0lem1a 24975 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ≤ ((𝑥↑2) / 𝑑) ∧ (⌊‘((𝑥↑2) / 𝑑)) ∈
(ℤ≥‘(⌊‘𝑥)))) |
13 | 12 | simprd 478 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (⌊‘((𝑥↑2) / 𝑑)) ∈
(ℤ≥‘(⌊‘𝑥))) |
14 | | fzsplit2 12237 |
. . . . . . . 8
⊢
((((⌊‘𝑥)
+ 1) ∈ (ℤ≥‘1) ∧ (⌊‘((𝑥↑2) / 𝑑)) ∈
(ℤ≥‘(⌊‘𝑥))) → (1...(⌊‘((𝑥↑2) / 𝑑))) = ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))))) |
15 | 11, 13, 14 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1...(⌊‘((𝑥↑2) / 𝑑))) = ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))))) |
16 | 2, 15 | syl5sseqr 3617 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑))) ⊆ (1...(⌊‘((𝑥↑2) / 𝑑)))) |
17 | 16 | sselda 3568 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑚 ∈ (1...(⌊‘((𝑥↑2) / 𝑑)))) |
18 | | rpvmasum2.g |
. . . . . . 7
⊢ 𝐺 = (DChr‘𝑁) |
19 | | rpvmasum.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
20 | | rpvmasum2.d |
. . . . . . 7
⊢ 𝐷 = (Base‘𝐺) |
21 | | rpvmasum.l |
. . . . . . 7
⊢ 𝐿 = (ℤRHom‘𝑍) |
22 | | rpvmasum2.w |
. . . . . . . . . . 11
⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} |
23 | | ssrab2 3650 |
. . . . . . . . . . 11
⊢ {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} ⊆ (𝐷 ∖ { 1 }) |
24 | 22, 23 | eqsstri 3598 |
. . . . . . . . . 10
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
25 | | dchrisum0.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
26 | 24, 25 | sseldi 3566 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ (𝐷 ∖ { 1 })) |
27 | 26 | eldifad 3552 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
28 | 27 | ad3antrrr 762 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑋 ∈ 𝐷) |
29 | | elfzelz 12213 |
. . . . . . . 8
⊢ (𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑))) → 𝑚 ∈ ℤ) |
30 | 29 | adantl 481 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑚 ∈ ℤ) |
31 | 18, 19, 20, 21, 28, 30 | dchrzrhcl 24770 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
32 | | elfznn 12241 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑))) → 𝑚 ∈ ℕ) |
33 | 32 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑚 ∈ ℕ) |
34 | 33 | nnrpd 11746 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑚 ∈ ℝ+) |
35 | 34 | rpsqrtcld 13998 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → (√‘𝑚) ∈
ℝ+) |
36 | 35 | rpcnd 11750 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → (√‘𝑚) ∈ ℂ) |
37 | 35 | rpne0d 11753 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → (√‘𝑚) ≠ 0) |
38 | 31, 36, 37 | divcld 10680 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
39 | 17, 38 | syldan 486 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘((𝑥↑2) / 𝑑)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
40 | 1, 39 | fsumcl 14311 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
41 | 40 | abscld 14023 |
. 2
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘Σ𝑚
∈ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ∈ ℝ) |
42 | | 1zzd 11285 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℤ) |
43 | 27 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑋 ∈ 𝐷) |
44 | | nnz 11276 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℤ) |
45 | 44 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℤ) |
46 | 18, 19, 20, 21, 43, 45 | dchrzrhcl 24770 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
47 | | nnrp 11718 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ+) |
48 | 47 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+) |
49 | 48 | rpsqrtcld 13998 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (√‘𝑚) ∈
ℝ+) |
50 | 49 | rpcnd 11750 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (√‘𝑚) ∈
ℂ) |
51 | 49 | rpne0d 11753 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (√‘𝑚) ≠ 0) |
52 | 46, 50, 51 | divcld 10680 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
53 | | dchrisum0lem1.f |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) |
54 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑚 → (𝐿‘𝑎) = (𝐿‘𝑚)) |
55 | 54 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑚 → (𝑋‘(𝐿‘𝑎)) = (𝑋‘(𝐿‘𝑚))) |
56 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑚 → (√‘𝑎) = (√‘𝑚)) |
57 | 55, 56 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑚 → ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
58 | 57 | cbvmptv 4678 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) = (𝑚 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
59 | 53, 58 | eqtri 2632 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
60 | 52, 59 | fmptd 6292 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:ℕ⟶ℂ) |
61 | 60 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚) ∈ ℂ) |
62 | 10, 42, 61 | serf 12691 |
. . . . . . 7
⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ) |
63 | 62 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ seq1( + , 𝐹):ℕ⟶ℂ) |
64 | 3 | rpregt0d 11754 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 <
𝑥)) |
65 | 64 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
66 | 65 | simpld 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ) |
67 | | 1red 9934 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ) |
68 | | elfznn 12241 |
. . . . . . . . . . 11
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℕ) |
69 | 68 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℕ) |
70 | 69 | nnred 10912 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℝ) |
71 | 69 | nnge1d 10940 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 1 ≤ 𝑑) |
72 | 3 | rpred 11748 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ) |
73 | | fznnfl 12523 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → (𝑑 ∈
(1...(⌊‘𝑥))
↔ (𝑑 ∈ ℕ
∧ 𝑑 ≤ 𝑥))) |
74 | 72, 73 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑑 ∈
(1...(⌊‘𝑥))
↔ (𝑑 ∈ ℕ
∧ 𝑑 ≤ 𝑥))) |
75 | 74 | simplbda 652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ≤ 𝑥) |
76 | 67, 70, 66, 71, 75 | letrd 10073 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 1 ≤ 𝑥) |
77 | | flge1nn 12484 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ) |
78 | 66, 76, 77 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (⌊‘𝑥)
∈ ℕ) |
79 | | eluznn 11634 |
. . . . . . 7
⊢
(((⌊‘𝑥)
∈ ℕ ∧ (⌊‘((𝑥↑2) / 𝑑)) ∈
(ℤ≥‘(⌊‘𝑥))) → (⌊‘((𝑥↑2) / 𝑑)) ∈ ℕ) |
80 | 78, 13, 79 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (⌊‘((𝑥↑2) / 𝑑)) ∈ ℕ) |
81 | 63, 80 | ffvelrnd 6268 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) ∈ ℂ) |
82 | | dchrisum0.s |
. . . . . . 7
⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) |
83 | | climcl 14078 |
. . . . . . 7
⊢ (seq1( +
, 𝐹) ⇝ 𝑆 → 𝑆 ∈ ℂ) |
84 | 82, 83 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ ℂ) |
85 | 84 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑆 ∈
ℂ) |
86 | 81, 85 | subcld 10271 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆) ∈ ℂ) |
87 | 86 | abscld 14023 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) ∈ ℝ) |
88 | 63, 78 | ffvelrnd 6268 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (seq1( + , 𝐹)‘(⌊‘𝑥)) ∈ ℂ) |
89 | 85, 88 | subcld 10271 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑆 − (seq1( +
, 𝐹)‘(⌊‘𝑥))) ∈ ℂ) |
90 | 89 | abscld 14023 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑆
− (seq1( + , 𝐹)‘(⌊‘𝑥)))) ∈ ℝ) |
91 | 87, 90 | readdcld 9948 |
. 2
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) + (abs‘(𝑆 − (seq1( + , 𝐹)‘(⌊‘𝑥))))) ∈ ℝ) |
92 | | 2re 10967 |
. . . . . 6
⊢ 2 ∈
ℝ |
93 | | dchrisum0.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) |
94 | | elrege0 12149 |
. . . . . . . 8
⊢ (𝐶 ∈ (0[,)+∞) ↔
(𝐶 ∈ ℝ ∧ 0
≤ 𝐶)) |
95 | 93, 94 | sylib 207 |
. . . . . . 7
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) |
96 | 95 | simpld 474 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℝ) |
97 | | remulcl 9900 |
. . . . . 6
⊢ ((2
∈ ℝ ∧ 𝐶
∈ ℝ) → (2 · 𝐶) ∈ ℝ) |
98 | 92, 96, 97 | sylancr 694 |
. . . . 5
⊢ (𝜑 → (2 · 𝐶) ∈
ℝ) |
99 | 98 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2
· 𝐶) ∈
ℝ) |
100 | 3 | rpsqrtcld 13998 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℝ+) |
101 | 99, 100 | rerpdivcld 11779 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2
· 𝐶) /
(√‘𝑥)) ∈
ℝ) |
102 | 101 | adantr 480 |
. 2
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((2 · 𝐶) /
(√‘𝑥)) ∈
ℝ) |
103 | | ssun1 3738 |
. . . . . . . . . . 11
⊢
(1...(⌊‘𝑥)) ⊆ ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) |
104 | 103, 15 | syl5sseqr 3617 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1...(⌊‘𝑥)) ⊆ (1...(⌊‘((𝑥↑2) / 𝑑)))) |
105 | 104 | sselda 3568 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) |
106 | | ovex 6577 |
. . . . . . . . . . 11
⊢ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)) ∈ V |
107 | 57, 53, 106 | fvmpt3i 6196 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → (𝐹‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
108 | 33, 107 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → (𝐹‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
109 | 105, 108 | syldan 486 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝐹‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
110 | 78, 10 | syl6eleq 2698 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (⌊‘𝑥)
∈ (ℤ≥‘1)) |
111 | 105, 38 | syldan 486 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
112 | 109, 110,
111 | fsumser 14308 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) = (seq1( + , 𝐹)‘(⌊‘𝑥))) |
113 | 112, 88 | eqeltrd 2688 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
114 | 113, 40 | pncan2d 10273 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
115 | | reflcl 12459 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ∈
ℝ) |
116 | 66, 115 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (⌊‘𝑥)
∈ ℝ) |
117 | 116 | ltp1d 10833 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (⌊‘𝑥)
< ((⌊‘𝑥) +
1)) |
118 | | fzdisj 12239 |
. . . . . . . . 9
⊢
((⌊‘𝑥)
< ((⌊‘𝑥) +
1) → ((1...(⌊‘𝑥)) ∩ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) = ∅) |
119 | 117, 118 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((1...(⌊‘𝑥)) ∩ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) = ∅) |
120 | | fzfid 12634 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1...(⌊‘((𝑥↑2) / 𝑑))) ∈ Fin) |
121 | 119, 15, 120, 38 | fsumsplit 14318 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) = (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)))) |
122 | 80, 10 | syl6eleq 2698 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (⌊‘((𝑥↑2) / 𝑑)) ∈
(ℤ≥‘1)) |
123 | 108, 122,
38 | fsumser 14308 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) = (seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑)))) |
124 | 121, 123 | eqtr3d 2646 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = (seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑)))) |
125 | 124, 112 | oveq12d 6567 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = ((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − (seq1( + , 𝐹)‘(⌊‘𝑥)))) |
126 | 114, 125 | eqtr3d 2646 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) = ((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − (seq1( + , 𝐹)‘(⌊‘𝑥)))) |
127 | 126 | fveq2d 6107 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘Σ𝑚
∈ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = (abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − (seq1( + , 𝐹)‘(⌊‘𝑥))))) |
128 | 81, 88, 85 | abs3difd 14047 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − (seq1( + , 𝐹)‘(⌊‘𝑥)))) ≤ ((abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) + (abs‘(𝑆 − (seq1( + , 𝐹)‘(⌊‘𝑥)))))) |
129 | 127, 128 | eqbrtrd 4605 |
. 2
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘Σ𝑚
∈ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ≤ ((abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) + (abs‘(𝑆 − (seq1( + , 𝐹)‘(⌊‘𝑥)))))) |
130 | 96 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝐶 ∈
ℝ) |
131 | | simplr 788 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ+) |
132 | 131 | rpsqrtcld 13998 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑥)
∈ ℝ+) |
133 | 130, 132 | rerpdivcld 11779 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐶 /
(√‘𝑥)) ∈
ℝ) |
134 | | 2z 11286 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
135 | | rpexpcl 12741 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝑥↑2) ∈
ℝ+) |
136 | 3, 134, 135 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑2) ∈
ℝ+) |
137 | 136 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥↑2) ∈
ℝ+) |
138 | 69 | nnrpd 11746 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℝ+) |
139 | 137, 138 | rpdivcld 11765 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((𝑥↑2) / 𝑑) ∈
ℝ+) |
140 | 139 | rpsqrtcld 13998 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (√‘((𝑥↑2) / 𝑑)) ∈
ℝ+) |
141 | 130, 140 | rerpdivcld 11779 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐶 /
(√‘((𝑥↑2)
/ 𝑑))) ∈
ℝ) |
142 | 136 | rpred 11748 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑2) ∈
ℝ) |
143 | | nndivre 10933 |
. . . . . . . 8
⊢ (((𝑥↑2) ∈ ℝ ∧
𝑑 ∈ ℕ) →
((𝑥↑2) / 𝑑) ∈
ℝ) |
144 | 142, 68, 143 | syl2an 493 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((𝑥↑2) / 𝑑) ∈
ℝ) |
145 | 12 | simpld 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ≤ ((𝑥↑2) / 𝑑)) |
146 | 67, 66, 144, 76, 145 | letrd 10073 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 1 ≤ ((𝑥↑2) /
𝑑)) |
147 | | 1re 9918 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
148 | | elicopnf 12140 |
. . . . . . . 8
⊢ (1 ∈
ℝ → (((𝑥↑2)
/ 𝑑) ∈ (1[,)+∞)
↔ (((𝑥↑2) / 𝑑) ∈ ℝ ∧ 1 ≤
((𝑥↑2) / 𝑑)))) |
149 | 147, 148 | ax-mp 5 |
. . . . . . 7
⊢ (((𝑥↑2) / 𝑑) ∈ (1[,)+∞) ↔ (((𝑥↑2) / 𝑑) ∈ ℝ ∧ 1 ≤ ((𝑥↑2) / 𝑑))) |
150 | 144, 146,
149 | sylanbrc 695 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((𝑥↑2) / 𝑑) ∈
(1[,)+∞)) |
151 | | dchrisum0.1 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) |
152 | 151 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) |
153 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = ((𝑥↑2) / 𝑑) → (⌊‘𝑦) = (⌊‘((𝑥↑2) / 𝑑))) |
154 | 153 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑦 = ((𝑥↑2) / 𝑑) → (seq1( + , 𝐹)‘(⌊‘𝑦)) = (seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑)))) |
155 | 154 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑦 = ((𝑥↑2) / 𝑑) → ((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆) = ((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) |
156 | 155 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑦 = ((𝑥↑2) / 𝑑) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) = (abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆))) |
157 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑦 = ((𝑥↑2) / 𝑑) → (√‘𝑦) = (√‘((𝑥↑2) / 𝑑))) |
158 | 157 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑦 = ((𝑥↑2) / 𝑑) → (𝐶 / (√‘𝑦)) = (𝐶 / (√‘((𝑥↑2) / 𝑑)))) |
159 | 156, 158 | breq12d 4596 |
. . . . . . 7
⊢ (𝑦 = ((𝑥↑2) / 𝑑) → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦)) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) ≤ (𝐶 / (√‘((𝑥↑2) / 𝑑))))) |
160 | 159 | rspcv 3278 |
. . . . . 6
⊢ (((𝑥↑2) / 𝑑) ∈ (1[,)+∞) → (∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦)) → (abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) ≤ (𝐶 / (√‘((𝑥↑2) / 𝑑))))) |
161 | 150, 152,
160 | sylc 63 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) ≤ (𝐶 / (√‘((𝑥↑2) / 𝑑)))) |
162 | 132 | rpregt0d 11754 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑥)
∈ ℝ ∧ 0 < (√‘𝑥))) |
163 | 140 | rpregt0d 11754 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((√‘((𝑥↑2) / 𝑑)) ∈ ℝ ∧ 0 <
(√‘((𝑥↑2)
/ 𝑑)))) |
164 | 95 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐶 ∈ ℝ
∧ 0 ≤ 𝐶)) |
165 | 131 | rprege0d 11755 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
166 | 139 | rprege0d 11755 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (((𝑥↑2) / 𝑑) ∈ ℝ ∧ 0 ≤
((𝑥↑2) / 𝑑))) |
167 | | sqrtle 13849 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) ∧ (((𝑥↑2) / 𝑑) ∈ ℝ ∧ 0 ≤ ((𝑥↑2) / 𝑑))) → (𝑥 ≤ ((𝑥↑2) / 𝑑) ↔ (√‘𝑥) ≤ (√‘((𝑥↑2) / 𝑑)))) |
168 | 165, 166,
167 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ≤ ((𝑥↑2) / 𝑑) ↔ (√‘𝑥) ≤ (√‘((𝑥↑2) / 𝑑)))) |
169 | 145, 168 | mpbid 221 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑥)
≤ (√‘((𝑥↑2) / 𝑑))) |
170 | | lediv2a 10796 |
. . . . . 6
⊢
(((((√‘𝑥) ∈ ℝ ∧ 0 <
(√‘𝑥)) ∧
((√‘((𝑥↑2)
/ 𝑑)) ∈ ℝ ∧
0 < (√‘((𝑥↑2) / 𝑑))) ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ (√‘𝑥) ≤ (√‘((𝑥↑2) / 𝑑))) → (𝐶 / (√‘((𝑥↑2) / 𝑑))) ≤ (𝐶 / (√‘𝑥))) |
171 | 162, 163,
164, 169, 170 | syl31anc 1321 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐶 /
(√‘((𝑥↑2)
/ 𝑑))) ≤ (𝐶 / (√‘𝑥))) |
172 | 87, 141, 133, 161, 171 | letrd 10073 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) ≤ (𝐶 / (√‘𝑥))) |
173 | 85, 88 | abssubd 14040 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑆
− (seq1( + , 𝐹)‘(⌊‘𝑥)))) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑆))) |
174 | | elicopnf 12140 |
. . . . . . . 8
⊢ (1 ∈
ℝ → (𝑥 ∈
(1[,)+∞) ↔ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥))) |
175 | 147, 174 | ax-mp 5 |
. . . . . . 7
⊢ (𝑥 ∈ (1[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 1
≤ 𝑥)) |
176 | 66, 76, 175 | sylanbrc 695 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
(1[,)+∞)) |
177 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (⌊‘𝑦) = (⌊‘𝑥)) |
178 | 177 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (seq1( + , 𝐹)‘(⌊‘𝑦)) = (seq1( + , 𝐹)‘(⌊‘𝑥))) |
179 | 178 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆) = ((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑆)) |
180 | 179 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑆))) |
181 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (√‘𝑦) = (√‘𝑥)) |
182 | 181 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝐶 / (√‘𝑦)) = (𝐶 / (√‘𝑥))) |
183 | 180, 182 | breq12d 4596 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦)) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑆)) ≤ (𝐶 / (√‘𝑥)))) |
184 | 183 | rspcv 3278 |
. . . . . 6
⊢ (𝑥 ∈ (1[,)+∞) →
(∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦)) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑆)) ≤ (𝐶 / (√‘𝑥)))) |
185 | 176, 152,
184 | sylc 63 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑆)) ≤ (𝐶 / (√‘𝑥))) |
186 | 173, 185 | eqbrtrd 4605 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑆
− (seq1( + , 𝐹)‘(⌊‘𝑥)))) ≤ (𝐶 / (√‘𝑥))) |
187 | 87, 90, 133, 133, 172, 186 | le2addd 10525 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) + (abs‘(𝑆 − (seq1( + , 𝐹)‘(⌊‘𝑥))))) ≤ ((𝐶 / (√‘𝑥)) + (𝐶 / (√‘𝑥)))) |
188 | | 2cnd 10970 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 2 ∈ ℂ) |
189 | 96 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈
ℝ) |
190 | 189 | recnd 9947 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈
ℂ) |
191 | 190 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝐶 ∈
ℂ) |
192 | 100 | rpcnne0d 11757 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((√‘𝑥) ∈
ℂ ∧ (√‘𝑥) ≠ 0)) |
193 | 192 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑥)
∈ ℂ ∧ (√‘𝑥) ≠ 0)) |
194 | | divass 10582 |
. . . . 5
⊢ ((2
∈ ℂ ∧ 𝐶
∈ ℂ ∧ ((√‘𝑥) ∈ ℂ ∧ (√‘𝑥) ≠ 0)) → ((2 ·
𝐶) / (√‘𝑥)) = (2 · (𝐶 / (√‘𝑥)))) |
195 | 188, 191,
193, 194 | syl3anc 1318 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((2 · 𝐶) /
(√‘𝑥)) = (2
· (𝐶 /
(√‘𝑥)))) |
196 | 133 | recnd 9947 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐶 /
(√‘𝑥)) ∈
ℂ) |
197 | 196 | 2timesd 11152 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (2 · (𝐶 /
(√‘𝑥))) =
((𝐶 / (√‘𝑥)) + (𝐶 / (√‘𝑥)))) |
198 | 195, 197 | eqtrd 2644 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((2 · 𝐶) /
(√‘𝑥)) =
((𝐶 / (√‘𝑥)) + (𝐶 / (√‘𝑥)))) |
199 | 187, 198 | breqtrrd 4611 |
. 2
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) + (abs‘(𝑆 − (seq1( + , 𝐹)‘(⌊‘𝑥))))) ≤ ((2 · 𝐶) / (√‘𝑥))) |
200 | 41, 91, 102, 129, 199 | letrd 10073 |
1
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘Σ𝑚
∈ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ≤ ((2 · 𝐶) / (√‘𝑥))) |