Step | Hyp | Ref
| Expression |
1 | | fzodisj 12371 |
. . . . . . . . 9
⊢
((1..^(𝐼 + 1)) ∩
((𝐼 + 1)..^(𝐽 + 1))) =
∅ |
2 | 1 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ((1..^(𝐼 + 1)) ∩ ((𝐼 + 1)..^(𝐽 + 1))) = ∅) |
3 | | dchrisumlem2.4 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ ℕ) |
4 | 3 | peano2nnd 10914 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐼 + 1) ∈ ℕ) |
5 | | nnuz 11599 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
6 | 4, 5 | syl6eleq 2698 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐼 + 1) ∈
(ℤ≥‘1)) |
7 | | dchrisumlem2.5 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘𝐼)) |
8 | | eluzp1p1 11589 |
. . . . . . . . . . 11
⊢ (𝐽 ∈
(ℤ≥‘𝐼) → (𝐽 + 1) ∈
(ℤ≥‘(𝐼 + 1))) |
9 | 7, 8 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐽 + 1) ∈
(ℤ≥‘(𝐼 + 1))) |
10 | | elfzuzb 12207 |
. . . . . . . . . 10
⊢ ((𝐼 + 1) ∈ (1...(𝐽 + 1)) ↔ ((𝐼 + 1) ∈
(ℤ≥‘1) ∧ (𝐽 + 1) ∈
(ℤ≥‘(𝐼 + 1)))) |
11 | 6, 9, 10 | sylanbrc 695 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼 + 1) ∈ (1...(𝐽 + 1))) |
12 | | fzosplit 12370 |
. . . . . . . . 9
⊢ ((𝐼 + 1) ∈ (1...(𝐽 + 1)) → (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1)))) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1)))) |
14 | | fzofi 12635 |
. . . . . . . . 9
⊢
(1..^(𝐽 + 1)) ∈
Fin |
15 | 14 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (1..^(𝐽 + 1)) ∈ Fin) |
16 | | elfzouz 12343 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1..^(𝐽 + 1)) → 𝑖 ∈
(ℤ≥‘1)) |
17 | 16, 5 | syl6eleqr 2699 |
. . . . . . . . 9
⊢ (𝑖 ∈ (1..^(𝐽 + 1)) → 𝑖 ∈ ℕ) |
18 | | rpvmasum.g |
. . . . . . . . . . 11
⊢ 𝐺 = (DChr‘𝑁) |
19 | | rpvmasum.z |
. . . . . . . . . . 11
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
20 | | rpvmasum.d |
. . . . . . . . . . 11
⊢ 𝐷 = (Base‘𝐺) |
21 | | rpvmasum.l |
. . . . . . . . . . 11
⊢ 𝐿 = (ℤRHom‘𝑍) |
22 | | dchrisum.b |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
23 | 22 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑋 ∈ 𝐷) |
24 | | nnz 11276 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ → 𝑖 ∈
ℤ) |
25 | 24 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℤ) |
26 | 18, 19, 20, 21, 23, 25 | dchrzrhcl 24770 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑋‘(𝐿‘𝑖)) ∈ ℂ) |
27 | | nnrp 11718 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℕ → 𝑖 ∈
ℝ+) |
28 | | rpvmasum.a |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℕ) |
29 | | rpvmasum.1 |
. . . . . . . . . . . . . . 15
⊢ 1 =
(0g‘𝐺) |
30 | | dchrisum.n1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ≠ 1 ) |
31 | | dchrisum.2 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) |
32 | | dchrisum.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℕ) |
33 | | dchrisum.4 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈
ℝ) |
34 | | dchrisum.5 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) |
35 | | dchrisum.6 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟
0) |
36 | | dchrisum.7 |
. . . . . . . . . . . . . . 15
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) |
37 | 19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36 | dchrisumlema 24977 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑖 ∈ ℝ+ →
⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ) ∧ (𝑖 ∈ (𝑀[,)+∞) → 0 ≤
⦋𝑖 / 𝑛⦌𝐴))) |
38 | 37 | simpld 474 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑖 ∈ ℝ+ →
⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ)) |
39 | 27, 38 | syl5 33 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑖 ∈ ℕ → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ)) |
40 | 39 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ) |
41 | 40 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℂ) |
42 | 26, 41 | mulcld 9939 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ) |
43 | 17, 42 | sylan2 490 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1..^(𝐽 + 1))) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ) |
44 | 2, 13, 15, 43 | fsumsplit 14318 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (1..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴))) |
45 | | eluzelz 11573 |
. . . . . . . . 9
⊢ (𝐽 ∈
(ℤ≥‘𝐼) → 𝐽 ∈ ℤ) |
46 | | fzval3 12404 |
. . . . . . . . 9
⊢ (𝐽 ∈ ℤ →
(1...𝐽) = (1..^(𝐽 + 1))) |
47 | 7, 45, 46 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (1...𝐽) = (1..^(𝐽 + 1))) |
48 | 47 | sumeq1d 14279 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = Σ𝑖 ∈ (1..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) |
49 | 3 | nnzd 11357 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ ℤ) |
50 | | fzval3 12404 |
. . . . . . . . . 10
⊢ (𝐼 ∈ ℤ →
(1...𝐼) = (1..^(𝐼 + 1))) |
51 | 49, 50 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝐼) = (1..^(𝐼 + 1))) |
52 | 51 | sumeq1d 14279 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) |
53 | 52 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴))) |
54 | 44, 48, 53 | 3eqtr4d 2654 |
. . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴))) |
55 | | elfznn 12241 |
. . . . . . . 8
⊢ (𝑖 ∈ (1...𝐽) → 𝑖 ∈ ℕ) |
56 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ) |
57 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑛𝑖 |
58 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛(𝑋‘(𝐿‘𝑖)) |
59 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛
· |
60 | | nfcsb1v 3515 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴 |
61 | 58, 59, 60 | nfov 6575 |
. . . . . . . . . 10
⊢
Ⅎ𝑛((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) |
62 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑖 → (𝐿‘𝑛) = (𝐿‘𝑖)) |
63 | 62 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑖 → (𝑋‘(𝐿‘𝑛)) = (𝑋‘(𝐿‘𝑖))) |
64 | | csbeq1a 3508 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑖 → 𝐴 = ⦋𝑖 / 𝑛⦌𝐴) |
65 | 63, 64 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑖 → ((𝑋‘(𝐿‘𝑛)) · 𝐴) = ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) |
66 | 57, 61, 65, 36 | fvmptf 6209 |
. . . . . . . . 9
⊢ ((𝑖 ∈ ℕ ∧ ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ) → (𝐹‘𝑖) = ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) |
67 | 56, 42, 66 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) = ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) |
68 | 55, 67 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝐽)) → (𝐹‘𝑖) = ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) |
69 | 3, 5 | syl6eleq 2698 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈
(ℤ≥‘1)) |
70 | | uztrn 11580 |
. . . . . . . 8
⊢ ((𝐽 ∈
(ℤ≥‘𝐼) ∧ 𝐼 ∈ (ℤ≥‘1))
→ 𝐽 ∈
(ℤ≥‘1)) |
71 | 7, 69, 70 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈
(ℤ≥‘1)) |
72 | 55, 42 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝐽)) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ) |
73 | 68, 71, 72 | fsumser 14308 |
. . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = (seq1( + , 𝐹)‘𝐽)) |
74 | 54, 73 | eqtr3d 2646 |
. . . . 5
⊢ (𝜑 → (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) = (seq1( + , 𝐹)‘𝐽)) |
75 | | elfznn 12241 |
. . . . . . 7
⊢ (𝑖 ∈ (1...𝐼) → 𝑖 ∈ ℕ) |
76 | 75, 67 | sylan2 490 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝐼)) → (𝐹‘𝑖) = ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) |
77 | 75, 42 | sylan2 490 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝐼)) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ) |
78 | 76, 69, 77 | fsumser 14308 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = (seq1( + , 𝐹)‘𝐼)) |
79 | 74, 78 | oveq12d 6567 |
. . . 4
⊢ (𝜑 → ((Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) − Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) = ((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) |
80 | | fzfid 12634 |
. . . . . 6
⊢ (𝜑 → (1...𝐼) ∈ Fin) |
81 | 80, 77 | fsumcl 14311 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ) |
82 | | fzofi 12635 |
. . . . . . 7
⊢ ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin |
83 | 82 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin) |
84 | | ssun2 3739 |
. . . . . . . . 9
⊢ ((𝐼 + 1)..^(𝐽 + 1)) ⊆ ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1))) |
85 | 84, 13 | syl5sseqr 3617 |
. . . . . . . 8
⊢ (𝜑 → ((𝐼 + 1)..^(𝐽 + 1)) ⊆ (1..^(𝐽 + 1))) |
86 | 85 | sselda 3568 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ (1..^(𝐽 + 1))) |
87 | 86, 43 | syldan 486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ) |
88 | 83, 87 | fsumcl 14311 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ) |
89 | 81, 88 | pncan2d 10273 |
. . . 4
⊢ (𝜑 → ((Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) − Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) |
90 | 79, 89 | eqtr3d 2646 |
. . 3
⊢ (𝜑 → ((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) |
91 | 90 | fveq2d 6107 |
. 2
⊢ (𝜑 → (abs‘((seq1( + ,
𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) = (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴))) |
92 | 88 | abscld 14023 |
. . 3
⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) ∈ ℝ) |
93 | | 2re 10967 |
. . . . . 6
⊢ 2 ∈
ℝ |
94 | 93 | a1i 11 |
. . . . 5
⊢ (𝜑 → 2 ∈
ℝ) |
95 | | dchrisum.9 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ ℝ) |
96 | 94, 95 | remulcld 9949 |
. . . 4
⊢ (𝜑 → (2 · 𝑅) ∈
ℝ) |
97 | 40 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑖 ∈ ℕ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ) |
98 | | csbeq1 3502 |
. . . . . . 7
⊢ (𝑖 = (𝐼 + 1) → ⦋𝑖 / 𝑛⦌𝐴 = ⦋(𝐼 + 1) / 𝑛⦌𝐴) |
99 | 98 | eleq1d 2672 |
. . . . . 6
⊢ (𝑖 = (𝐼 + 1) → (⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ ↔ ⦋(𝐼 + 1) / 𝑛⦌𝐴 ∈ ℝ)) |
100 | 99 | rspcv 3278 |
. . . . 5
⊢ ((𝐼 + 1) ∈ ℕ →
(∀𝑖 ∈ ℕ
⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ → ⦋(𝐼 + 1) / 𝑛⦌𝐴 ∈ ℝ)) |
101 | 4, 97, 100 | sylc 63 |
. . . 4
⊢ (𝜑 → ⦋(𝐼 + 1) / 𝑛⦌𝐴 ∈ ℝ) |
102 | 96, 101 | remulcld 9949 |
. . 3
⊢ (𝜑 → ((2 · 𝑅) · ⦋(𝐼 + 1) / 𝑛⦌𝐴) ∈ ℝ) |
103 | | dchrisumlem2.1 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈
ℝ+) |
104 | 33 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ) |
105 | | nfcsb1v 3515 |
. . . . . . 7
⊢
Ⅎ𝑛⦋𝑈 / 𝑛⦌𝐴 |
106 | 105 | nfel1 2765 |
. . . . . 6
⊢
Ⅎ𝑛⦋𝑈 / 𝑛⦌𝐴 ∈ ℝ |
107 | | csbeq1a 3508 |
. . . . . . 7
⊢ (𝑛 = 𝑈 → 𝐴 = ⦋𝑈 / 𝑛⦌𝐴) |
108 | 107 | eleq1d 2672 |
. . . . . 6
⊢ (𝑛 = 𝑈 → (𝐴 ∈ ℝ ↔ ⦋𝑈 / 𝑛⦌𝐴 ∈ ℝ)) |
109 | 106, 108 | rspc 3276 |
. . . . 5
⊢ (𝑈 ∈ ℝ+
→ (∀𝑛 ∈
ℝ+ 𝐴
∈ ℝ → ⦋𝑈 / 𝑛⦌𝐴 ∈ ℝ)) |
110 | 103, 104,
109 | sylc 63 |
. . . 4
⊢ (𝜑 → ⦋𝑈 / 𝑛⦌𝐴 ∈ ℝ) |
111 | 96, 110 | remulcld 9949 |
. . 3
⊢ (𝜑 → ((2 · 𝑅) · ⦋𝑈 / 𝑛⦌𝐴) ∈ ℝ) |
112 | 71, 5 | syl6eleqr 2699 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ ℕ) |
113 | 112 | peano2nnd 10914 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐽 + 1) ∈ ℕ) |
114 | 113 | nnrpd 11746 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐽 + 1) ∈
ℝ+) |
115 | 19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36 | dchrisumlema 24977 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐽 + 1) ∈ ℝ+ →
⦋(𝐽 + 1) /
𝑛⦌𝐴 ∈ ℝ) ∧ ((𝐽 + 1) ∈ (𝑀[,)+∞) → 0 ≤
⦋(𝐽 + 1) /
𝑛⦌𝐴))) |
116 | 115 | simpld 474 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐽 + 1) ∈ ℝ+ →
⦋(𝐽 + 1) /
𝑛⦌𝐴 ∈
ℝ)) |
117 | 114, 116 | mpd 15 |
. . . . . . . . 9
⊢ (𝜑 → ⦋(𝐽 + 1) / 𝑛⦌𝐴 ∈ ℝ) |
118 | 117 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → ⦋(𝐽 + 1) / 𝑛⦌𝐴 ∈ ℂ) |
119 | | fzofi 12635 |
. . . . . . . . . 10
⊢
(0..^(𝐽 + 1)) ∈
Fin |
120 | 119 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (0..^(𝐽 + 1)) ∈ Fin) |
121 | | elfzoelz 12339 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (0..^(𝐽 + 1)) → 𝑛 ∈ ℤ) |
122 | 22 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℤ) → 𝑋 ∈ 𝐷) |
123 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℤ) → 𝑛 ∈ ℤ) |
124 | 18, 19, 20, 21, 122, 123 | dchrzrhcl 24770 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℤ) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
125 | 121, 124 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^(𝐽 + 1))) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
126 | 120, 125 | fsumcl 14311 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
127 | 118, 126 | mulcld 9939 |
. . . . . . 7
⊢ (𝜑 → (⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) ∈ ℂ) |
128 | 101 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → ⦋(𝐼 + 1) / 𝑛⦌𝐴 ∈ ℂ) |
129 | | fzofi 12635 |
. . . . . . . . . 10
⊢
(0..^(𝐼 + 1)) ∈
Fin |
130 | 129 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (0..^(𝐼 + 1)) ∈ Fin) |
131 | | elfzoelz 12339 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (0..^(𝐼 + 1)) → 𝑛 ∈ ℤ) |
132 | 131, 124 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^(𝐼 + 1))) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
133 | 130, 132 | fsumcl 14311 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
134 | 128, 133 | mulcld 9939 |
. . . . . . 7
⊢ (𝜑 → (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))) ∈ ℂ) |
135 | 127, 134 | subcld 10271 |
. . . . . 6
⊢ (𝜑 → ((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) ∈ ℂ) |
136 | 135 | abscld 14023 |
. . . . 5
⊢ (𝜑 →
(abs‘((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) ∈ ℝ) |
137 | 86, 17 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ ℕ) |
138 | | peano2nn 10909 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℕ → (𝑖 + 1) ∈
ℕ) |
139 | 138 | nnrpd 11746 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ → (𝑖 + 1) ∈
ℝ+) |
140 | | nfcsb1v 3515 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛⦋(𝑖 + 1) / 𝑛⦌𝐴 |
141 | 140 | nfel1 2765 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛⦋(𝑖 + 1) / 𝑛⦌𝐴 ∈ ℝ |
142 | | csbeq1a 3508 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑖 + 1) → 𝐴 = ⦋(𝑖 + 1) / 𝑛⦌𝐴) |
143 | 142 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑖 + 1) → (𝐴 ∈ ℝ ↔ ⦋(𝑖 + 1) / 𝑛⦌𝐴 ∈ ℝ)) |
144 | 141, 143 | rspc 3276 |
. . . . . . . . . . . . 13
⊢ ((𝑖 + 1) ∈ ℝ+
→ (∀𝑛 ∈
ℝ+ 𝐴
∈ ℝ → ⦋(𝑖 + 1) / 𝑛⦌𝐴 ∈ ℝ)) |
145 | 144 | impcom 445 |
. . . . . . . . . . . 12
⊢
((∀𝑛 ∈
ℝ+ 𝐴
∈ ℝ ∧ (𝑖 +
1) ∈ ℝ+) → ⦋(𝑖 + 1) / 𝑛⦌𝐴 ∈ ℝ) |
146 | 104, 139,
145 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ⦋(𝑖 + 1) / 𝑛⦌𝐴 ∈ ℝ) |
147 | 146, 40 | resubcld 10337 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) →
(⦋(𝑖 + 1) /
𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) ∈ ℝ) |
148 | 147 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) →
(⦋(𝑖 + 1) /
𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ) |
149 | | fzofi 12635 |
. . . . . . . . . . . 12
⊢
(0..^(𝑖 + 1)) ∈
Fin |
150 | 149 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (0..^(𝑖 + 1)) ∈ Fin) |
151 | | elfzoelz 12339 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (0..^(𝑖 + 1)) → 𝑛 ∈ ℤ) |
152 | 151, 124 | sylan2 490 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^(𝑖 + 1))) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
153 | 150, 152 | fsumcl 14311 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
154 | 153 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
155 | 148, 154 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) →
((⦋(𝑖 + 1) /
𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))) ∈ ℂ) |
156 | 137, 155 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))) ∈ ℂ) |
157 | 83, 156 | fsumcl 14311 |
. . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))) ∈ ℂ) |
158 | 157 | abscld 14023 |
. . . . 5
⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ∈ ℝ) |
159 | 136, 158 | readdcld 9948 |
. . . 4
⊢ (𝜑 →
((abs‘((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))) ∈ ℝ) |
160 | 26, 41 | mulcomd 9940 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = (⦋𝑖 / 𝑛⦌𝐴 · (𝑋‘(𝐿‘𝑖)))) |
161 | | nnnn0 11176 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℕ → 𝑖 ∈
ℕ0) |
162 | 161 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ0) |
163 | | nn0uz 11598 |
. . . . . . . . . . . . . . 15
⊢
ℕ0 = (ℤ≥‘0) |
164 | 162, 163 | syl6eleq 2698 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈
(ℤ≥‘0)) |
165 | | elfzelz 12213 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (0...𝑖) → 𝑛 ∈ ℤ) |
166 | 124 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
167 | 165, 166 | sylan2 490 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑛 ∈ (0...𝑖)) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
168 | 164, 167,
63 | fzosump1 14325 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) = (Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)) + (𝑋‘(𝐿‘𝑖)))) |
169 | 168 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))) = ((Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)) + (𝑋‘(𝐿‘𝑖))) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)))) |
170 | | fzofi 12635 |
. . . . . . . . . . . . . . 15
⊢
(0..^𝑖) ∈
Fin |
171 | 170 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (0..^𝑖) ∈ Fin) |
172 | | elfzoelz 12339 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (0..^𝑖) → 𝑛 ∈ ℤ) |
173 | 172, 166 | sylan2 490 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑛 ∈ (0..^𝑖)) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
174 | 171, 173 | fsumcl 14311 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
175 | 174, 26 | pncan2d 10273 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)) + (𝑋‘(𝐿‘𝑖))) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))) = (𝑋‘(𝐿‘𝑖))) |
176 | 169, 175 | eqtr2d 2645 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑋‘(𝐿‘𝑖)) = (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)))) |
177 | 176 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (⦋𝑖 / 𝑛⦌𝐴 · (𝑋‘(𝐿‘𝑖))) = (⦋𝑖 / 𝑛⦌𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))))) |
178 | 160, 177 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = (⦋𝑖 / 𝑛⦌𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))))) |
179 | 137, 178 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = (⦋𝑖 / 𝑛⦌𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))))) |
180 | 179 | sumeq2dv 14281 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / 𝑛⦌𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))))) |
181 | | csbeq1 3502 |
. . . . . . . . 9
⊢ (𝑘 = 𝑖 → ⦋𝑘 / 𝑛⦌𝐴 = ⦋𝑖 / 𝑛⦌𝐴) |
182 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → (0..^𝑘) = (0..^𝑖)) |
183 | 182 | sumeq1d 14279 |
. . . . . . . . 9
⊢ (𝑘 = 𝑖 → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))) |
184 | 181, 183 | jca 553 |
. . . . . . . 8
⊢ (𝑘 = 𝑖 → (⦋𝑘 / 𝑛⦌𝐴 = ⦋𝑖 / 𝑛⦌𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)))) |
185 | | csbeq1 3502 |
. . . . . . . . 9
⊢ (𝑘 = (𝑖 + 1) → ⦋𝑘 / 𝑛⦌𝐴 = ⦋(𝑖 + 1) / 𝑛⦌𝐴) |
186 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑖 + 1) → (0..^𝑘) = (0..^(𝑖 + 1))) |
187 | 186 | sumeq1d 14279 |
. . . . . . . . 9
⊢ (𝑘 = (𝑖 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))) |
188 | 185, 187 | jca 553 |
. . . . . . . 8
⊢ (𝑘 = (𝑖 + 1) → (⦋𝑘 / 𝑛⦌𝐴 = ⦋(𝑖 + 1) / 𝑛⦌𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) |
189 | | csbeq1 3502 |
. . . . . . . . 9
⊢ (𝑘 = (𝐼 + 1) → ⦋𝑘 / 𝑛⦌𝐴 = ⦋(𝐼 + 1) / 𝑛⦌𝐴) |
190 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑘 = (𝐼 + 1) → (0..^𝑘) = (0..^(𝐼 + 1))) |
191 | 190 | sumeq1d 14279 |
. . . . . . . . 9
⊢ (𝑘 = (𝐼 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))) |
192 | 189, 191 | jca 553 |
. . . . . . . 8
⊢ (𝑘 = (𝐼 + 1) → (⦋𝑘 / 𝑛⦌𝐴 = ⦋(𝐼 + 1) / 𝑛⦌𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) |
193 | | csbeq1 3502 |
. . . . . . . . 9
⊢ (𝑘 = (𝐽 + 1) → ⦋𝑘 / 𝑛⦌𝐴 = ⦋(𝐽 + 1) / 𝑛⦌𝐴) |
194 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑘 = (𝐽 + 1) → (0..^𝑘) = (0..^(𝐽 + 1))) |
195 | 194 | sumeq1d 14279 |
. . . . . . . . 9
⊢ (𝑘 = (𝐽 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) |
196 | 193, 195 | jca 553 |
. . . . . . . 8
⊢ (𝑘 = (𝐽 + 1) → (⦋𝑘 / 𝑛⦌𝐴 = ⦋(𝐽 + 1) / 𝑛⦌𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) |
197 | | elfzuz 12209 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1)) → 𝑘 ∈ (ℤ≥‘(𝐼 + 1))) |
198 | | eluznn 11634 |
. . . . . . . . . 10
⊢ (((𝐼 + 1) ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝐼 + 1))) → 𝑘 ∈ ℕ) |
199 | 4, 197, 198 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → 𝑘 ∈ ℕ) |
200 | 41 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑖 ∈ ℕ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℂ) |
201 | | csbeq1 3502 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → ⦋𝑖 / 𝑛⦌𝐴 = ⦋𝑘 / 𝑛⦌𝐴) |
202 | 201 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → (⦋𝑖 / 𝑛⦌𝐴 ∈ ℂ ↔ ⦋𝑘 / 𝑛⦌𝐴 ∈ ℂ)) |
203 | 202 | rspccva 3281 |
. . . . . . . . . 10
⊢
((∀𝑖 ∈
ℕ ⦋𝑖 /
𝑛⦌𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) →
⦋𝑘 / 𝑛⦌𝐴 ∈ ℂ) |
204 | 200, 203 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ⦋𝑘 / 𝑛⦌𝐴 ∈ ℂ) |
205 | 199, 204 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → ⦋𝑘 / 𝑛⦌𝐴 ∈ ℂ) |
206 | | fzofi 12635 |
. . . . . . . . . . 11
⊢
(0..^𝑘) ∈
Fin |
207 | 206 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (0..^𝑘) ∈ Fin) |
208 | | elfzoelz 12339 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (0..^𝑘) → 𝑛 ∈ ℤ) |
209 | 208, 124 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑘)) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
210 | 207, 209 | fsumcl 14311 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
211 | 210 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
212 | 184, 188,
192, 196, 9, 205, 211 | fsumparts 14379 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / 𝑛⦌𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)))) = (((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))) |
213 | 180, 212 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = (((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))) |
214 | 213 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) = (abs‘(((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))))) |
215 | 135, 157 | abs2dif2d 14045 |
. . . . 5
⊢ (𝜑 →
(abs‘(((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))) ≤
((abs‘((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))))) |
216 | 214, 215 | eqbrtrd 4605 |
. . . 4
⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) ≤ ((abs‘((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))))) |
217 | 117, 101 | readdcld 9948 |
. . . . . . 7
⊢ (𝜑 → (⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) ∈ ℝ) |
218 | 217, 95 | remulcld 9949 |
. . . . . 6
⊢ (𝜑 → ((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) · 𝑅) ∈ ℝ) |
219 | 181, 185,
189, 193, 9, 205 | telfsumo 14375 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) = (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴)) |
220 | 137, 40 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ) |
221 | 137, 146 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ⦋(𝑖 + 1) / 𝑛⦌𝐴 ∈ ℝ) |
222 | 220, 221 | resubcld 10337 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) ∈ ℝ) |
223 | 83, 222 | fsumrecl 14312 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) ∈ ℝ) |
224 | 219, 223 | eqeltrrd 2689 |
. . . . . . 7
⊢ (𝜑 → (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) ∈ ℝ) |
225 | 224, 95 | remulcld 9949 |
. . . . . 6
⊢ (𝜑 → ((⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) · 𝑅) ∈ ℝ) |
226 | 127 | abscld 14023 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘(⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) ∈ ℝ) |
227 | 134 | abscld 14023 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘(⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) ∈ ℝ) |
228 | 226, 227 | readdcld 9948 |
. . . . . . 7
⊢ (𝜑 →
((abs‘(⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) + (abs‘(⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) ∈ ℝ) |
229 | 127, 134 | abs2dif2d 14045 |
. . . . . . 7
⊢ (𝜑 →
(abs‘((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) ≤ ((abs‘(⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) + (abs‘(⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))))) |
230 | 117, 95 | remulcld 9949 |
. . . . . . . . 9
⊢ (𝜑 → (⦋(𝐽 + 1) / 𝑛⦌𝐴 · 𝑅) ∈ ℝ) |
231 | 101, 95 | remulcld 9949 |
. . . . . . . . 9
⊢ (𝜑 → (⦋(𝐼 + 1) / 𝑛⦌𝐴 · 𝑅) ∈ ℝ) |
232 | 118, 126 | absmuld 14041 |
. . . . . . . . . . 11
⊢ (𝜑 →
(abs‘(⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) = ((abs‘⦋(𝐽 + 1) / 𝑛⦌𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))))) |
233 | | eluzelre 11574 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → 𝑖 ∈ ℝ) |
234 | 233 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑖 ∈ ℝ) |
235 | | eluzle 11576 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑖) |
236 | 235 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑀 ≤ 𝑖) |
237 | 32 | nnred 10912 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℝ) |
238 | 237 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ ℝ) |
239 | | elicopnf 12140 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℝ → (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀 ≤ 𝑖))) |
240 | 238, 239 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀 ≤ 𝑖))) |
241 | 234, 236,
240 | mpbir2and 959 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑖 ∈ (𝑀[,)+∞)) |
242 | 241 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑖 ∈ (ℤ≥‘𝑀) → 𝑖 ∈ (𝑀[,)+∞))) |
243 | 242 | ssrdv 3574 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(ℤ≥‘𝑀) ⊆ (𝑀[,)+∞)) |
244 | 32 | nnzd 11357 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈ ℤ) |
245 | 49 | peano2zd 11361 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐼 + 1) ∈ ℤ) |
246 | 103 | rpred 11748 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑈 ∈ ℝ) |
247 | 4 | nnred 10912 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐼 + 1) ∈ ℝ) |
248 | | dchrisumlem2.2 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ≤ 𝑈) |
249 | | dchrisumlem2.3 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑈 ≤ (𝐼 + 1)) |
250 | 237, 246,
247, 248, 249 | letrd 10073 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ≤ (𝐼 + 1)) |
251 | | eluz2 11569 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 + 1) ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝐼 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝐼 + 1))) |
252 | 244, 245,
250, 251 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐼 + 1) ∈
(ℤ≥‘𝑀)) |
253 | | uztrn 11580 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 + 1) ∈
(ℤ≥‘(𝐼 + 1)) ∧ (𝐼 + 1) ∈
(ℤ≥‘𝑀)) → (𝐽 + 1) ∈
(ℤ≥‘𝑀)) |
254 | 9, 252, 253 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐽 + 1) ∈
(ℤ≥‘𝑀)) |
255 | 243, 254 | sseldd 3569 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐽 + 1) ∈ (𝑀[,)+∞)) |
256 | 115 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐽 + 1) ∈ (𝑀[,)+∞) → 0 ≤
⦋(𝐽 + 1) /
𝑛⦌𝐴)) |
257 | 255, 256 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤
⦋(𝐽 + 1) /
𝑛⦌𝐴) |
258 | 117, 257 | absidd 14009 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(abs‘⦋(𝐽 + 1) / 𝑛⦌𝐴) = ⦋(𝐽 + 1) / 𝑛⦌𝐴) |
259 | 258 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝜑 →
((abs‘⦋(𝐽 + 1) / 𝑛⦌𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) = (⦋(𝐽 + 1) / 𝑛⦌𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))))) |
260 | 232, 259 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝜑 →
(abs‘(⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) = (⦋(𝐽 + 1) / 𝑛⦌𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))))) |
261 | 126 | abscld 14023 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) ∈ ℝ) |
262 | 113 | nnnn0d 11228 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐽 + 1) ∈
ℕ0) |
263 | | dchrisum.10 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |
264 | 19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263 | dchrisumlem1 24978 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐽 + 1) ∈ ℕ0) →
(abs‘Σ𝑛 ∈
(0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |
265 | 262, 264 | mpdan 699 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |
266 | 261, 95, 117, 257, 265 | lemul2ad 10843 |
. . . . . . . . . 10
⊢ (𝜑 → (⦋(𝐽 + 1) / 𝑛⦌𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ (⦋(𝐽 + 1) / 𝑛⦌𝐴 · 𝑅)) |
267 | 260, 266 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ (𝜑 →
(abs‘(⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ (⦋(𝐽 + 1) / 𝑛⦌𝐴 · 𝑅)) |
268 | 128, 133 | absmuld 14041 |
. . . . . . . . . . 11
⊢ (𝜑 →
(abs‘(⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) = ((abs‘⦋(𝐼 + 1) / 𝑛⦌𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) |
269 | 243, 252 | sseldd 3569 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐼 + 1) ∈ (𝑀[,)+∞)) |
270 | 19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36 | dchrisumlema 24977 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐼 + 1) ∈ ℝ+ →
⦋(𝐼 + 1) /
𝑛⦌𝐴 ∈ ℝ) ∧ ((𝐼 + 1) ∈ (𝑀[,)+∞) → 0 ≤
⦋(𝐼 + 1) /
𝑛⦌𝐴))) |
271 | 270 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐼 + 1) ∈ (𝑀[,)+∞) → 0 ≤
⦋(𝐼 + 1) /
𝑛⦌𝐴)) |
272 | 269, 271 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤
⦋(𝐼 + 1) /
𝑛⦌𝐴) |
273 | 101, 272 | absidd 14009 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(abs‘⦋(𝐼 + 1) / 𝑛⦌𝐴) = ⦋(𝐼 + 1) / 𝑛⦌𝐴) |
274 | 273 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝜑 →
((abs‘⦋(𝐼 + 1) / 𝑛⦌𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) = (⦋(𝐼 + 1) / 𝑛⦌𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) |
275 | 268, 274 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝜑 →
(abs‘(⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) = (⦋(𝐼 + 1) / 𝑛⦌𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) |
276 | 133 | abscld 14023 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))) ∈ ℝ) |
277 | 4 | nnnn0d 11228 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐼 + 1) ∈
ℕ0) |
278 | 19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263 | dchrisumlem1 24978 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐼 + 1) ∈ ℕ0) →
(abs‘Σ𝑛 ∈
(0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |
279 | 277, 278 | mpdan 699 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |
280 | 276, 95, 101, 272, 279 | lemul2ad 10843 |
. . . . . . . . . 10
⊢ (𝜑 → (⦋(𝐼 + 1) / 𝑛⦌𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ (⦋(𝐼 + 1) / 𝑛⦌𝐴 · 𝑅)) |
281 | 275, 280 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ (𝜑 →
(abs‘(⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ (⦋(𝐼 + 1) / 𝑛⦌𝐴 · 𝑅)) |
282 | 226, 227,
230, 231, 267, 281 | le2addd 10525 |
. . . . . . . 8
⊢ (𝜑 →
((abs‘(⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) + (abs‘(⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) ≤ ((⦋(𝐽 + 1) / 𝑛⦌𝐴 · 𝑅) + (⦋(𝐼 + 1) / 𝑛⦌𝐴 · 𝑅))) |
283 | 95 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ ℂ) |
284 | 118, 128,
283 | adddird 9944 |
. . . . . . . 8
⊢ (𝜑 → ((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) · 𝑅) = ((⦋(𝐽 + 1) / 𝑛⦌𝐴 · 𝑅) + (⦋(𝐼 + 1) / 𝑛⦌𝐴 · 𝑅))) |
285 | 282, 284 | breqtrrd 4611 |
. . . . . . 7
⊢ (𝜑 →
((abs‘(⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) + (abs‘(⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) ≤ ((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) · 𝑅)) |
286 | 136, 228,
218, 229, 285 | letrd 10073 |
. . . . . 6
⊢ (𝜑 →
(abs‘((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) ≤ ((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) · 𝑅)) |
287 | 156 | abscld 14023 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) →
(abs‘((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ∈ ℝ) |
288 | 83, 287 | fsumrecl 14312 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ∈ ℝ) |
289 | 83, 156 | fsumabs 14374 |
. . . . . . 7
⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))) |
290 | 95 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑅 ∈ ℝ) |
291 | 222, 290 | remulcld 9949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · 𝑅) ∈ ℝ) |
292 | 137, 148 | syldan 486 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ) |
293 | 153 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
294 | 292, 293 | absmuld 14041 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) →
(abs‘((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) = ((abs‘(⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴)) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))) |
295 | | elfzouz 12343 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1)) → 𝑖 ∈ (ℤ≥‘(𝐼 + 1))) |
296 | | uztrn 11580 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈
(ℤ≥‘(𝐼 + 1)) ∧ (𝐼 + 1) ∈
(ℤ≥‘𝑀)) → 𝑖 ∈ (ℤ≥‘𝑀)) |
297 | 295, 252,
296 | syl2anr 494 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ (ℤ≥‘𝑀)) |
298 | | eluznn 11634 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ ∧ 𝑖 ∈
(ℤ≥‘𝑀)) → 𝑖 ∈ ℕ) |
299 | 32, 298 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑖 ∈ ℕ) |
300 | 299, 139 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝑖 + 1) ∈
ℝ+) |
301 | 299 | nnrpd 11746 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑖 ∈ ℝ+) |
302 | 34 | 3expia 1259 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+))
→ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴)) |
303 | 302 | ralrimivva 2954 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑛 ∈ ℝ+ ∀𝑥 ∈ ℝ+
((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴)) |
304 | 303 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → ∀𝑛 ∈ ℝ+
∀𝑥 ∈
ℝ+ ((𝑀
≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴)) |
305 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑛ℝ+ |
306 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑛(𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) |
307 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑛𝐵 |
308 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑛
≤ |
309 | 307, 308,
60 | nfbr 4629 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑛 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴 |
310 | 306, 309 | nfim 1813 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑛((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) → 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴) |
311 | 305, 310 | nfral 2929 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛∀𝑥 ∈ ℝ+ ((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) → 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴) |
312 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑖 → (𝑀 ≤ 𝑛 ↔ 𝑀 ≤ 𝑖)) |
313 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑖 → (𝑛 ≤ 𝑥 ↔ 𝑖 ≤ 𝑥)) |
314 | 312, 313 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑖 → ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) ↔ (𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥))) |
315 | 64 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑖 → (𝐵 ≤ 𝐴 ↔ 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴)) |
316 | 314, 315 | imbi12d 333 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑖 → (((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) ↔ ((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) → 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴))) |
317 | 316 | ralbidv 2969 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑖 → (∀𝑥 ∈ ℝ+ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) ↔ ∀𝑥 ∈ ℝ+ ((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) → 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴))) |
318 | 311, 317 | rspc 3276 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℝ+
→ (∀𝑛 ∈
ℝ+ ∀𝑥 ∈ ℝ+ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) → ∀𝑥 ∈ ℝ+ ((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) → 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴))) |
319 | 301, 304,
318 | sylc 63 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → ∀𝑥 ∈ ℝ+
((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) → 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴)) |
320 | 234 | lep1d 10834 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑖 ≤ (𝑖 + 1)) |
321 | 236, 320 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝑀 ≤ 𝑖 ∧ 𝑖 ≤ (𝑖 + 1))) |
322 | | breq2 4587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑖 + 1) → (𝑖 ≤ 𝑥 ↔ 𝑖 ≤ (𝑖 + 1))) |
323 | 322 | anbi2d 736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑖 + 1) → ((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) ↔ (𝑀 ≤ 𝑖 ∧ 𝑖 ≤ (𝑖 + 1)))) |
324 | | eqvisset 3184 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝑖 + 1) → (𝑖 + 1) ∈ V) |
325 | | eqtr3 2631 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) → 𝑥 = 𝑛) |
326 | 31 | equcoms 1934 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑛 → 𝐴 = 𝐵) |
327 | 325, 326 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) → 𝐴 = 𝐵) |
328 | 324, 327 | csbied 3526 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑖 + 1) → ⦋(𝑖 + 1) / 𝑛⦌𝐴 = 𝐵) |
329 | 328 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑖 + 1) → 𝐵 = ⦋(𝑖 + 1) / 𝑛⦌𝐴) |
330 | 329 | breq1d 4593 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑖 + 1) → (𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴 ↔ ⦋(𝑖 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑖 / 𝑛⦌𝐴)) |
331 | 323, 330 | imbi12d 333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑖 + 1) → (((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) → 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴) ↔ ((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ (𝑖 + 1)) → ⦋(𝑖 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑖 / 𝑛⦌𝐴))) |
332 | 331 | rspcv 3278 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 + 1) ∈ ℝ+
→ (∀𝑥 ∈
ℝ+ ((𝑀
≤ 𝑖 ∧ 𝑖 ≤ 𝑥) → 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴) → ((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ (𝑖 + 1)) → ⦋(𝑖 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑖 / 𝑛⦌𝐴))) |
333 | 300, 319,
321, 332 | syl3c 64 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → ⦋(𝑖 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑖 / 𝑛⦌𝐴) |
334 | 297, 333 | syldan 486 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ⦋(𝑖 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑖 / 𝑛⦌𝐴) |
335 | 221, 220,
334 | abssuble0d 14019 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) →
(abs‘(⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴)) = (⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴)) |
336 | 335 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) →
((abs‘(⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴)) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) = ((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))) |
337 | 294, 336 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) →
(abs‘((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) = ((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))) |
338 | 293 | abscld 14023 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))) ∈ ℝ) |
339 | 220, 221 | subge0d 10496 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (0 ≤ (⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) ↔ ⦋(𝑖 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑖 / 𝑛⦌𝐴)) |
340 | 334, 339 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 0 ≤ (⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴)) |
341 | 137 | peano2nnd 10914 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) ∈ ℕ) |
342 | 341 | nnnn0d 11228 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) ∈
ℕ0) |
343 | 19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263 | dchrisumlem1 24978 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 + 1) ∈ ℕ0) →
(abs‘Σ𝑛 ∈
(0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |
344 | 342, 343 | syldan 486 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |
345 | 338, 290,
222, 340, 344 | lemul2ad 10843 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ ((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · 𝑅)) |
346 | 337, 345 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) →
(abs‘((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ ((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · 𝑅)) |
347 | 83, 287, 291, 346 | fsumle 14372 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · 𝑅)) |
348 | 222 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) ∈ ℂ) |
349 | 83, 283, 348 | fsummulc1 14359 |
. . . . . . . . 9
⊢ (𝜑 → (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · 𝑅) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · 𝑅)) |
350 | 219 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · 𝑅) = ((⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) · 𝑅)) |
351 | 349, 350 | eqtr3d 2646 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · 𝑅) = ((⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) · 𝑅)) |
352 | 347, 351 | breqtrd 4609 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ ((⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) · 𝑅)) |
353 | 158, 288,
225, 289, 352 | letrd 10073 |
. . . . . 6
⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ ((⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) · 𝑅)) |
354 | 136, 158,
218, 225, 286, 353 | le2addd 10525 |
. . . . 5
⊢ (𝜑 →
((abs‘((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))) ≤ (((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) · 𝑅) + ((⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) · 𝑅))) |
355 | 128 | 2timesd 11152 |
. . . . . . . 8
⊢ (𝜑 → (2 ·
⦋(𝐼 + 1) /
𝑛⦌𝐴) = (⦋(𝐼 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴)) |
356 | 128, 118,
128 | ppncand 10311 |
. . . . . . . 8
⊢ (𝜑 → ((⦋(𝐼 + 1) / 𝑛⦌𝐴 + ⦋(𝐽 + 1) / 𝑛⦌𝐴) + (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴)) = (⦋(𝐼 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴)) |
357 | 128, 118 | addcomd 10117 |
. . . . . . . . 9
⊢ (𝜑 → (⦋(𝐼 + 1) / 𝑛⦌𝐴 + ⦋(𝐽 + 1) / 𝑛⦌𝐴) = (⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴)) |
358 | 357 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝜑 → ((⦋(𝐼 + 1) / 𝑛⦌𝐴 + ⦋(𝐽 + 1) / 𝑛⦌𝐴) + (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴)) = ((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) + (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴))) |
359 | 355, 356,
358 | 3eqtr2d 2650 |
. . . . . . 7
⊢ (𝜑 → (2 ·
⦋(𝐼 + 1) /
𝑛⦌𝐴) = ((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) + (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴))) |
360 | 359 | oveq1d 6564 |
. . . . . 6
⊢ (𝜑 → ((2 ·
⦋(𝐼 + 1) /
𝑛⦌𝐴) · 𝑅) = (((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) + (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴)) · 𝑅)) |
361 | | 2cnd 10970 |
. . . . . . 7
⊢ (𝜑 → 2 ∈
ℂ) |
362 | 361, 128,
283 | mul32d 10125 |
. . . . . 6
⊢ (𝜑 → ((2 ·
⦋(𝐼 + 1) /
𝑛⦌𝐴) · 𝑅) = ((2 · 𝑅) · ⦋(𝐼 + 1) / 𝑛⦌𝐴)) |
363 | 217 | recnd 9947 |
. . . . . . 7
⊢ (𝜑 → (⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) ∈ ℂ) |
364 | 224 | recnd 9947 |
. . . . . . 7
⊢ (𝜑 → (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) ∈ ℂ) |
365 | 363, 364,
283 | adddird 9944 |
. . . . . 6
⊢ (𝜑 → (((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) + (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴)) · 𝑅) = (((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) · 𝑅) + ((⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) · 𝑅))) |
366 | 360, 362,
365 | 3eqtr3d 2652 |
. . . . 5
⊢ (𝜑 → ((2 · 𝑅) · ⦋(𝐼 + 1) / 𝑛⦌𝐴) = (((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) · 𝑅) + ((⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) · 𝑅))) |
367 | 354, 366 | breqtrrd 4611 |
. . . 4
⊢ (𝜑 →
((abs‘((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))) ≤ ((2 · 𝑅) · ⦋(𝐼 + 1) / 𝑛⦌𝐴)) |
368 | 92, 159, 102, 216, 367 | letrd 10073 |
. . 3
⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) ≤ ((2 · 𝑅) · ⦋(𝐼 + 1) / 𝑛⦌𝐴)) |
369 | | 2nn0 11186 |
. . . . . 6
⊢ 2 ∈
ℕ0 |
370 | | nn0ge0 11195 |
. . . . . 6
⊢ (2 ∈
ℕ0 → 0 ≤ 2) |
371 | 369, 370 | mp1i 13 |
. . . . 5
⊢ (𝜑 → 0 ≤ 2) |
372 | | 0red 9920 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ) |
373 | 126 | absge0d 14031 |
. . . . . 6
⊢ (𝜑 → 0 ≤
(abs‘Σ𝑛 ∈
(0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) |
374 | 372, 261,
95, 373, 265 | letrd 10073 |
. . . . 5
⊢ (𝜑 → 0 ≤ 𝑅) |
375 | 94, 95, 371, 374 | mulge0d 10483 |
. . . 4
⊢ (𝜑 → 0 ≤ (2 · 𝑅)) |
376 | 4 | nnrpd 11746 |
. . . . 5
⊢ (𝜑 → (𝐼 + 1) ∈
ℝ+) |
377 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑛(𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) |
378 | 307, 308,
105 | nfbr 4629 |
. . . . . . . . 9
⊢
Ⅎ𝑛 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴 |
379 | 377, 378 | nfim 1813 |
. . . . . . . 8
⊢
Ⅎ𝑛((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) → 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴) |
380 | 305, 379 | nfral 2929 |
. . . . . . 7
⊢
Ⅎ𝑛∀𝑥 ∈ ℝ+ ((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) → 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴) |
381 | | breq2 4587 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑈 → (𝑀 ≤ 𝑛 ↔ 𝑀 ≤ 𝑈)) |
382 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑈 → (𝑛 ≤ 𝑥 ↔ 𝑈 ≤ 𝑥)) |
383 | 381, 382 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑛 = 𝑈 → ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) ↔ (𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥))) |
384 | 107 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑛 = 𝑈 → (𝐵 ≤ 𝐴 ↔ 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴)) |
385 | 383, 384 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑛 = 𝑈 → (((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) ↔ ((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) → 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴))) |
386 | 385 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑛 = 𝑈 → (∀𝑥 ∈ ℝ+ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) ↔ ∀𝑥 ∈ ℝ+ ((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) → 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴))) |
387 | 380, 386 | rspc 3276 |
. . . . . 6
⊢ (𝑈 ∈ ℝ+
→ (∀𝑛 ∈
ℝ+ ∀𝑥 ∈ ℝ+ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) → ∀𝑥 ∈ ℝ+ ((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) → 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴))) |
388 | 103, 303,
387 | sylc 63 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) → 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴)) |
389 | 248, 249 | jca 553 |
. . . . 5
⊢ (𝜑 → (𝑀 ≤ 𝑈 ∧ 𝑈 ≤ (𝐼 + 1))) |
390 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑥 = (𝐼 + 1) → (𝑈 ≤ 𝑥 ↔ 𝑈 ≤ (𝐼 + 1))) |
391 | 390 | anbi2d 736 |
. . . . . . 7
⊢ (𝑥 = (𝐼 + 1) → ((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) ↔ (𝑀 ≤ 𝑈 ∧ 𝑈 ≤ (𝐼 + 1)))) |
392 | | eqvisset 3184 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐼 + 1) → (𝐼 + 1) ∈ V) |
393 | | eqtr3 2631 |
. . . . . . . . . . 11
⊢ ((𝑥 = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) → 𝑥 = 𝑛) |
394 | 393, 326 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑥 = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) → 𝐴 = 𝐵) |
395 | 392, 394 | csbied 3526 |
. . . . . . . . 9
⊢ (𝑥 = (𝐼 + 1) → ⦋(𝐼 + 1) / 𝑛⦌𝐴 = 𝐵) |
396 | 395 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝑥 = (𝐼 + 1) → 𝐵 = ⦋(𝐼 + 1) / 𝑛⦌𝐴) |
397 | 396 | breq1d 4593 |
. . . . . . 7
⊢ (𝑥 = (𝐼 + 1) → (𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴 ↔ ⦋(𝐼 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑈 / 𝑛⦌𝐴)) |
398 | 391, 397 | imbi12d 333 |
. . . . . 6
⊢ (𝑥 = (𝐼 + 1) → (((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) → 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴) ↔ ((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ (𝐼 + 1)) → ⦋(𝐼 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑈 / 𝑛⦌𝐴))) |
399 | 398 | rspcv 3278 |
. . . . 5
⊢ ((𝐼 + 1) ∈ ℝ+
→ (∀𝑥 ∈
ℝ+ ((𝑀
≤ 𝑈 ∧ 𝑈 ≤ 𝑥) → 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴) → ((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ (𝐼 + 1)) → ⦋(𝐼 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑈 / 𝑛⦌𝐴))) |
400 | 376, 388,
389, 399 | syl3c 64 |
. . . 4
⊢ (𝜑 → ⦋(𝐼 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑈 / 𝑛⦌𝐴) |
401 | 101, 110,
96, 375, 400 | lemul2ad 10843 |
. . 3
⊢ (𝜑 → ((2 · 𝑅) · ⦋(𝐼 + 1) / 𝑛⦌𝐴) ≤ ((2 · 𝑅) · ⦋𝑈 / 𝑛⦌𝐴)) |
402 | 92, 102, 111, 368, 401 | letrd 10073 |
. 2
⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) ≤ ((2 · 𝑅) · ⦋𝑈 / 𝑛⦌𝐴)) |
403 | 91, 402 | eqbrtrd 4605 |
1
⊢ (𝜑 → (abs‘((seq1( + ,
𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) ≤ ((2 · 𝑅) · ⦋𝑈 / 𝑛⦌𝐴)) |