Proof of Theorem dchrisum0lem1b
| Step | Hyp | Ref
| Expression |
| 1 | | fzfid 14014 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑))) ∈ Fin) |
| 2 | | ssun2 4179 |
. . . . . . 7
⊢
(((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑))) ⊆ ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) |
| 3 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
| 4 | 3 | rprege0d 13084 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤
𝑥)) |
| 5 | | flge0nn0 13860 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
| 6 | 4, 5 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘𝑥) ∈
ℕ0) |
| 7 | | nn0p1nn 12565 |
. . . . . . . . . . 11
⊢
((⌊‘𝑥)
∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ) |
| 8 | 6, 7 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘𝑥) + 1)
∈ ℕ) |
| 9 | 8 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((⌊‘𝑥) +
1) ∈ ℕ) |
| 10 | | nnuz 12921 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
| 11 | 9, 10 | eleqtrdi 2851 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((⌊‘𝑥) +
1) ∈ (ℤ≥‘1)) |
| 12 | | dchrisum0lem1a 27530 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ≤ ((𝑥↑2) / 𝑑) ∧ (⌊‘((𝑥↑2) / 𝑑)) ∈
(ℤ≥‘(⌊‘𝑥)))) |
| 13 | 12 | simprd 495 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (⌊‘((𝑥↑2) / 𝑑)) ∈
(ℤ≥‘(⌊‘𝑥))) |
| 14 | | fzsplit2 13589 |
. . . . . . . 8
⊢
((((⌊‘𝑥)
+ 1) ∈ (ℤ≥‘1) ∧ (⌊‘((𝑥↑2) / 𝑑)) ∈
(ℤ≥‘(⌊‘𝑥))) → (1...(⌊‘((𝑥↑2) / 𝑑))) = ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))))) |
| 15 | 11, 13, 14 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1...(⌊‘((𝑥↑2) / 𝑑))) = ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))))) |
| 16 | 2, 15 | sseqtrrid 4027 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑))) ⊆ (1...(⌊‘((𝑥↑2) / 𝑑)))) |
| 17 | 16 | sselda 3983 |
. . . . 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 | 22 | ssrab3 4082 |
. . . . . . . . . 10
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
| 24 | | dchrisum0.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
| 25 | 23, 24 | sselid 3981 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ (𝐷 ∖ { 1 })) |
| 26 | 25 | eldifad 3963 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
| 27 | 26 | ad3antrrr 730 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑋 ∈ 𝐷) |
| 28 | | elfzelz 13564 |
. . . . . . . 8
⊢ (𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑))) → 𝑚 ∈ ℤ) |
| 29 | 28 | adantl 481 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑚 ∈ ℤ) |
| 30 | 18, 19, 20, 21, 27, 29 | dchrzrhcl 27289 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
| 31 | | elfznn 13593 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑))) → 𝑚 ∈ ℕ) |
| 32 | 31 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑚 ∈ ℕ) |
| 33 | 32 | nnrpd 13075 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑚 ∈ ℝ+) |
| 34 | 33 | rpsqrtcld 15450 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → (√‘𝑚) ∈
ℝ+) |
| 35 | 34 | rpcnd 13079 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → (√‘𝑚) ∈ ℂ) |
| 36 | 34 | rpne0d 13082 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → (√‘𝑚) ≠ 0) |
| 37 | 30, 35, 36 | divcld 12043 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
| 38 | 17, 37 | syldan 591 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘((𝑥↑2) / 𝑑)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
| 39 | 1, 38 | fsumcl 15769 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
| 40 | 39 | abscld 15475 |
. 2
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘Σ𝑚
∈ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ∈ ℝ) |
| 41 | | 1zzd 12648 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℤ) |
| 42 | 26 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑋 ∈ 𝐷) |
| 43 | | nnz 12634 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℤ) |
| 44 | 43 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℤ) |
| 45 | 18, 19, 20, 21, 42, 44 | dchrzrhcl 27289 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
| 46 | | nnrp 13046 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ+) |
| 47 | 46 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+) |
| 48 | 47 | rpsqrtcld 15450 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (√‘𝑚) ∈
ℝ+) |
| 49 | 48 | rpcnd 13079 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (√‘𝑚) ∈
ℂ) |
| 50 | 48 | rpne0d 13082 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (√‘𝑚) ≠ 0) |
| 51 | 45, 49, 50 | divcld 12043 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
| 52 | | dchrisum0lem1.f |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) |
| 53 | | 2fveq3 6911 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑚 → (𝑋‘(𝐿‘𝑎)) = (𝑋‘(𝐿‘𝑚))) |
| 54 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑚 → (√‘𝑎) = (√‘𝑚)) |
| 55 | 53, 54 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑚 → ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
| 56 | 55 | cbvmptv 5255 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) = (𝑚 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
| 57 | 52, 56 | eqtri 2765 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
| 58 | 51, 57 | fmptd 7134 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:ℕ⟶ℂ) |
| 59 | 58 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚) ∈ ℂ) |
| 60 | 10, 41, 59 | serf 14071 |
. . . . . . 7
⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ) |
| 61 | 60 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ seq1( + , 𝐹):ℕ⟶ℂ) |
| 62 | 3 | rpregt0d 13083 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 <
𝑥)) |
| 63 | 62 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
| 64 | 63 | simpld 494 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ) |
| 65 | | 1red 11262 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ) |
| 66 | | elfznn 13593 |
. . . . . . . . . . 11
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℕ) |
| 67 | 66 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℕ) |
| 68 | 67 | nnred 12281 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℝ) |
| 69 | 67 | nnge1d 12314 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 1 ≤ 𝑑) |
| 70 | 3 | rpred 13077 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ) |
| 71 | | fznnfl 13902 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → (𝑑 ∈
(1...(⌊‘𝑥))
↔ (𝑑 ∈ ℕ
∧ 𝑑 ≤ 𝑥))) |
| 72 | 70, 71 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑑 ∈
(1...(⌊‘𝑥))
↔ (𝑑 ∈ ℕ
∧ 𝑑 ≤ 𝑥))) |
| 73 | 72 | simplbda 499 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ≤ 𝑥) |
| 74 | 65, 68, 64, 69, 73 | letrd 11418 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 1 ≤ 𝑥) |
| 75 | | flge1nn 13861 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ) |
| 76 | 64, 74, 75 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (⌊‘𝑥)
∈ ℕ) |
| 77 | | eluznn 12960 |
. . . . . . 7
⊢
(((⌊‘𝑥)
∈ ℕ ∧ (⌊‘((𝑥↑2) / 𝑑)) ∈
(ℤ≥‘(⌊‘𝑥))) → (⌊‘((𝑥↑2) / 𝑑)) ∈ ℕ) |
| 78 | 76, 13, 77 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (⌊‘((𝑥↑2) / 𝑑)) ∈ ℕ) |
| 79 | 61, 78 | ffvelcdmd 7105 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) ∈ ℂ) |
| 80 | | dchrisum0.s |
. . . . . . 7
⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) |
| 81 | | climcl 15535 |
. . . . . . 7
⊢ (seq1( +
, 𝐹) ⇝ 𝑆 → 𝑆 ∈ ℂ) |
| 82 | 80, 81 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ ℂ) |
| 83 | 82 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑆 ∈
ℂ) |
| 84 | 79, 83 | subcld 11620 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆) ∈ ℂ) |
| 85 | 84 | abscld 15475 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) ∈ ℝ) |
| 86 | 61, 76 | ffvelcdmd 7105 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (seq1( + , 𝐹)‘(⌊‘𝑥)) ∈ ℂ) |
| 87 | 83, 86 | subcld 11620 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑆 − (seq1( +
, 𝐹)‘(⌊‘𝑥))) ∈ ℂ) |
| 88 | 87 | abscld 15475 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑆
− (seq1( + , 𝐹)‘(⌊‘𝑥)))) ∈ ℝ) |
| 89 | 85, 88 | readdcld 11290 |
. 2
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) + (abs‘(𝑆 − (seq1( + , 𝐹)‘(⌊‘𝑥))))) ∈ ℝ) |
| 90 | | 2re 12340 |
. . . . . 6
⊢ 2 ∈
ℝ |
| 91 | | dchrisum0.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) |
| 92 | | elrege0 13494 |
. . . . . . . 8
⊢ (𝐶 ∈ (0[,)+∞) ↔
(𝐶 ∈ ℝ ∧ 0
≤ 𝐶)) |
| 93 | 91, 92 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) |
| 94 | 93 | simpld 494 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℝ) |
| 95 | | remulcl 11240 |
. . . . . 6
⊢ ((2
∈ ℝ ∧ 𝐶
∈ ℝ) → (2 · 𝐶) ∈ ℝ) |
| 96 | 90, 94, 95 | sylancr 587 |
. . . . 5
⊢ (𝜑 → (2 · 𝐶) ∈
ℝ) |
| 97 | 96 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2
· 𝐶) ∈
ℝ) |
| 98 | 3 | rpsqrtcld 15450 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℝ+) |
| 99 | 97, 98 | rerpdivcld 13108 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2
· 𝐶) /
(√‘𝑥)) ∈
ℝ) |
| 100 | 99 | adantr 480 |
. 2
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((2 · 𝐶) /
(√‘𝑥)) ∈
ℝ) |
| 101 | | ssun1 4178 |
. . . . . . . . . . 11
⊢
(1...(⌊‘𝑥)) ⊆ ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) |
| 102 | 101, 15 | sseqtrrid 4027 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1...(⌊‘𝑥)) ⊆ (1...(⌊‘((𝑥↑2) / 𝑑)))) |
| 103 | 102 | sselda 3983 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) |
| 104 | | ovex 7464 |
. . . . . . . . . . 11
⊢ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)) ∈ V |
| 105 | 55, 52, 104 | fvmpt3i 7021 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → (𝐹‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
| 106 | 32, 105 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → (𝐹‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
| 107 | 103, 106 | syldan 591 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝐹‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
| 108 | 76, 10 | eleqtrdi 2851 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (⌊‘𝑥)
∈ (ℤ≥‘1)) |
| 109 | 103, 37 | syldan 591 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
| 110 | 107, 108,
109 | fsumser 15766 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) = (seq1( + , 𝐹)‘(⌊‘𝑥))) |
| 111 | 110, 86 | eqeltrd 2841 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
| 112 | 111, 39 | pncan2d 11622 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
| 113 | | reflcl 13836 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ∈
ℝ) |
| 114 | 64, 113 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (⌊‘𝑥)
∈ ℝ) |
| 115 | 114 | ltp1d 12198 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (⌊‘𝑥)
< ((⌊‘𝑥) +
1)) |
| 116 | | fzdisj 13591 |
. . . . . . . . 9
⊢
((⌊‘𝑥)
< ((⌊‘𝑥) +
1) → ((1...(⌊‘𝑥)) ∩ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) = ∅) |
| 117 | 115, 116 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((1...(⌊‘𝑥)) ∩ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) = ∅) |
| 118 | | fzfid 14014 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1...(⌊‘((𝑥↑2) / 𝑑))) ∈ Fin) |
| 119 | 117, 15, 118, 37 | fsumsplit 15777 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) = (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)))) |
| 120 | 78, 10 | eleqtrdi 2851 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (⌊‘((𝑥↑2) / 𝑑)) ∈
(ℤ≥‘1)) |
| 121 | 106, 120,
37 | fsumser 15766 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) = (seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑)))) |
| 122 | 119, 121 | eqtr3d 2779 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = (seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑)))) |
| 123 | 122, 110 | oveq12d 7449 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = ((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − (seq1( + , 𝐹)‘(⌊‘𝑥)))) |
| 124 | 112, 123 | eqtr3d 2779 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) = ((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − (seq1( + , 𝐹)‘(⌊‘𝑥)))) |
| 125 | 124 | fveq2d 6910 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘Σ𝑚
∈ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = (abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − (seq1( + , 𝐹)‘(⌊‘𝑥))))) |
| 126 | 79, 86, 83 | abs3difd 15499 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − (seq1( + , 𝐹)‘(⌊‘𝑥)))) ≤ ((abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) + (abs‘(𝑆 − (seq1( + , 𝐹)‘(⌊‘𝑥)))))) |
| 127 | 125, 126 | eqbrtrd 5165 |
. 2
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘Σ𝑚
∈ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ≤ ((abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) + (abs‘(𝑆 − (seq1( + , 𝐹)‘(⌊‘𝑥)))))) |
| 128 | 94 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝐶 ∈
ℝ) |
| 129 | | simplr 769 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ+) |
| 130 | 129 | rpsqrtcld 15450 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑥)
∈ ℝ+) |
| 131 | 128, 130 | rerpdivcld 13108 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐶 /
(√‘𝑥)) ∈
ℝ) |
| 132 | | 2z 12649 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
| 133 | | rpexpcl 14121 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝑥↑2) ∈
ℝ+) |
| 134 | 3, 132, 133 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑2) ∈
ℝ+) |
| 135 | 134 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥↑2) ∈
ℝ+) |
| 136 | 67 | nnrpd 13075 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℝ+) |
| 137 | 135, 136 | rpdivcld 13094 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((𝑥↑2) / 𝑑) ∈
ℝ+) |
| 138 | 137 | rpsqrtcld 15450 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (√‘((𝑥↑2) / 𝑑)) ∈
ℝ+) |
| 139 | 128, 138 | rerpdivcld 13108 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐶 /
(√‘((𝑥↑2)
/ 𝑑))) ∈
ℝ) |
| 140 | | 2fveq3 6911 |
. . . . . . . 8
⊢ (𝑦 = ((𝑥↑2) / 𝑑) → (seq1( + , 𝐹)‘(⌊‘𝑦)) = (seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑)))) |
| 141 | 140 | fvoveq1d 7453 |
. . . . . . 7
⊢ (𝑦 = ((𝑥↑2) / 𝑑) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) = (abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆))) |
| 142 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑦 = ((𝑥↑2) / 𝑑) → (√‘𝑦) = (√‘((𝑥↑2) / 𝑑))) |
| 143 | 142 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑦 = ((𝑥↑2) / 𝑑) → (𝐶 / (√‘𝑦)) = (𝐶 / (√‘((𝑥↑2) / 𝑑)))) |
| 144 | 141, 143 | breq12d 5156 |
. . . . . 6
⊢ (𝑦 = ((𝑥↑2) / 𝑑) → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦)) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) ≤ (𝐶 / (√‘((𝑥↑2) / 𝑑))))) |
| 145 | | dchrisum0.1 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) |
| 146 | 145 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) |
| 147 | 134 | rpred 13077 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑2) ∈
ℝ) |
| 148 | | nndivre 12307 |
. . . . . . . 8
⊢ (((𝑥↑2) ∈ ℝ ∧
𝑑 ∈ ℕ) →
((𝑥↑2) / 𝑑) ∈
ℝ) |
| 149 | 147, 66, 148 | syl2an 596 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((𝑥↑2) / 𝑑) ∈
ℝ) |
| 150 | 12 | simpld 494 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ≤ ((𝑥↑2) / 𝑑)) |
| 151 | 65, 64, 149, 74, 150 | letrd 11418 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 1 ≤ ((𝑥↑2) /
𝑑)) |
| 152 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 153 | | elicopnf 13485 |
. . . . . . . 8
⊢ (1 ∈
ℝ → (((𝑥↑2)
/ 𝑑) ∈ (1[,)+∞)
↔ (((𝑥↑2) / 𝑑) ∈ ℝ ∧ 1 ≤
((𝑥↑2) / 𝑑)))) |
| 154 | 152, 153 | ax-mp 5 |
. . . . . . 7
⊢ (((𝑥↑2) / 𝑑) ∈ (1[,)+∞) ↔ (((𝑥↑2) / 𝑑) ∈ ℝ ∧ 1 ≤ ((𝑥↑2) / 𝑑))) |
| 155 | 149, 151,
154 | sylanbrc 583 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((𝑥↑2) / 𝑑) ∈
(1[,)+∞)) |
| 156 | 144, 146,
155 | rspcdva 3623 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) ≤ (𝐶 / (√‘((𝑥↑2) / 𝑑)))) |
| 157 | 130 | rpregt0d 13083 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑥)
∈ ℝ ∧ 0 < (√‘𝑥))) |
| 158 | 138 | rpregt0d 13083 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((√‘((𝑥↑2) / 𝑑)) ∈ ℝ ∧ 0 <
(√‘((𝑥↑2)
/ 𝑑)))) |
| 159 | 93 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐶 ∈ ℝ
∧ 0 ≤ 𝐶)) |
| 160 | 129 | rprege0d 13084 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
| 161 | 137 | rprege0d 13084 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (((𝑥↑2) / 𝑑) ∈ ℝ ∧ 0 ≤
((𝑥↑2) / 𝑑))) |
| 162 | | sqrtle 15299 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) ∧ (((𝑥↑2) / 𝑑) ∈ ℝ ∧ 0 ≤ ((𝑥↑2) / 𝑑))) → (𝑥 ≤ ((𝑥↑2) / 𝑑) ↔ (√‘𝑥) ≤ (√‘((𝑥↑2) / 𝑑)))) |
| 163 | 160, 161,
162 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ≤ ((𝑥↑2) / 𝑑) ↔ (√‘𝑥) ≤ (√‘((𝑥↑2) / 𝑑)))) |
| 164 | 150, 163 | mpbid 232 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑥)
≤ (√‘((𝑥↑2) / 𝑑))) |
| 165 | | lediv2a 12162 |
. . . . . 6
⊢
(((((√‘𝑥) ∈ ℝ ∧ 0 <
(√‘𝑥)) ∧
((√‘((𝑥↑2)
/ 𝑑)) ∈ ℝ ∧
0 < (√‘((𝑥↑2) / 𝑑))) ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ (√‘𝑥) ≤ (√‘((𝑥↑2) / 𝑑))) → (𝐶 / (√‘((𝑥↑2) / 𝑑))) ≤ (𝐶 / (√‘𝑥))) |
| 166 | 157, 158,
159, 164, 165 | syl31anc 1375 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐶 /
(√‘((𝑥↑2)
/ 𝑑))) ≤ (𝐶 / (√‘𝑥))) |
| 167 | 85, 139, 131, 156, 166 | letrd 11418 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) ≤ (𝐶 / (√‘𝑥))) |
| 168 | 83, 86 | abssubd 15492 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑆
− (seq1( + , 𝐹)‘(⌊‘𝑥)))) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑆))) |
| 169 | | 2fveq3 6911 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (seq1( + , 𝐹)‘(⌊‘𝑦)) = (seq1( + , 𝐹)‘(⌊‘𝑥))) |
| 170 | 169 | fvoveq1d 7453 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑆))) |
| 171 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (√‘𝑦) = (√‘𝑥)) |
| 172 | 171 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (𝐶 / (√‘𝑦)) = (𝐶 / (√‘𝑥))) |
| 173 | 170, 172 | breq12d 5156 |
. . . . . 6
⊢ (𝑦 = 𝑥 → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦)) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑆)) ≤ (𝐶 / (√‘𝑥)))) |
| 174 | | elicopnf 13485 |
. . . . . . . 8
⊢ (1 ∈
ℝ → (𝑥 ∈
(1[,)+∞) ↔ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥))) |
| 175 | 152, 174 | ax-mp 5 |
. . . . . . 7
⊢ (𝑥 ∈ (1[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 1
≤ 𝑥)) |
| 176 | 64, 74, 175 | sylanbrc 583 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
(1[,)+∞)) |
| 177 | 173, 146,
176 | rspcdva 3623 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑆)) ≤ (𝐶 / (√‘𝑥))) |
| 178 | 168, 177 | eqbrtrd 5165 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑆
− (seq1( + , 𝐹)‘(⌊‘𝑥)))) ≤ (𝐶 / (√‘𝑥))) |
| 179 | 85, 88, 131, 131, 167, 178 | le2addd 11882 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) + (abs‘(𝑆 − (seq1( + , 𝐹)‘(⌊‘𝑥))))) ≤ ((𝐶 / (√‘𝑥)) + (𝐶 / (√‘𝑥)))) |
| 180 | | 2cnd 12344 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 2 ∈ ℂ) |
| 181 | 94 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈
ℝ) |
| 182 | 181 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈
ℂ) |
| 183 | 182 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝐶 ∈
ℂ) |
| 184 | 98 | rpcnne0d 13086 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((√‘𝑥) ∈
ℂ ∧ (√‘𝑥) ≠ 0)) |
| 185 | 184 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑥)
∈ ℂ ∧ (√‘𝑥) ≠ 0)) |
| 186 | | divass 11940 |
. . . . 5
⊢ ((2
∈ ℂ ∧ 𝐶
∈ ℂ ∧ ((√‘𝑥) ∈ ℂ ∧ (√‘𝑥) ≠ 0)) → ((2 ·
𝐶) / (√‘𝑥)) = (2 · (𝐶 / (√‘𝑥)))) |
| 187 | 180, 183,
185, 186 | syl3anc 1373 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((2 · 𝐶) /
(√‘𝑥)) = (2
· (𝐶 /
(√‘𝑥)))) |
| 188 | 131 | recnd 11289 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐶 /
(√‘𝑥)) ∈
ℂ) |
| 189 | 188 | 2timesd 12509 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (2 · (𝐶 /
(√‘𝑥))) =
((𝐶 / (√‘𝑥)) + (𝐶 / (√‘𝑥)))) |
| 190 | 187, 189 | eqtrd 2777 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((2 · 𝐶) /
(√‘𝑥)) =
((𝐶 / (√‘𝑥)) + (𝐶 / (√‘𝑥)))) |
| 191 | 179, 190 | breqtrrd 5171 |
. 2
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((seq1( + , 𝐹)‘(⌊‘((𝑥↑2) / 𝑑))) − 𝑆)) + (abs‘(𝑆 − (seq1( + , 𝐹)‘(⌊‘𝑥))))) ≤ ((2 · 𝐶) / (√‘𝑥))) |
| 192 | 40, 89, 100, 127, 191 | letrd 11418 |
1
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘Σ𝑚
∈ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ≤ ((2 · 𝐶) / (√‘𝑥))) |