MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrisumlem2 Structured version   Visualization version   GIF version

Theorem dchrisumlem2 25224
Description: Lemma for dchrisum 25226. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.)
Hypotheses
Ref Expression
rpvmasum.z 𝑍 = (ℤ/nℤ‘𝑁)
rpvmasum.l 𝐿 = (ℤRHom‘𝑍)
rpvmasum.a (𝜑𝑁 ∈ ℕ)
rpvmasum.g 𝐺 = (DChr‘𝑁)
rpvmasum.d 𝐷 = (Base‘𝐺)
rpvmasum.1 1 = (0g𝐺)
dchrisum.b (𝜑𝑋𝐷)
dchrisum.n1 (𝜑𝑋1 )
dchrisum.2 (𝑛 = 𝑥𝐴 = 𝐵)
dchrisum.3 (𝜑𝑀 ∈ ℕ)
dchrisum.4 ((𝜑𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)
dchrisum.5 ((𝜑 ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+) ∧ (𝑀𝑛𝑛𝑥)) → 𝐵𝐴)
dchrisum.6 (𝜑 → (𝑛 ∈ ℝ+𝐴) ⇝𝑟 0)
dchrisum.7 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿𝑛)) · 𝐴))
dchrisum.9 (𝜑𝑅 ∈ ℝ)
dchrisum.10 (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅)
dchrisumlem2.1 (𝜑𝑈 ∈ ℝ+)
dchrisumlem2.2 (𝜑𝑀𝑈)
dchrisumlem2.3 (𝜑𝑈 ≤ (𝐼 + 1))
dchrisumlem2.4 (𝜑𝐼 ∈ ℕ)
dchrisumlem2.5 (𝜑𝐽 ∈ (ℤ𝐼))
Assertion
Ref Expression
dchrisumlem2 (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) ≤ ((2 · 𝑅) · 𝑈 / 𝑛𝐴))
Distinct variable groups:   𝑢,𝑛,𝑥   1 ,𝑛,𝑥   𝑛,𝐹,𝑢,𝑥   𝑛,𝐼,𝑢,𝑥   𝑛,𝐽,𝑢,𝑥   𝑥,𝐴   𝑛,𝑁,𝑢,𝑥   𝜑,𝑛,𝑢,𝑥   𝑅,𝑛,𝑢,𝑥   𝑈,𝑛,𝑢,𝑥   𝐵,𝑛   𝑛,𝑍,𝑥   𝐷,𝑛,𝑥   𝑛,𝐿,𝑢,𝑥   𝑛,𝑀,𝑢,𝑥   𝑛,𝑋,𝑢,𝑥
Allowed substitution hints:   𝐴(𝑢,𝑛)   𝐵(𝑥,𝑢)   𝐷(𝑢)   1 (𝑢)   𝐺(𝑥,𝑢,𝑛)   𝑍(𝑢)

Proof of Theorem dchrisumlem2
Dummy variables 𝑘 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzodisj 12541 . . . . . . . . 9 ((1..^(𝐼 + 1)) ∩ ((𝐼 + 1)..^(𝐽 + 1))) = ∅
21a1i 11 . . . . . . . 8 (𝜑 → ((1..^(𝐼 + 1)) ∩ ((𝐼 + 1)..^(𝐽 + 1))) = ∅)
3 dchrisumlem2.4 . . . . . . . . . . . 12 (𝜑𝐼 ∈ ℕ)
43peano2nnd 11075 . . . . . . . . . . 11 (𝜑 → (𝐼 + 1) ∈ ℕ)
5 nnuz 11761 . . . . . . . . . . 11 ℕ = (ℤ‘1)
64, 5syl6eleq 2740 . . . . . . . . . 10 (𝜑 → (𝐼 + 1) ∈ (ℤ‘1))
7 dchrisumlem2.5 . . . . . . . . . . 11 (𝜑𝐽 ∈ (ℤ𝐼))
8 eluzp1p1 11751 . . . . . . . . . . 11 (𝐽 ∈ (ℤ𝐼) → (𝐽 + 1) ∈ (ℤ‘(𝐼 + 1)))
97, 8syl 17 . . . . . . . . . 10 (𝜑 → (𝐽 + 1) ∈ (ℤ‘(𝐼 + 1)))
10 elfzuzb 12374 . . . . . . . . . 10 ((𝐼 + 1) ∈ (1...(𝐽 + 1)) ↔ ((𝐼 + 1) ∈ (ℤ‘1) ∧ (𝐽 + 1) ∈ (ℤ‘(𝐼 + 1))))
116, 9, 10sylanbrc 699 . . . . . . . . 9 (𝜑 → (𝐼 + 1) ∈ (1...(𝐽 + 1)))
12 fzosplit 12540 . . . . . . . . 9 ((𝐼 + 1) ∈ (1...(𝐽 + 1)) → (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1))))
1311, 12syl 17 . . . . . . . 8 (𝜑 → (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1))))
14 fzofi 12813 . . . . . . . . 9 (1..^(𝐽 + 1)) ∈ Fin
1514a1i 11 . . . . . . . 8 (𝜑 → (1..^(𝐽 + 1)) ∈ Fin)
16 elfzouz 12513 . . . . . . . . . 10 (𝑖 ∈ (1..^(𝐽 + 1)) → 𝑖 ∈ (ℤ‘1))
1716, 5syl6eleqr 2741 . . . . . . . . 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 (𝜑𝑋𝐷)
2322adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 𝑋𝐷)
24 nnz 11437 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → 𝑖 ∈ ℤ)
2524adantl 481 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℤ)
2618, 19, 20, 21, 23, 25dchrzrhcl 25015 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → (𝑋‘(𝐿𝑖)) ∈ ℂ)
27 nnrp 11880 . . . . . . . . . . . . 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 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿𝑛)) · 𝐴))
3719, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36dchrisumlema 25222 . . . . . . . . . . . . . 14 (𝜑 → ((𝑖 ∈ ℝ+𝑖 / 𝑛𝐴 ∈ ℝ) ∧ (𝑖 ∈ (𝑀[,)+∞) → 0 ≤ 𝑖 / 𝑛𝐴)))
3837simpld 474 . . . . . . . . . . . . 13 (𝜑 → (𝑖 ∈ ℝ+𝑖 / 𝑛𝐴 ∈ ℝ))
3927, 38syl5 34 . . . . . . . . . . . 12 (𝜑 → (𝑖 ∈ ℕ → 𝑖 / 𝑛𝐴 ∈ ℝ))
4039imp 444 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 𝑖 / 𝑛𝐴 ∈ ℝ)
4140recnd 10106 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → 𝑖 / 𝑛𝐴 ∈ ℂ)
4226, 41mulcld 10098 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
4317, 42sylan2 490 . . . . . . . 8 ((𝜑𝑖 ∈ (1..^(𝐽 + 1))) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
442, 13, 15, 43fsumsplit 14515 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (1..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
45 eluzelz 11735 . . . . . . . . 9 (𝐽 ∈ (ℤ𝐼) → 𝐽 ∈ ℤ)
46 fzval3 12576 . . . . . . . . 9 (𝐽 ∈ ℤ → (1...𝐽) = (1..^(𝐽 + 1)))
477, 45, 463syl 18 . . . . . . . 8 (𝜑 → (1...𝐽) = (1..^(𝐽 + 1)))
4847sumeq1d 14475 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = Σ𝑖 ∈ (1..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
493nnzd 11519 . . . . . . . . . 10 (𝜑𝐼 ∈ ℤ)
50 fzval3 12576 . . . . . . . . . 10 (𝐼 ∈ ℤ → (1...𝐼) = (1..^(𝐼 + 1)))
5149, 50syl 17 . . . . . . . . 9 (𝜑 → (1...𝐼) = (1..^(𝐼 + 1)))
5251sumeq1d 14475 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
5352oveq1d 6705 . . . . . . 7 (𝜑 → (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
5444, 48, 533eqtr4d 2695 . . . . . 6 (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
55 elfznn 12408 . . . . . . . 8 (𝑖 ∈ (1...𝐽) → 𝑖 ∈ ℕ)
56 simpr 476 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
57 nfcv 2793 . . . . . . . . . 10 𝑛𝑖
58 nfcv 2793 . . . . . . . . . . 11 𝑛(𝑋‘(𝐿𝑖))
59 nfcv 2793 . . . . . . . . . . 11 𝑛 ·
60 nfcsb1v 3582 . . . . . . . . . . 11 𝑛𝑖 / 𝑛𝐴
6158, 59, 60nfov 6716 . . . . . . . . . 10 𝑛((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)
62 fveq2 6229 . . . . . . . . . . . 12 (𝑛 = 𝑖 → (𝐿𝑛) = (𝐿𝑖))
6362fveq2d 6233 . . . . . . . . . . 11 (𝑛 = 𝑖 → (𝑋‘(𝐿𝑛)) = (𝑋‘(𝐿𝑖)))
64 csbeq1a 3575 . . . . . . . . . . 11 (𝑛 = 𝑖𝐴 = 𝑖 / 𝑛𝐴)
6563, 64oveq12d 6708 . . . . . . . . . 10 (𝑛 = 𝑖 → ((𝑋‘(𝐿𝑛)) · 𝐴) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
6657, 61, 65, 36fvmptf 6340 . . . . . . . . 9 ((𝑖 ∈ ℕ ∧ ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
6756, 42, 66syl2anc 694 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
6855, 67sylan2 490 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝐽)) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
693, 5syl6eleq 2740 . . . . . . . 8 (𝜑𝐼 ∈ (ℤ‘1))
70 uztrn 11742 . . . . . . . 8 ((𝐽 ∈ (ℤ𝐼) ∧ 𝐼 ∈ (ℤ‘1)) → 𝐽 ∈ (ℤ‘1))
717, 69, 70syl2anc 694 . . . . . . 7 (𝜑𝐽 ∈ (ℤ‘1))
7255, 42sylan2 490 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝐽)) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
7368, 71, 72fsumser 14505 . . . . . 6 (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (seq1( + , 𝐹)‘𝐽))
7454, 73eqtr3d 2687 . . . . 5 (𝜑 → (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = (seq1( + , 𝐹)‘𝐽))
75 elfznn 12408 . . . . . . 7 (𝑖 ∈ (1...𝐼) → 𝑖 ∈ ℕ)
7675, 67sylan2 490 . . . . . 6 ((𝜑𝑖 ∈ (1...𝐼)) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
7775, 42sylan2 490 . . . . . 6 ((𝜑𝑖 ∈ (1...𝐼)) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
7876, 69, 77fsumser 14505 . . . . 5 (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (seq1( + , 𝐹)‘𝐼))
7974, 78oveq12d 6708 . . . 4 (𝜑 → ((Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) − Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = ((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼)))
80 fzfid 12812 . . . . . 6 (𝜑 → (1...𝐼) ∈ Fin)
8180, 77fsumcl 14508 . . . . 5 (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
82 fzofi 12813 . . . . . . 7 ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin
8382a1i 11 . . . . . 6 (𝜑 → ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin)
84 ssun2 3810 . . . . . . . . 9 ((𝐼 + 1)..^(𝐽 + 1)) ⊆ ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1)))
8584, 13syl5sseqr 3687 . . . . . . . 8 (𝜑 → ((𝐼 + 1)..^(𝐽 + 1)) ⊆ (1..^(𝐽 + 1)))
8685sselda 3636 . . . . . . 7 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ (1..^(𝐽 + 1)))
8786, 43syldan 486 . . . . . 6 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
8883, 87fsumcl 14508 . . . . 5 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
8981, 88pncan2d 10432 . . . 4 (𝜑 → ((Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) − Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
9079, 89eqtr3d 2687 . . 3 (𝜑 → ((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
9190fveq2d 6233 . 2 (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) = (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
9288abscld 14219 . . 3 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ∈ ℝ)
93 2re 11128 . . . . . 6 2 ∈ ℝ
9493a1i 11 . . . . 5 (𝜑 → 2 ∈ ℝ)
95 dchrisum.9 . . . . 5 (𝜑𝑅 ∈ ℝ)
9694, 95remulcld 10108 . . . 4 (𝜑 → (2 · 𝑅) ∈ ℝ)
9740ralrimiva 2995 . . . . 5 (𝜑 → ∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℝ)
98 csbeq1 3569 . . . . . . 7 (𝑖 = (𝐼 + 1) → 𝑖 / 𝑛𝐴 = (𝐼 + 1) / 𝑛𝐴)
9998eleq1d 2715 . . . . . 6 (𝑖 = (𝐼 + 1) → (𝑖 / 𝑛𝐴 ∈ ℝ ↔ (𝐼 + 1) / 𝑛𝐴 ∈ ℝ))
10099rspcv 3336 . . . . 5 ((𝐼 + 1) ∈ ℕ → (∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℝ → (𝐼 + 1) / 𝑛𝐴 ∈ ℝ))
1014, 97, 100sylc 65 . . . 4 (𝜑(𝐼 + 1) / 𝑛𝐴 ∈ ℝ)
10296, 101remulcld 10108 . . 3 (𝜑 → ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴) ∈ ℝ)
103 dchrisumlem2.1 . . . . 5 (𝜑𝑈 ∈ ℝ+)
10433ralrimiva 2995 . . . . 5 (𝜑 → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ)
105 nfcsb1v 3582 . . . . . . 7 𝑛𝑈 / 𝑛𝐴
106105nfel1 2808 . . . . . 6 𝑛𝑈 / 𝑛𝐴 ∈ ℝ
107 csbeq1a 3575 . . . . . . 7 (𝑛 = 𝑈𝐴 = 𝑈 / 𝑛𝐴)
108107eleq1d 2715 . . . . . 6 (𝑛 = 𝑈 → (𝐴 ∈ ℝ ↔ 𝑈 / 𝑛𝐴 ∈ ℝ))
109106, 108rspc 3334 . . . . 5 (𝑈 ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → 𝑈 / 𝑛𝐴 ∈ ℝ))
110103, 104, 109sylc 65 . . . 4 (𝜑𝑈 / 𝑛𝐴 ∈ ℝ)
11196, 110remulcld 10108 . . 3 (𝜑 → ((2 · 𝑅) · 𝑈 / 𝑛𝐴) ∈ ℝ)
11271, 5syl6eleqr 2741 . . . . . . . . . . . 12 (𝜑𝐽 ∈ ℕ)
113112peano2nnd 11075 . . . . . . . . . . 11 (𝜑 → (𝐽 + 1) ∈ ℕ)
114113nnrpd 11908 . . . . . . . . . 10 (𝜑 → (𝐽 + 1) ∈ ℝ+)
11519, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36dchrisumlema 25222 . . . . . . . . . . 11 (𝜑 → (((𝐽 + 1) ∈ ℝ+(𝐽 + 1) / 𝑛𝐴 ∈ ℝ) ∧ ((𝐽 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐽 + 1) / 𝑛𝐴)))
116115simpld 474 . . . . . . . . . 10 (𝜑 → ((𝐽 + 1) ∈ ℝ+(𝐽 + 1) / 𝑛𝐴 ∈ ℝ))
117114, 116mpd 15 . . . . . . . . 9 (𝜑(𝐽 + 1) / 𝑛𝐴 ∈ ℝ)
118117recnd 10106 . . . . . . . 8 (𝜑(𝐽 + 1) / 𝑛𝐴 ∈ ℂ)
119 fzofi 12813 . . . . . . . . . 10 (0..^(𝐽 + 1)) ∈ Fin
120119a1i 11 . . . . . . . . 9 (𝜑 → (0..^(𝐽 + 1)) ∈ Fin)
121 elfzoelz 12509 . . . . . . . . . 10 (𝑛 ∈ (0..^(𝐽 + 1)) → 𝑛 ∈ ℤ)
12222adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℤ) → 𝑋𝐷)
123 simpr 476 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℤ) → 𝑛 ∈ ℤ)
12418, 19, 20, 21, 122, 123dchrzrhcl 25015 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℤ) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
125121, 124sylan2 490 . . . . . . . . 9 ((𝜑𝑛 ∈ (0..^(𝐽 + 1))) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
126120, 125fsumcl 14508 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
127118, 126mulcld 10098 . . . . . . 7 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
128101recnd 10106 . . . . . . . 8 (𝜑(𝐼 + 1) / 𝑛𝐴 ∈ ℂ)
129 fzofi 12813 . . . . . . . . . 10 (0..^(𝐼 + 1)) ∈ Fin
130129a1i 11 . . . . . . . . 9 (𝜑 → (0..^(𝐼 + 1)) ∈ Fin)
131 elfzoelz 12509 . . . . . . . . . 10 (𝑛 ∈ (0..^(𝐼 + 1)) → 𝑛 ∈ ℤ)
132131, 124sylan2 490 . . . . . . . . 9 ((𝜑𝑛 ∈ (0..^(𝐼 + 1))) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
133130, 132fsumcl 14508 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
134128, 133mulcld 10098 . . . . . . 7 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
135127, 134subcld 10430 . . . . . 6 (𝜑 → (((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℂ)
136135abscld 14219 . . . . 5 (𝜑 → (abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ∈ ℝ)
13786, 17syl 17 . . . . . . . 8 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ ℕ)
138 peano2nn 11070 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℕ)
139138nnrpd 11908 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℝ+)
140 nfcsb1v 3582 . . . . . . . . . . . . . . 15 𝑛(𝑖 + 1) / 𝑛𝐴
141140nfel1 2808 . . . . . . . . . . . . . 14 𝑛(𝑖 + 1) / 𝑛𝐴 ∈ ℝ
142 csbeq1a 3575 . . . . . . . . . . . . . . 15 (𝑛 = (𝑖 + 1) → 𝐴 = (𝑖 + 1) / 𝑛𝐴)
143142eleq1d 2715 . . . . . . . . . . . . . 14 (𝑛 = (𝑖 + 1) → (𝐴 ∈ ℝ ↔ (𝑖 + 1) / 𝑛𝐴 ∈ ℝ))
144141, 143rspc 3334 . . . . . . . . . . . . 13 ((𝑖 + 1) ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ))
145144impcom 445 . . . . . . . . . . . 12 ((∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ ∧ (𝑖 + 1) ∈ ℝ+) → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ)
146104, 139, 145syl2an 493 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ)
147146, 40resubcld 10496 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → ((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) ∈ ℝ)
148147recnd 10106 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) ∈ ℂ)
149 fzofi 12813 . . . . . . . . . . . 12 (0..^(𝑖 + 1)) ∈ Fin
150149a1i 11 . . . . . . . . . . 11 (𝜑 → (0..^(𝑖 + 1)) ∈ Fin)
151 elfzoelz 12509 . . . . . . . . . . . 12 (𝑛 ∈ (0..^(𝑖 + 1)) → 𝑛 ∈ ℤ)
152151, 124sylan2 490 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (0..^(𝑖 + 1))) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
153150, 152fsumcl 14508 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
154153adantr 480 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
155148, 154mulcld 10098 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ) → (((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
156137, 155syldan 486 . . . . . . 7 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
15783, 156fsumcl 14508 . . . . . 6 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
158157abscld 14219 . . . . 5 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
159136, 158readdcld 10107 . . . 4 (𝜑 → ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))) ∈ ℝ)
16026, 41mulcomd 10099 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (𝑖 / 𝑛𝐴 · (𝑋‘(𝐿𝑖))))
161 nnnn0 11337 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → 𝑖 ∈ ℕ0)
162161adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ0)
163 nn0uz 11760 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
164162, 163syl6eleq 2740 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ (ℤ‘0))
165 elfzelz 12380 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0...𝑖) → 𝑛 ∈ ℤ)
166124adantlr 751 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
167165, 166sylan2 490 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ ℕ) ∧ 𝑛 ∈ (0...𝑖)) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
168164, 167, 63fzosump1 14525 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) = (Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) + (𝑋‘(𝐿𝑖))))
169168oveq1d 6705 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))) = ((Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) + (𝑋‘(𝐿𝑖))) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))))
170 fzofi 12813 . . . . . . . . . . . . . . 15 (0..^𝑖) ∈ Fin
171170a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → (0..^𝑖) ∈ Fin)
172 elfzoelz 12509 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0..^𝑖) → 𝑛 ∈ ℤ)
173172, 166sylan2 490 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ ℕ) ∧ 𝑛 ∈ (0..^𝑖)) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
174171, 173fsumcl 14508 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) ∈ ℂ)
175174, 26pncan2d 10432 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) + (𝑋‘(𝐿𝑖))) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))) = (𝑋‘(𝐿𝑖)))
176169, 175eqtr2d 2686 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (𝑋‘(𝐿𝑖)) = (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))))
177176oveq2d 6706 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → (𝑖 / 𝑛𝐴 · (𝑋‘(𝐿𝑖))) = (𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
178160, 177eqtrd 2685 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
179137, 178syldan 486 . . . . . . . 8 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
180179sumeq2dv 14477 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
181 csbeq1 3569 . . . . . . . . 9 (𝑘 = 𝑖𝑘 / 𝑛𝐴 = 𝑖 / 𝑛𝐴)
182 oveq2 6698 . . . . . . . . . 10 (𝑘 = 𝑖 → (0..^𝑘) = (0..^𝑖))
183182sumeq1d 14475 . . . . . . . . 9 (𝑘 = 𝑖 → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))
184181, 183jca 553 . . . . . . . 8 (𝑘 = 𝑖 → (𝑘 / 𝑛𝐴 = 𝑖 / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))))
185 csbeq1 3569 . . . . . . . . 9 (𝑘 = (𝑖 + 1) → 𝑘 / 𝑛𝐴 = (𝑖 + 1) / 𝑛𝐴)
186 oveq2 6698 . . . . . . . . . 10 (𝑘 = (𝑖 + 1) → (0..^𝑘) = (0..^(𝑖 + 1)))
187186sumeq1d 14475 . . . . . . . . 9 (𝑘 = (𝑖 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))
188185, 187jca 553 . . . . . . . 8 (𝑘 = (𝑖 + 1) → (𝑘 / 𝑛𝐴 = (𝑖 + 1) / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))
189 csbeq1 3569 . . . . . . . . 9 (𝑘 = (𝐼 + 1) → 𝑘 / 𝑛𝐴 = (𝐼 + 1) / 𝑛𝐴)
190 oveq2 6698 . . . . . . . . . 10 (𝑘 = (𝐼 + 1) → (0..^𝑘) = (0..^(𝐼 + 1)))
191190sumeq1d 14475 . . . . . . . . 9 (𝑘 = (𝐼 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))
192189, 191jca 553 . . . . . . . 8 (𝑘 = (𝐼 + 1) → (𝑘 / 𝑛𝐴 = (𝐼 + 1) / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))
193 csbeq1 3569 . . . . . . . . 9 (𝑘 = (𝐽 + 1) → 𝑘 / 𝑛𝐴 = (𝐽 + 1) / 𝑛𝐴)
194 oveq2 6698 . . . . . . . . . 10 (𝑘 = (𝐽 + 1) → (0..^𝑘) = (0..^(𝐽 + 1)))
195194sumeq1d 14475 . . . . . . . . 9 (𝑘 = (𝐽 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))
196193, 195jca 553 . . . . . . . 8 (𝑘 = (𝐽 + 1) → (𝑘 / 𝑛𝐴 = (𝐽 + 1) / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))))
197 elfzuz 12376 . . . . . . . . . 10 (𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1)) → 𝑘 ∈ (ℤ‘(𝐼 + 1)))
198 eluznn 11796 . . . . . . . . . 10 (((𝐼 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(𝐼 + 1))) → 𝑘 ∈ ℕ)
1994, 197, 198syl2an 493 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → 𝑘 ∈ ℕ)
20041ralrimiva 2995 . . . . . . . . . 10 (𝜑 → ∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℂ)
201 csbeq1 3569 . . . . . . . . . . . 12 (𝑖 = 𝑘𝑖 / 𝑛𝐴 = 𝑘 / 𝑛𝐴)
202201eleq1d 2715 . . . . . . . . . . 11 (𝑖 = 𝑘 → (𝑖 / 𝑛𝐴 ∈ ℂ ↔ 𝑘 / 𝑛𝐴 ∈ ℂ))
203202rspccva 3339 . . . . . . . . . 10 ((∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) → 𝑘 / 𝑛𝐴 ∈ ℂ)
204200, 203sylan 487 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 𝑘 / 𝑛𝐴 ∈ ℂ)
205199, 204syldan 486 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → 𝑘 / 𝑛𝐴 ∈ ℂ)
206 fzofi 12813 . . . . . . . . . . 11 (0..^𝑘) ∈ Fin
207206a1i 11 . . . . . . . . . 10 (𝜑 → (0..^𝑘) ∈ Fin)
208 elfzoelz 12509 . . . . . . . . . . 11 (𝑛 ∈ (0..^𝑘) → 𝑛 ∈ ℤ)
209208, 124sylan2 490 . . . . . . . . . 10 ((𝜑𝑛 ∈ (0..^𝑘)) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
210207, 209fsumcl 14508 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) ∈ ℂ)
211210adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) ∈ ℂ)
212184, 188, 192, 196, 9, 205, 211fsumparts 14582 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))) = ((((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
213180, 212eqtrd 2685 . . . . . 6 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = ((((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
214213fveq2d 6233 . . . . 5 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = (abs‘((((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))))
215135, 157abs2dif2d 14241 . . . . 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))(𝑋‘(𝐿𝑛))))))
216214, 215eqbrtrd 4707 . . . 4 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ≤ ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))))
217117, 101readdcld 10107 . . . . . . 7 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) ∈ ℝ)
218217, 95remulcld 10108 . . . . . 6 (𝜑 → (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) ∈ ℝ)
219181, 185, 189, 193, 9, 205telfsumo 14578 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) = ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴))
220137, 40syldan 486 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 / 𝑛𝐴 ∈ ℝ)
221137, 146syldan 486 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ)
222220, 221resubcld 10496 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ∈ ℝ)
22383, 222fsumrecl 14509 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ∈ ℝ)
224219, 223eqeltrrd 2731 . . . . . . 7 (𝜑 → ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) ∈ ℝ)
225224, 95remulcld 10108 . . . . . 6 (𝜑 → (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅) ∈ ℝ)
226127abscld 14219 . . . . . . . 8 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
227134abscld 14219 . . . . . . . 8 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
228226, 227readdcld 10107 . . . . . . 7 (𝜑 → ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ∈ ℝ)
229127, 134abs2dif2d 14241 . . . . . . 7 (𝜑 → (abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))))
230117, 95remulcld 10108 . . . . . . . . 9 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 · 𝑅) ∈ ℝ)
231101, 95remulcld 10108 . . . . . . . . 9 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 · 𝑅) ∈ ℝ)
232118, 126absmuld 14237 . . . . . . . . . . 11 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) = ((abs‘(𝐽 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))))
233 eluzelre 11736 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (ℤ𝑀) → 𝑖 ∈ ℝ)
234233adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℝ)
235 eluzle 11738 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (ℤ𝑀) → 𝑀𝑖)
236235adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀𝑖)
23732nnred 11073 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℝ)
238237adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ)
239 elicopnf 12307 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℝ → (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀𝑖)))
240238, 239syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀𝑖)))
241234, 236, 240mpbir2and 977 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ (𝑀[,)+∞))
242241ex 449 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑖 ∈ (ℤ𝑀) → 𝑖 ∈ (𝑀[,)+∞)))
243242ssrdv 3642 . . . . . . . . . . . . . . 15 (𝜑 → (ℤ𝑀) ⊆ (𝑀[,)+∞))
24432nnzd 11519 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℤ)
24549peano2zd 11523 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐼 + 1) ∈ ℤ)
246103rpred 11910 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 ∈ ℝ)
2474nnred 11073 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐼 + 1) ∈ ℝ)
248 dchrisumlem2.2 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀𝑈)
249 dchrisumlem2.3 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 ≤ (𝐼 + 1))
250237, 246, 247, 248, 249letrd 10232 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ≤ (𝐼 + 1))
251 eluz2 11731 . . . . . . . . . . . . . . . . 17 ((𝐼 + 1) ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝐼 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝐼 + 1)))
252244, 245, 250, 251syl3anbrc 1265 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐼 + 1) ∈ (ℤ𝑀))
253 uztrn 11742 . . . . . . . . . . . . . . . 16 (((𝐽 + 1) ∈ (ℤ‘(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (ℤ𝑀)) → (𝐽 + 1) ∈ (ℤ𝑀))
2549, 252, 253syl2anc 694 . . . . . . . . . . . . . . 15 (𝜑 → (𝐽 + 1) ∈ (ℤ𝑀))
255243, 254sseldd 3637 . . . . . . . . . . . . . 14 (𝜑 → (𝐽 + 1) ∈ (𝑀[,)+∞))
256115simprd 478 . . . . . . . . . . . . . 14 (𝜑 → ((𝐽 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐽 + 1) / 𝑛𝐴))
257255, 256mpd 15 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ (𝐽 + 1) / 𝑛𝐴)
258117, 257absidd 14205 . . . . . . . . . . . 12 (𝜑 → (abs‘(𝐽 + 1) / 𝑛𝐴) = (𝐽 + 1) / 𝑛𝐴)
259258oveq1d 6705 . . . . . . . . . . 11 (𝜑 → ((abs‘(𝐽 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐽 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))))
260232, 259eqtrd 2685 . . . . . . . . . 10 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐽 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))))
261126abscld 14219 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ∈ ℝ)
262113nnnn0d 11389 . . . . . . . . . . . 12 (𝜑 → (𝐽 + 1) ∈ ℕ0)
263 dchrisum.10 . . . . . . . . . . . . 13 (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅)
26419, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263dchrisumlem1 25223 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐽 + 1) ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
265262, 264mpdan 703 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
266261, 95, 117, 257, 265lemul2ad 11002 . . . . . . . . . 10 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐽 + 1) / 𝑛𝐴 · 𝑅))
267260, 266eqbrtrd 4707 . . . . . . . . 9 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐽 + 1) / 𝑛𝐴 · 𝑅))
268128, 133absmuld 14237 . . . . . . . . . . 11 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) = ((abs‘(𝐼 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))))
269243, 252sseldd 3637 . . . . . . . . . . . . . 14 (𝜑 → (𝐼 + 1) ∈ (𝑀[,)+∞))
27019, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36dchrisumlema 25222 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐼 + 1) ∈ ℝ+(𝐼 + 1) / 𝑛𝐴 ∈ ℝ) ∧ ((𝐼 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐼 + 1) / 𝑛𝐴)))
271270simprd 478 . . . . . . . . . . . . . 14 (𝜑 → ((𝐼 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐼 + 1) / 𝑛𝐴))
272269, 271mpd 15 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ (𝐼 + 1) / 𝑛𝐴)
273101, 272absidd 14205 . . . . . . . . . . . 12 (𝜑 → (abs‘(𝐼 + 1) / 𝑛𝐴) = (𝐼 + 1) / 𝑛𝐴)
274273oveq1d 6705 . . . . . . . . . . 11 (𝜑 → ((abs‘(𝐼 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐼 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))))
275268, 274eqtrd 2685 . . . . . . . . . 10 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐼 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))))
276133abscld 14219 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ∈ ℝ)
2774nnnn0d 11389 . . . . . . . . . . . 12 (𝜑 → (𝐼 + 1) ∈ ℕ0)
27819, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263dchrisumlem1 25223 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐼 + 1) ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
279277, 278mpdan 703 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
280276, 95, 101, 272, 279lemul2ad 11002 . . . . . . . . . 10 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐼 + 1) / 𝑛𝐴 · 𝑅))
281275, 280eqbrtrd 4707 . . . . . . . . 9 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐼 + 1) / 𝑛𝐴 · 𝑅))
282226, 227, 230, 231, 267, 281le2addd 10684 . . . . . . . 8 (𝜑 → ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ (((𝐽 + 1) / 𝑛𝐴 · 𝑅) + ((𝐼 + 1) / 𝑛𝐴 · 𝑅)))
28395recnd 10106 . . . . . . . . 9 (𝜑𝑅 ∈ ℂ)
284118, 128, 283adddird 10103 . . . . . . . 8 (𝜑 → (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) = (((𝐽 + 1) / 𝑛𝐴 · 𝑅) + ((𝐼 + 1) / 𝑛𝐴 · 𝑅)))
285282, 284breqtrrd 4713 . . . . . . 7 (𝜑 → ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅))
286136, 228, 218, 229, 285letrd 10232 . . . . . 6 (𝜑 → (abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅))
287156abscld 14219 . . . . . . . 8 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
28883, 287fsumrecl 14509 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
28983, 156fsumabs 14577 . . . . . . 7 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
29095adantr 480 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑅 ∈ ℝ)
291222, 290remulcld 10108 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) ∈ ℝ)
292137, 148syldan 486 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) ∈ ℂ)
293153adantr 480 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
294292, 293absmuld 14237 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) = ((abs‘((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
295 elfzouz 12513 . . . . . . . . . . . . . . 15 (𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1)) → 𝑖 ∈ (ℤ‘(𝐼 + 1)))
296 uztrn 11742 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (ℤ‘(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (ℤ𝑀)) → 𝑖 ∈ (ℤ𝑀))
297295, 252, 296syl2anr 494 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ (ℤ𝑀))
298 eluznn 11796 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℕ ∧ 𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℕ)
29932, 298sylan 487 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℕ)
300299, 139syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑖 + 1) ∈ ℝ+)
301299nnrpd 11908 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℝ+)
302343expia 1286 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+)) → ((𝑀𝑛𝑛𝑥) → 𝐵𝐴))
303302ralrimivva 3000 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴))
304303adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → ∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴))
305 nfcv 2793 . . . . . . . . . . . . . . . . . 18 𝑛+
306 nfv 1883 . . . . . . . . . . . . . . . . . . 19 𝑛(𝑀𝑖𝑖𝑥)
307 nfcv 2793 . . . . . . . . . . . . . . . . . . . 20 𝑛𝐵
308 nfcv 2793 . . . . . . . . . . . . . . . . . . . 20 𝑛
309307, 308, 60nfbr 4732 . . . . . . . . . . . . . . . . . . 19 𝑛 𝐵𝑖 / 𝑛𝐴
310306, 309nfim 1865 . . . . . . . . . . . . . . . . . 18 𝑛((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)
311305, 310nfral 2974 . . . . . . . . . . . . . . . . 17 𝑛𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)
312 breq2 4689 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑖 → (𝑀𝑛𝑀𝑖))
313 breq1 4688 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑖 → (𝑛𝑥𝑖𝑥))
314312, 313anbi12d 747 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑖 → ((𝑀𝑛𝑛𝑥) ↔ (𝑀𝑖𝑖𝑥)))
31564breq2d 4697 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑖 → (𝐵𝐴𝐵𝑖 / 𝑛𝐴))
316314, 315imbi12d 333 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑖 → (((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)))
317316ralbidv 3015 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 → (∀𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)))
318311, 317rspc 3334 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℝ+ → (∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) → ∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)))
319301, 304, 318sylc 65 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → ∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴))
320234lep1d 10993 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ≤ (𝑖 + 1))
321236, 320jca 553 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑀𝑖𝑖 ≤ (𝑖 + 1)))
322 breq2 4689 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑖 + 1) → (𝑖𝑥𝑖 ≤ (𝑖 + 1)))
323322anbi2d 740 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑖 + 1) → ((𝑀𝑖𝑖𝑥) ↔ (𝑀𝑖𝑖 ≤ (𝑖 + 1))))
324 eqvisset 3242 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑖 + 1) → (𝑖 + 1) ∈ V)
325 eqtr3 2672 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) → 𝑥 = 𝑛)
32631equcoms 1993 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑛𝐴 = 𝐵)
327325, 326syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) → 𝐴 = 𝐵)
328324, 327csbied 3593 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑖 + 1) → (𝑖 + 1) / 𝑛𝐴 = 𝐵)
329328eqcomd 2657 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑖 + 1) → 𝐵 = (𝑖 + 1) / 𝑛𝐴)
330329breq1d 4695 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑖 + 1) → (𝐵𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴))
331323, 330imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑖 + 1) → (((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴) ↔ ((𝑀𝑖𝑖 ≤ (𝑖 + 1)) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)))
332331rspcv 3336 . . . . . . . . . . . . . . 15 ((𝑖 + 1) ∈ ℝ+ → (∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴) → ((𝑀𝑖𝑖 ≤ (𝑖 + 1)) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)))
333300, 319, 321, 332syl3c 66 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)
334297, 333syldan 486 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)
335221, 220, 334abssuble0d 14215 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)) = (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴))
336335oveq1d 6705 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((abs‘((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) = ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
337294, 336eqtrd 2685 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) = ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
338293abscld 14219 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℝ)
339220, 221subge0d 10655 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (0 ≤ (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ↔ (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴))
340334, 339mpbird 247 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 0 ≤ (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴))
341137peano2nnd 11075 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) ∈ ℕ)
342341nnnn0d 11389 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) ∈ ℕ0)
34319, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263dchrisumlem1 25223 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 + 1) ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
344342, 343syldan 486 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
345338, 290, 222, 340, 344lemul2ad 11002 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
346337, 345eqbrtrd 4707 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
34783, 287, 291, 346fsumle 14575 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
348222recnd 10106 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ∈ ℂ)
34983, 283, 348fsummulc1 14561 . . . . . . . . 9 (𝜑 → (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
350219oveq1d 6705 . . . . . . . . 9 (𝜑 → (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) = (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
351349, 350eqtr3d 2687 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) = (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
352347, 351breqtrd 4711 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
353158, 288, 225, 289, 352letrd 10232 . . . . . 6 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
354136, 158, 218, 225, 286, 353le2addd 10684 . . . . 5 (𝜑 → ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))) ≤ ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) + (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅)))
3551282timesd 11313 . . . . . . . 8 (𝜑 → (2 · (𝐼 + 1) / 𝑛𝐴) = ((𝐼 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴))
356128, 118, 128ppncand 10470 . . . . . . . 8 (𝜑 → (((𝐼 + 1) / 𝑛𝐴 + (𝐽 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) = ((𝐼 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴))
357128, 118addcomd 10276 . . . . . . . . 9 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 + (𝐽 + 1) / 𝑛𝐴) = ((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴))
358357oveq1d 6705 . . . . . . . 8 (𝜑 → (((𝐼 + 1) / 𝑛𝐴 + (𝐽 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) = (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)))
359355, 356, 3583eqtr2d 2691 . . . . . . 7 (𝜑 → (2 · (𝐼 + 1) / 𝑛𝐴) = (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)))
360359oveq1d 6705 . . . . . 6 (𝜑 → ((2 · (𝐼 + 1) / 𝑛𝐴) · 𝑅) = ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) · 𝑅))
361 2cnd 11131 . . . . . . 7 (𝜑 → 2 ∈ ℂ)
362361, 128, 283mul32d 10284 . . . . . 6 (𝜑 → ((2 · (𝐼 + 1) / 𝑛𝐴) · 𝑅) = ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴))
363217recnd 10106 . . . . . . 7 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) ∈ ℂ)
364224recnd 10106 . . . . . . 7 (𝜑 → ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) ∈ ℂ)
365363, 364, 283adddird 10103 . . . . . 6 (𝜑 → ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) · 𝑅) = ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) + (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅)))
366360, 362, 3653eqtr3d 2693 . . . . 5 (𝜑 → ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴) = ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) + (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅)))
367354, 366breqtrrd 4713 . . . 4 (𝜑 → ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))) ≤ ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴))
36892, 159, 102, 216, 367letrd 10232 . . 3 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ≤ ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴))
369 2nn0 11347 . . . . . 6 2 ∈ ℕ0
370 nn0ge0 11356 . . . . . 6 (2 ∈ ℕ0 → 0 ≤ 2)
371369, 370mp1i 13 . . . . 5 (𝜑 → 0 ≤ 2)
372 0red 10079 . . . . . 6 (𝜑 → 0 ∈ ℝ)
373126absge0d 14227 . . . . . 6 (𝜑 → 0 ≤ (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))))
374372, 261, 95, 373, 265letrd 10232 . . . . 5 (𝜑 → 0 ≤ 𝑅)
37594, 95, 371, 374mulge0d 10642 . . . 4 (𝜑 → 0 ≤ (2 · 𝑅))
3764nnrpd 11908 . . . . 5 (𝜑 → (𝐼 + 1) ∈ ℝ+)
377 nfv 1883 . . . . . . . . 9 𝑛(𝑀𝑈𝑈𝑥)
378307, 308, 105nfbr 4732 . . . . . . . . 9 𝑛 𝐵𝑈 / 𝑛𝐴
379377, 378nfim 1865 . . . . . . . 8 𝑛((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)
380305, 379nfral 2974 . . . . . . 7 𝑛𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)
381 breq2 4689 . . . . . . . . . 10 (𝑛 = 𝑈 → (𝑀𝑛𝑀𝑈))
382 breq1 4688 . . . . . . . . . 10 (𝑛 = 𝑈 → (𝑛𝑥𝑈𝑥))
383381, 382anbi12d 747 . . . . . . . . 9 (𝑛 = 𝑈 → ((𝑀𝑛𝑛𝑥) ↔ (𝑀𝑈𝑈𝑥)))
384107breq2d 4697 . . . . . . . . 9 (𝑛 = 𝑈 → (𝐵𝐴𝐵𝑈 / 𝑛𝐴))
385383, 384imbi12d 333 . . . . . . . 8 (𝑛 = 𝑈 → (((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)))
386385ralbidv 3015 . . . . . . 7 (𝑛 = 𝑈 → (∀𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)))
387380, 386rspc 3334 . . . . . 6 (𝑈 ∈ ℝ+ → (∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) → ∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)))
388103, 303, 387sylc 65 . . . . 5 (𝜑 → ∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴))
389248, 249jca 553 . . . . 5 (𝜑 → (𝑀𝑈𝑈 ≤ (𝐼 + 1)))
390 breq2 4689 . . . . . . . 8 (𝑥 = (𝐼 + 1) → (𝑈𝑥𝑈 ≤ (𝐼 + 1)))
391390anbi2d 740 . . . . . . 7 (𝑥 = (𝐼 + 1) → ((𝑀𝑈𝑈𝑥) ↔ (𝑀𝑈𝑈 ≤ (𝐼 + 1))))
392 eqvisset 3242 . . . . . . . . . 10 (𝑥 = (𝐼 + 1) → (𝐼 + 1) ∈ V)
393 eqtr3 2672 . . . . . . . . . . 11 ((𝑥 = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) → 𝑥 = 𝑛)
394393, 326syl 17 . . . . . . . . . 10 ((𝑥 = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) → 𝐴 = 𝐵)
395392, 394csbied 3593 . . . . . . . . 9 (𝑥 = (𝐼 + 1) → (𝐼 + 1) / 𝑛𝐴 = 𝐵)
396395eqcomd 2657 . . . . . . . 8 (𝑥 = (𝐼 + 1) → 𝐵 = (𝐼 + 1) / 𝑛𝐴)
397396breq1d 4695 . . . . . . 7 (𝑥 = (𝐼 + 1) → (𝐵𝑈 / 𝑛𝐴(𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴))
398391, 397imbi12d 333 . . . . . 6 (𝑥 = (𝐼 + 1) → (((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴) ↔ ((𝑀𝑈𝑈 ≤ (𝐼 + 1)) → (𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴)))
399398rspcv 3336 . . . . 5 ((𝐼 + 1) ∈ ℝ+ → (∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴) → ((𝑀𝑈𝑈 ≤ (𝐼 + 1)) → (𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴)))
400376, 388, 389, 399syl3c 66 . . . 4 (𝜑(𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴)
401101, 110, 96, 375, 400lemul2ad 11002 . . 3 (𝜑 → ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴) ≤ ((2 · 𝑅) · 𝑈 / 𝑛𝐴))
40292, 102, 111, 368, 401letrd 10232 . 2 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ≤ ((2 · 𝑅) · 𝑈 / 𝑛𝐴))
40391, 402eqbrtrd 4707 1 (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) ≤ ((2 · 𝑅) · 𝑈 / 𝑛𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  Vcvv 3231  csb 3566  cun 3605  cin 3606  c0 3948   class class class wbr 4685  cmpt 4762  cfv 5926  (class class class)co 6690  Fincfn 7997  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  +∞cpnf 10109  cle 10113  cmin 10304  cn 11058  2c2 11108  0cn0 11330  cz 11415  cuz 11725  +crp 11870  [,)cico 12215  ...cfz 12364  ..^cfzo 12504  seqcseq 12841  abscabs 14018  𝑟 crli 14260  Σcsu 14460  Basecbs 15904  0gc0g 16147  ℤRHomczrh 19896  ℤ/nczn 19899  DChrcdchr 25002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-tpos 7397  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-ec 7789  df-qs 7793  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-xnn0 11402  df-z 11416  df-dec 11532  df-uz 11726  df-rp 11871  df-ico 12219  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-rlim 14264  df-sum 14461  df-dvds 15028  df-gcd 15264  df-phi 15518  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-0g 16149  df-imas 16215  df-qus 16216  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-mhm 17382  df-grp 17472  df-minusg 17473  df-sbg 17474  df-mulg 17588  df-subg 17638  df-nsg 17639  df-eqg 17640  df-ghm 17705  df-cmn 18241  df-abl 18242  df-mgp 18536  df-ur 18548  df-ring 18595  df-cring 18596  df-oppr 18669  df-dvdsr 18687  df-unit 18688  df-invr 18718  df-rnghom 18763  df-subrg 18826  df-lmod 18913  df-lss 18981  df-lsp 19020  df-sra 19220  df-rgmod 19221  df-lidl 19222  df-rsp 19223  df-2idl 19280  df-cnfld 19795  df-zring 19867  df-zrh 19900  df-zn 19903  df-dchr 25003
This theorem is referenced by:  dchrisumlem3  25225
  Copyright terms: Public domain W3C validator