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

Theorem dchrisumlem2 27552
Description: Lemma for dchrisum 27554. 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 13750 . . . . . . . . 9 ((1..^(𝐼 + 1)) ∩ ((𝐼 + 1)..^(𝐽 + 1))) = ∅
21a1i 11 . . . . . . . 8 (𝜑 → ((1..^(𝐼 + 1)) ∩ ((𝐼 + 1)..^(𝐽 + 1))) = ∅)
3 dchrisumlem2.4 . . . . . . . . . . . 12 (𝜑𝐼 ∈ ℕ)
43peano2nnd 12310 . . . . . . . . . . 11 (𝜑 → (𝐼 + 1) ∈ ℕ)
5 nnuz 12946 . . . . . . . . . . 11 ℕ = (ℤ‘1)
64, 5eleqtrdi 2854 . . . . . . . . . 10 (𝜑 → (𝐼 + 1) ∈ (ℤ‘1))
7 dchrisumlem2.5 . . . . . . . . . . 11 (𝜑𝐽 ∈ (ℤ𝐼))
8 eluzp1p1 12931 . . . . . . . . . . 11 (𝐽 ∈ (ℤ𝐼) → (𝐽 + 1) ∈ (ℤ‘(𝐼 + 1)))
97, 8syl 17 . . . . . . . . . 10 (𝜑 → (𝐽 + 1) ∈ (ℤ‘(𝐼 + 1)))
10 elfzuzb 13578 . . . . . . . . . 10 ((𝐼 + 1) ∈ (1...(𝐽 + 1)) ↔ ((𝐼 + 1) ∈ (ℤ‘1) ∧ (𝐽 + 1) ∈ (ℤ‘(𝐼 + 1))))
116, 9, 10sylanbrc 582 . . . . . . . . 9 (𝜑 → (𝐼 + 1) ∈ (1...(𝐽 + 1)))
12 fzosplit 13749 . . . . . . . . 9 ((𝐼 + 1) ∈ (1...(𝐽 + 1)) → (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1))))
1311, 12syl 17 . . . . . . . 8 (𝜑 → (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1))))
14 fzofi 14025 . . . . . . . . 9 (1..^(𝐽 + 1)) ∈ Fin
1514a1i 11 . . . . . . . 8 (𝜑 → (1..^(𝐽 + 1)) ∈ Fin)
16 elfzouz 13720 . . . . . . . . . 10 (𝑖 ∈ (1..^(𝐽 + 1)) → 𝑖 ∈ (ℤ‘1))
1716, 5eleqtrrdi 2855 . . . . . . . . 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 12660 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → 𝑖 ∈ ℤ)
2524adantl 481 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℤ)
2618, 19, 20, 21, 23, 25dchrzrhcl 27307 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → (𝑋‘(𝐿𝑖)) ∈ ℂ)
27 rpvmasum.a . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ)
28 rpvmasum.1 . . . . . . . . . . . . . 14 1 = (0g𝐺)
29 dchrisum.n1 . . . . . . . . . . . . . 14 (𝜑𝑋1 )
30 dchrisum.2 . . . . . . . . . . . . . 14 (𝑛 = 𝑥𝐴 = 𝐵)
31 dchrisum.3 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℕ)
32 dchrisum.4 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)
33 dchrisum.5 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+) ∧ (𝑀𝑛𝑛𝑥)) → 𝐵𝐴)
34 dchrisum.6 . . . . . . . . . . . . . 14 (𝜑 → (𝑛 ∈ ℝ+𝐴) ⇝𝑟 0)
35 dchrisum.7 . . . . . . . . . . . . . 14 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿𝑛)) · 𝐴))
3619, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35dchrisumlema 27550 . . . . . . . . . . . . 13 (𝜑 → ((𝑖 ∈ ℝ+𝑖 / 𝑛𝐴 ∈ ℝ) ∧ (𝑖 ∈ (𝑀[,)+∞) → 0 ≤ 𝑖 / 𝑛𝐴)))
3736simpld 494 . . . . . . . . . . . 12 (𝜑 → (𝑖 ∈ ℝ+𝑖 / 𝑛𝐴 ∈ ℝ))
38 nnrp 13068 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → 𝑖 ∈ ℝ+)
3937, 38impel 505 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 𝑖 / 𝑛𝐴 ∈ ℝ)
4039recnd 11318 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → 𝑖 / 𝑛𝐴 ∈ ℂ)
4126, 40mulcld 11310 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
4217, 41sylan2 592 . . . . . . . 8 ((𝜑𝑖 ∈ (1..^(𝐽 + 1))) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
432, 13, 15, 42fsumsplit 15789 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (1..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
44 eluzelz 12913 . . . . . . . . 9 (𝐽 ∈ (ℤ𝐼) → 𝐽 ∈ ℤ)
45 fzval3 13785 . . . . . . . . 9 (𝐽 ∈ ℤ → (1...𝐽) = (1..^(𝐽 + 1)))
467, 44, 453syl 18 . . . . . . . 8 (𝜑 → (1...𝐽) = (1..^(𝐽 + 1)))
4746sumeq1d 15748 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = Σ𝑖 ∈ (1..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
483nnzd 12666 . . . . . . . . . 10 (𝜑𝐼 ∈ ℤ)
49 fzval3 13785 . . . . . . . . . 10 (𝐼 ∈ ℤ → (1...𝐼) = (1..^(𝐼 + 1)))
5048, 49syl 17 . . . . . . . . 9 (𝜑 → (1...𝐼) = (1..^(𝐼 + 1)))
5150sumeq1d 15748 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
5251oveq1d 7463 . . . . . . 7 (𝜑 → (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
5343, 47, 523eqtr4d 2790 . . . . . 6 (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
54 elfznn 13613 . . . . . . . 8 (𝑖 ∈ (1...𝐽) → 𝑖 ∈ ℕ)
55 simpr 484 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
56 nfcv 2908 . . . . . . . . . 10 𝑛𝑖
57 nfcv 2908 . . . . . . . . . . 11 𝑛(𝑋‘(𝐿𝑖))
58 nfcv 2908 . . . . . . . . . . 11 𝑛 ·
59 nfcsb1v 3946 . . . . . . . . . . 11 𝑛𝑖 / 𝑛𝐴
6057, 58, 59nfov 7478 . . . . . . . . . 10 𝑛((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)
61 2fveq3 6925 . . . . . . . . . . 11 (𝑛 = 𝑖 → (𝑋‘(𝐿𝑛)) = (𝑋‘(𝐿𝑖)))
62 csbeq1a 3935 . . . . . . . . . . 11 (𝑛 = 𝑖𝐴 = 𝑖 / 𝑛𝐴)
6361, 62oveq12d 7466 . . . . . . . . . 10 (𝑛 = 𝑖 → ((𝑋‘(𝐿𝑛)) · 𝐴) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
6456, 60, 63, 35fvmptf 7050 . . . . . . . . 9 ((𝑖 ∈ ℕ ∧ ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
6555, 41, 64syl2anc 583 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
6654, 65sylan2 592 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝐽)) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
673, 5eleqtrdi 2854 . . . . . . . 8 (𝜑𝐼 ∈ (ℤ‘1))
68 uztrn 12921 . . . . . . . 8 ((𝐽 ∈ (ℤ𝐼) ∧ 𝐼 ∈ (ℤ‘1)) → 𝐽 ∈ (ℤ‘1))
697, 67, 68syl2anc 583 . . . . . . 7 (𝜑𝐽 ∈ (ℤ‘1))
7054, 41sylan2 592 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝐽)) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
7166, 69, 70fsumser 15778 . . . . . 6 (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (seq1( + , 𝐹)‘𝐽))
7253, 71eqtr3d 2782 . . . . 5 (𝜑 → (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = (seq1( + , 𝐹)‘𝐽))
73 elfznn 13613 . . . . . . 7 (𝑖 ∈ (1...𝐼) → 𝑖 ∈ ℕ)
7473, 65sylan2 592 . . . . . 6 ((𝜑𝑖 ∈ (1...𝐼)) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
7573, 41sylan2 592 . . . . . 6 ((𝜑𝑖 ∈ (1...𝐼)) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
7674, 67, 75fsumser 15778 . . . . 5 (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (seq1( + , 𝐹)‘𝐼))
7772, 76oveq12d 7466 . . . 4 (𝜑 → ((Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) − Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = ((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼)))
78 fzfid 14024 . . . . . 6 (𝜑 → (1...𝐼) ∈ Fin)
7978, 75fsumcl 15781 . . . . 5 (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
80 fzofi 14025 . . . . . . 7 ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin
8180a1i 11 . . . . . 6 (𝜑 → ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin)
82 ssun2 4202 . . . . . . . . 9 ((𝐼 + 1)..^(𝐽 + 1)) ⊆ ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1)))
8382, 13sseqtrrid 4062 . . . . . . . 8 (𝜑 → ((𝐼 + 1)..^(𝐽 + 1)) ⊆ (1..^(𝐽 + 1)))
8483sselda 4008 . . . . . . 7 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ (1..^(𝐽 + 1)))
8584, 42syldan 590 . . . . . 6 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
8681, 85fsumcl 15781 . . . . 5 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
8779, 86pncan2d 11649 . . . 4 (𝜑 → ((Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) − Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
8877, 87eqtr3d 2782 . . 3 (𝜑 → ((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
8988fveq2d 6924 . 2 (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) = (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
9086abscld 15485 . . 3 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ∈ ℝ)
91 2re 12367 . . . . . 6 2 ∈ ℝ
9291a1i 11 . . . . 5 (𝜑 → 2 ∈ ℝ)
93 dchrisum.9 . . . . 5 (𝜑𝑅 ∈ ℝ)
9492, 93remulcld 11320 . . . 4 (𝜑 → (2 · 𝑅) ∈ ℝ)
9539ralrimiva 3152 . . . . 5 (𝜑 → ∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℝ)
96 csbeq1 3924 . . . . . . 7 (𝑖 = (𝐼 + 1) → 𝑖 / 𝑛𝐴 = (𝐼 + 1) / 𝑛𝐴)
9796eleq1d 2829 . . . . . 6 (𝑖 = (𝐼 + 1) → (𝑖 / 𝑛𝐴 ∈ ℝ ↔ (𝐼 + 1) / 𝑛𝐴 ∈ ℝ))
9897rspcv 3631 . . . . 5 ((𝐼 + 1) ∈ ℕ → (∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℝ → (𝐼 + 1) / 𝑛𝐴 ∈ ℝ))
994, 95, 98sylc 65 . . . 4 (𝜑(𝐼 + 1) / 𝑛𝐴 ∈ ℝ)
10094, 99remulcld 11320 . . 3 (𝜑 → ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴) ∈ ℝ)
101 dchrisumlem2.1 . . . . 5 (𝜑𝑈 ∈ ℝ+)
10232ralrimiva 3152 . . . . 5 (𝜑 → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ)
103 nfcsb1v 3946 . . . . . . 7 𝑛𝑈 / 𝑛𝐴
104103nfel1 2925 . . . . . 6 𝑛𝑈 / 𝑛𝐴 ∈ ℝ
105 csbeq1a 3935 . . . . . . 7 (𝑛 = 𝑈𝐴 = 𝑈 / 𝑛𝐴)
106105eleq1d 2829 . . . . . 6 (𝑛 = 𝑈 → (𝐴 ∈ ℝ ↔ 𝑈 / 𝑛𝐴 ∈ ℝ))
107104, 106rspc 3623 . . . . 5 (𝑈 ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → 𝑈 / 𝑛𝐴 ∈ ℝ))
108101, 102, 107sylc 65 . . . 4 (𝜑𝑈 / 𝑛𝐴 ∈ ℝ)
10994, 108remulcld 11320 . . 3 (𝜑 → ((2 · 𝑅) · 𝑈 / 𝑛𝐴) ∈ ℝ)
11069, 5eleqtrrdi 2855 . . . . . . . . . . . 12 (𝜑𝐽 ∈ ℕ)
111110peano2nnd 12310 . . . . . . . . . . 11 (𝜑 → (𝐽 + 1) ∈ ℕ)
112111nnrpd 13097 . . . . . . . . . 10 (𝜑 → (𝐽 + 1) ∈ ℝ+)
11319, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35dchrisumlema 27550 . . . . . . . . . . 11 (𝜑 → (((𝐽 + 1) ∈ ℝ+(𝐽 + 1) / 𝑛𝐴 ∈ ℝ) ∧ ((𝐽 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐽 + 1) / 𝑛𝐴)))
114113simpld 494 . . . . . . . . . 10 (𝜑 → ((𝐽 + 1) ∈ ℝ+(𝐽 + 1) / 𝑛𝐴 ∈ ℝ))
115112, 114mpd 15 . . . . . . . . 9 (𝜑(𝐽 + 1) / 𝑛𝐴 ∈ ℝ)
116115recnd 11318 . . . . . . . 8 (𝜑(𝐽 + 1) / 𝑛𝐴 ∈ ℂ)
117 fzofi 14025 . . . . . . . . . 10 (0..^(𝐽 + 1)) ∈ Fin
118117a1i 11 . . . . . . . . 9 (𝜑 → (0..^(𝐽 + 1)) ∈ Fin)
119 elfzoelz 13716 . . . . . . . . . 10 (𝑛 ∈ (0..^(𝐽 + 1)) → 𝑛 ∈ ℤ)
12022adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℤ) → 𝑋𝐷)
121 simpr 484 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℤ) → 𝑛 ∈ ℤ)
12218, 19, 20, 21, 120, 121dchrzrhcl 27307 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℤ) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
123119, 122sylan2 592 . . . . . . . . 9 ((𝜑𝑛 ∈ (0..^(𝐽 + 1))) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
124118, 123fsumcl 15781 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
125116, 124mulcld 11310 . . . . . . 7 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
12699recnd 11318 . . . . . . . 8 (𝜑(𝐼 + 1) / 𝑛𝐴 ∈ ℂ)
127 fzofi 14025 . . . . . . . . . 10 (0..^(𝐼 + 1)) ∈ Fin
128127a1i 11 . . . . . . . . 9 (𝜑 → (0..^(𝐼 + 1)) ∈ Fin)
129 elfzoelz 13716 . . . . . . . . . 10 (𝑛 ∈ (0..^(𝐼 + 1)) → 𝑛 ∈ ℤ)
130129, 122sylan2 592 . . . . . . . . 9 ((𝜑𝑛 ∈ (0..^(𝐼 + 1))) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
131128, 130fsumcl 15781 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
132126, 131mulcld 11310 . . . . . . 7 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
133125, 132subcld 11647 . . . . . 6 (𝜑 → (((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℂ)
134133abscld 15485 . . . . 5 (𝜑 → (abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ∈ ℝ)
13584, 17syl 17 . . . . . . . 8 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ ℕ)
136 peano2nn 12305 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℕ)
137136nnrpd 13097 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℝ+)
138 nfcsb1v 3946 . . . . . . . . . . . . . . 15 𝑛(𝑖 + 1) / 𝑛𝐴
139138nfel1 2925 . . . . . . . . . . . . . 14 𝑛(𝑖 + 1) / 𝑛𝐴 ∈ ℝ
140 csbeq1a 3935 . . . . . . . . . . . . . . 15 (𝑛 = (𝑖 + 1) → 𝐴 = (𝑖 + 1) / 𝑛𝐴)
141140eleq1d 2829 . . . . . . . . . . . . . 14 (𝑛 = (𝑖 + 1) → (𝐴 ∈ ℝ ↔ (𝑖 + 1) / 𝑛𝐴 ∈ ℝ))
142139, 141rspc 3623 . . . . . . . . . . . . 13 ((𝑖 + 1) ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ))
143142impcom 407 . . . . . . . . . . . 12 ((∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ ∧ (𝑖 + 1) ∈ ℝ+) → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ)
144102, 137, 143syl2an 595 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ)
145144, 39resubcld 11718 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → ((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) ∈ ℝ)
146145recnd 11318 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) ∈ ℂ)
147 fzofi 14025 . . . . . . . . . . . 12 (0..^(𝑖 + 1)) ∈ Fin
148147a1i 11 . . . . . . . . . . 11 (𝜑 → (0..^(𝑖 + 1)) ∈ Fin)
149 elfzoelz 13716 . . . . . . . . . . . 12 (𝑛 ∈ (0..^(𝑖 + 1)) → 𝑛 ∈ ℤ)
150149, 122sylan2 592 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (0..^(𝑖 + 1))) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
151148, 150fsumcl 15781 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
152151adantr 480 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
153146, 152mulcld 11310 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ) → (((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
154135, 153syldan 590 . . . . . . 7 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
15581, 154fsumcl 15781 . . . . . 6 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
156155abscld 15485 . . . . 5 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
157134, 156readdcld 11319 . . . 4 (𝜑 → ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))) ∈ ℝ)
15826, 40mulcomd 11311 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (𝑖 / 𝑛𝐴 · (𝑋‘(𝐿𝑖))))
159 nnnn0 12560 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → 𝑖 ∈ ℕ0)
160159adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ0)
161 nn0uz 12945 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
162160, 161eleqtrdi 2854 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ (ℤ‘0))
163 elfzelz 13584 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0...𝑖) → 𝑛 ∈ ℤ)
164122adantlr 714 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
165163, 164sylan2 592 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ ℕ) ∧ 𝑛 ∈ (0...𝑖)) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
166162, 165, 61fzosump1 15800 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) = (Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) + (𝑋‘(𝐿𝑖))))
167166oveq1d 7463 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))) = ((Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) + (𝑋‘(𝐿𝑖))) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))))
168 fzofi 14025 . . . . . . . . . . . . . . 15 (0..^𝑖) ∈ Fin
169168a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → (0..^𝑖) ∈ Fin)
170 elfzoelz 13716 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0..^𝑖) → 𝑛 ∈ ℤ)
171170, 164sylan2 592 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ ℕ) ∧ 𝑛 ∈ (0..^𝑖)) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
172169, 171fsumcl 15781 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) ∈ ℂ)
173172, 26pncan2d 11649 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) + (𝑋‘(𝐿𝑖))) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))) = (𝑋‘(𝐿𝑖)))
174167, 173eqtr2d 2781 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (𝑋‘(𝐿𝑖)) = (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))))
175174oveq2d 7464 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → (𝑖 / 𝑛𝐴 · (𝑋‘(𝐿𝑖))) = (𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
176158, 175eqtrd 2780 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
177135, 176syldan 590 . . . . . . . 8 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
178177sumeq2dv 15750 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
179 csbeq1 3924 . . . . . . . . 9 (𝑘 = 𝑖𝑘 / 𝑛𝐴 = 𝑖 / 𝑛𝐴)
180 oveq2 7456 . . . . . . . . . 10 (𝑘 = 𝑖 → (0..^𝑘) = (0..^𝑖))
181180sumeq1d 15748 . . . . . . . . 9 (𝑘 = 𝑖 → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))
182179, 181jca 511 . . . . . . . 8 (𝑘 = 𝑖 → (𝑘 / 𝑛𝐴 = 𝑖 / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))))
183 csbeq1 3924 . . . . . . . . 9 (𝑘 = (𝑖 + 1) → 𝑘 / 𝑛𝐴 = (𝑖 + 1) / 𝑛𝐴)
184 oveq2 7456 . . . . . . . . . 10 (𝑘 = (𝑖 + 1) → (0..^𝑘) = (0..^(𝑖 + 1)))
185184sumeq1d 15748 . . . . . . . . 9 (𝑘 = (𝑖 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))
186183, 185jca 511 . . . . . . . 8 (𝑘 = (𝑖 + 1) → (𝑘 / 𝑛𝐴 = (𝑖 + 1) / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))
187 csbeq1 3924 . . . . . . . . 9 (𝑘 = (𝐼 + 1) → 𝑘 / 𝑛𝐴 = (𝐼 + 1) / 𝑛𝐴)
188 oveq2 7456 . . . . . . . . . 10 (𝑘 = (𝐼 + 1) → (0..^𝑘) = (0..^(𝐼 + 1)))
189188sumeq1d 15748 . . . . . . . . 9 (𝑘 = (𝐼 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))
190187, 189jca 511 . . . . . . . 8 (𝑘 = (𝐼 + 1) → (𝑘 / 𝑛𝐴 = (𝐼 + 1) / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))
191 csbeq1 3924 . . . . . . . . 9 (𝑘 = (𝐽 + 1) → 𝑘 / 𝑛𝐴 = (𝐽 + 1) / 𝑛𝐴)
192 oveq2 7456 . . . . . . . . . 10 (𝑘 = (𝐽 + 1) → (0..^𝑘) = (0..^(𝐽 + 1)))
193192sumeq1d 15748 . . . . . . . . 9 (𝑘 = (𝐽 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))
194191, 193jca 511 . . . . . . . 8 (𝑘 = (𝐽 + 1) → (𝑘 / 𝑛𝐴 = (𝐽 + 1) / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))))
19540ralrimiva 3152 . . . . . . . . 9 (𝜑 → ∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℂ)
196 elfzuz 13580 . . . . . . . . . 10 (𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1)) → 𝑘 ∈ (ℤ‘(𝐼 + 1)))
197 eluznn 12983 . . . . . . . . . 10 (((𝐼 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(𝐼 + 1))) → 𝑘 ∈ ℕ)
1984, 196, 197syl2an 595 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → 𝑘 ∈ ℕ)
199 csbeq1 3924 . . . . . . . . . . 11 (𝑖 = 𝑘𝑖 / 𝑛𝐴 = 𝑘 / 𝑛𝐴)
200199eleq1d 2829 . . . . . . . . . 10 (𝑖 = 𝑘 → (𝑖 / 𝑛𝐴 ∈ ℂ ↔ 𝑘 / 𝑛𝐴 ∈ ℂ))
201200rspccva 3634 . . . . . . . . 9 ((∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) → 𝑘 / 𝑛𝐴 ∈ ℂ)
202195, 198, 201syl2an2r 684 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → 𝑘 / 𝑛𝐴 ∈ ℂ)
203 fzofi 14025 . . . . . . . . . . 11 (0..^𝑘) ∈ Fin
204203a1i 11 . . . . . . . . . 10 (𝜑 → (0..^𝑘) ∈ Fin)
205 elfzoelz 13716 . . . . . . . . . . 11 (𝑛 ∈ (0..^𝑘) → 𝑛 ∈ ℤ)
206205, 122sylan2 592 . . . . . . . . . 10 ((𝜑𝑛 ∈ (0..^𝑘)) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
207204, 206fsumcl 15781 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) ∈ ℂ)
208207adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) ∈ ℂ)
209182, 186, 190, 194, 9, 202, 208fsumparts 15854 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))) = ((((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
210178, 209eqtrd 2780 . . . . . 6 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = ((((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
211210fveq2d 6924 . . . . 5 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = (abs‘((((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))))
212133, 155abs2dif2d 15507 . . . . 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))(𝑋‘(𝐿𝑛))))))
213211, 212eqbrtrd 5188 . . . 4 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ≤ ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))))
214115, 99readdcld 11319 . . . . . . 7 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) ∈ ℝ)
215214, 93remulcld 11320 . . . . . 6 (𝜑 → (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) ∈ ℝ)
216179, 183, 187, 191, 9, 202telfsumo 15850 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) = ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴))
217135, 39syldan 590 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 / 𝑛𝐴 ∈ ℝ)
218135, 144syldan 590 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ)
219217, 218resubcld 11718 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ∈ ℝ)
22081, 219fsumrecl 15782 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ∈ ℝ)
221216, 220eqeltrrd 2845 . . . . . . 7 (𝜑 → ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) ∈ ℝ)
222221, 93remulcld 11320 . . . . . 6 (𝜑 → (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅) ∈ ℝ)
223125abscld 15485 . . . . . . . 8 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
224132abscld 15485 . . . . . . . 8 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
225223, 224readdcld 11319 . . . . . . 7 (𝜑 → ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ∈ ℝ)
226125, 132abs2dif2d 15507 . . . . . . 7 (𝜑 → (abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))))
227115, 93remulcld 11320 . . . . . . . . 9 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 · 𝑅) ∈ ℝ)
22899, 93remulcld 11320 . . . . . . . . 9 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 · 𝑅) ∈ ℝ)
229116, 124absmuld 15503 . . . . . . . . . . 11 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) = ((abs‘(𝐽 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))))
230 eluzelre 12914 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (ℤ𝑀) → 𝑖 ∈ ℝ)
231230adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℝ)
232 eluzle 12916 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (ℤ𝑀) → 𝑀𝑖)
233232adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀𝑖)
23431nnred 12308 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℝ)
235234adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ)
236 elicopnf 13505 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℝ → (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀𝑖)))
237235, 236syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀𝑖)))
238231, 233, 237mpbir2and 712 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ (𝑀[,)+∞))
239238ex 412 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑖 ∈ (ℤ𝑀) → 𝑖 ∈ (𝑀[,)+∞)))
240239ssrdv 4014 . . . . . . . . . . . . . . 15 (𝜑 → (ℤ𝑀) ⊆ (𝑀[,)+∞))
24131nnzd 12666 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℤ)
24248peano2zd 12750 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐼 + 1) ∈ ℤ)
243101rpred 13099 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 ∈ ℝ)
2444nnred 12308 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐼 + 1) ∈ ℝ)
245 dchrisumlem2.2 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀𝑈)
246 dchrisumlem2.3 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 ≤ (𝐼 + 1))
247234, 243, 244, 245, 246letrd 11447 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ≤ (𝐼 + 1))
248 eluz2 12909 . . . . . . . . . . . . . . . . 17 ((𝐼 + 1) ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝐼 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝐼 + 1)))
249241, 242, 247, 248syl3anbrc 1343 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐼 + 1) ∈ (ℤ𝑀))
250 uztrn 12921 . . . . . . . . . . . . . . . 16 (((𝐽 + 1) ∈ (ℤ‘(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (ℤ𝑀)) → (𝐽 + 1) ∈ (ℤ𝑀))
2519, 249, 250syl2anc 583 . . . . . . . . . . . . . . 15 (𝜑 → (𝐽 + 1) ∈ (ℤ𝑀))
252240, 251sseldd 4009 . . . . . . . . . . . . . 14 (𝜑 → (𝐽 + 1) ∈ (𝑀[,)+∞))
253113simprd 495 . . . . . . . . . . . . . 14 (𝜑 → ((𝐽 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐽 + 1) / 𝑛𝐴))
254252, 253mpd 15 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ (𝐽 + 1) / 𝑛𝐴)
255115, 254absidd 15471 . . . . . . . . . . . 12 (𝜑 → (abs‘(𝐽 + 1) / 𝑛𝐴) = (𝐽 + 1) / 𝑛𝐴)
256255oveq1d 7463 . . . . . . . . . . 11 (𝜑 → ((abs‘(𝐽 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐽 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))))
257229, 256eqtrd 2780 . . . . . . . . . 10 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐽 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))))
258124abscld 15485 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ∈ ℝ)
259111nnnn0d 12613 . . . . . . . . . . . 12 (𝜑 → (𝐽 + 1) ∈ ℕ0)
260 dchrisum.10 . . . . . . . . . . . . 13 (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅)
26119, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35, 93, 260dchrisumlem1 27551 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐽 + 1) ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
262259, 261mpdan 686 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
263258, 93, 115, 254, 262lemul2ad 12235 . . . . . . . . . 10 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐽 + 1) / 𝑛𝐴 · 𝑅))
264257, 263eqbrtrd 5188 . . . . . . . . 9 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐽 + 1) / 𝑛𝐴 · 𝑅))
265126, 131absmuld 15503 . . . . . . . . . . 11 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) = ((abs‘(𝐼 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))))
266240, 249sseldd 4009 . . . . . . . . . . . . . 14 (𝜑 → (𝐼 + 1) ∈ (𝑀[,)+∞))
26719, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35dchrisumlema 27550 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐼 + 1) ∈ ℝ+(𝐼 + 1) / 𝑛𝐴 ∈ ℝ) ∧ ((𝐼 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐼 + 1) / 𝑛𝐴)))
268267simprd 495 . . . . . . . . . . . . . 14 (𝜑 → ((𝐼 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐼 + 1) / 𝑛𝐴))
269266, 268mpd 15 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ (𝐼 + 1) / 𝑛𝐴)
27099, 269absidd 15471 . . . . . . . . . . . 12 (𝜑 → (abs‘(𝐼 + 1) / 𝑛𝐴) = (𝐼 + 1) / 𝑛𝐴)
271270oveq1d 7463 . . . . . . . . . . 11 (𝜑 → ((abs‘(𝐼 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐼 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))))
272265, 271eqtrd 2780 . . . . . . . . . 10 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐼 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))))
273131abscld 15485 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ∈ ℝ)
2744nnnn0d 12613 . . . . . . . . . . . 12 (𝜑 → (𝐼 + 1) ∈ ℕ0)
27519, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35, 93, 260dchrisumlem1 27551 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐼 + 1) ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
276274, 275mpdan 686 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
277273, 93, 99, 269, 276lemul2ad 12235 . . . . . . . . . 10 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐼 + 1) / 𝑛𝐴 · 𝑅))
278272, 277eqbrtrd 5188 . . . . . . . . 9 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐼 + 1) / 𝑛𝐴 · 𝑅))
279223, 224, 227, 228, 264, 278le2addd 11909 . . . . . . . 8 (𝜑 → ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ (((𝐽 + 1) / 𝑛𝐴 · 𝑅) + ((𝐼 + 1) / 𝑛𝐴 · 𝑅)))
28093recnd 11318 . . . . . . . . 9 (𝜑𝑅 ∈ ℂ)
281116, 126, 280adddird 11315 . . . . . . . 8 (𝜑 → (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) = (((𝐽 + 1) / 𝑛𝐴 · 𝑅) + ((𝐼 + 1) / 𝑛𝐴 · 𝑅)))
282279, 281breqtrrd 5194 . . . . . . 7 (𝜑 → ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅))
283134, 225, 215, 226, 282letrd 11447 . . . . . 6 (𝜑 → (abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅))
284154abscld 15485 . . . . . . . 8 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
28581, 284fsumrecl 15782 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
28681, 154fsumabs 15849 . . . . . . 7 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
28793adantr 480 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑅 ∈ ℝ)
288219, 287remulcld 11320 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) ∈ ℝ)
289135, 146syldan 590 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) ∈ ℂ)
290151adantr 480 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
291289, 290absmuld 15503 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) = ((abs‘((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
292 elfzouz 13720 . . . . . . . . . . . . . . 15 (𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1)) → 𝑖 ∈ (ℤ‘(𝐼 + 1)))
293 uztrn 12921 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (ℤ‘(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (ℤ𝑀)) → 𝑖 ∈ (ℤ𝑀))
294292, 249, 293syl2anr 596 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ (ℤ𝑀))
295 eluznn 12983 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℕ ∧ 𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℕ)
29631, 295sylan 579 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℕ)
297296, 137syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑖 + 1) ∈ ℝ+)
298296nnrpd 13097 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℝ+)
299333expia 1121 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+)) → ((𝑀𝑛𝑛𝑥) → 𝐵𝐴))
300299ralrimivva 3208 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴))
301300adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → ∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴))
302 nfcv 2908 . . . . . . . . . . . . . . . . . 18 𝑛+
303 nfv 1913 . . . . . . . . . . . . . . . . . . 19 𝑛(𝑀𝑖𝑖𝑥)
304 nfcv 2908 . . . . . . . . . . . . . . . . . . . 20 𝑛𝐵
305 nfcv 2908 . . . . . . . . . . . . . . . . . . . 20 𝑛
306304, 305, 59nfbr 5213 . . . . . . . . . . . . . . . . . . 19 𝑛 𝐵𝑖 / 𝑛𝐴
307303, 306nfim 1895 . . . . . . . . . . . . . . . . . 18 𝑛((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)
308302, 307nfralw 3317 . . . . . . . . . . . . . . . . 17 𝑛𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)
309 breq2 5170 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑖 → (𝑀𝑛𝑀𝑖))
310 breq1 5169 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑖 → (𝑛𝑥𝑖𝑥))
311309, 310anbi12d 631 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑖 → ((𝑀𝑛𝑛𝑥) ↔ (𝑀𝑖𝑖𝑥)))
31262breq2d 5178 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑖 → (𝐵𝐴𝐵𝑖 / 𝑛𝐴))
313311, 312imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑖 → (((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)))
314313ralbidv 3184 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 → (∀𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)))
315308, 314rspc 3623 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℝ+ → (∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) → ∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)))
316298, 301, 315sylc 65 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → ∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴))
317231lep1d 12226 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ≤ (𝑖 + 1))
318233, 317jca 511 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑀𝑖𝑖 ≤ (𝑖 + 1)))
319 breq2 5170 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑖 + 1) → (𝑖𝑥𝑖 ≤ (𝑖 + 1)))
320319anbi2d 629 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑖 + 1) → ((𝑀𝑖𝑖𝑥) ↔ (𝑀𝑖𝑖 ≤ (𝑖 + 1))))
321 eqvisset 3508 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑖 + 1) → (𝑖 + 1) ∈ V)
322 eqtr3 2766 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) → 𝑥 = 𝑛)
32330equcoms 2019 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑛𝐴 = 𝐵)
324322, 323syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) → 𝐴 = 𝐵)
325321, 324csbied 3959 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑖 + 1) → (𝑖 + 1) / 𝑛𝐴 = 𝐵)
326325eqcomd 2746 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑖 + 1) → 𝐵 = (𝑖 + 1) / 𝑛𝐴)
327326breq1d 5176 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑖 + 1) → (𝐵𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴))
328320, 327imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑖 + 1) → (((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴) ↔ ((𝑀𝑖𝑖 ≤ (𝑖 + 1)) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)))
329328rspcv 3631 . . . . . . . . . . . . . . 15 ((𝑖 + 1) ∈ ℝ+ → (∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴) → ((𝑀𝑖𝑖 ≤ (𝑖 + 1)) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)))
330297, 316, 318, 329syl3c 66 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)
331294, 330syldan 590 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)
332218, 217, 331abssuble0d 15481 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)) = (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴))
333332oveq1d 7463 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((abs‘((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) = ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
334291, 333eqtrd 2780 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) = ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
335290abscld 15485 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℝ)
336217, 218subge0d 11880 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (0 ≤ (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ↔ (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴))
337331, 336mpbird 257 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 0 ≤ (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴))
338135peano2nnd 12310 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) ∈ ℕ)
339338nnnn0d 12613 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) ∈ ℕ0)
34019, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35, 93, 260dchrisumlem1 27551 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 + 1) ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
341339, 340syldan 590 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
342335, 287, 219, 337, 341lemul2ad 12235 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
343334, 342eqbrtrd 5188 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
34481, 284, 288, 343fsumle 15847 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
345219recnd 11318 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ∈ ℂ)
34681, 280, 345fsummulc1 15833 . . . . . . . . 9 (𝜑 → (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
347216oveq1d 7463 . . . . . . . . 9 (𝜑 → (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) = (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
348346, 347eqtr3d 2782 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) = (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
349344, 348breqtrd 5192 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
350156, 285, 222, 286, 349letrd 11447 . . . . . 6 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
351134, 156, 215, 222, 283, 350le2addd 11909 . . . . 5 (𝜑 → ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))) ≤ ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) + (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅)))
3521262timesd 12536 . . . . . . . 8 (𝜑 → (2 · (𝐼 + 1) / 𝑛𝐴) = ((𝐼 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴))
353126, 116, 126ppncand 11687 . . . . . . . 8 (𝜑 → (((𝐼 + 1) / 𝑛𝐴 + (𝐽 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) = ((𝐼 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴))
354126, 116addcomd 11492 . . . . . . . . 9 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 + (𝐽 + 1) / 𝑛𝐴) = ((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴))
355354oveq1d 7463 . . . . . . . 8 (𝜑 → (((𝐼 + 1) / 𝑛𝐴 + (𝐽 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) = (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)))
356352, 353, 3553eqtr2d 2786 . . . . . . 7 (𝜑 → (2 · (𝐼 + 1) / 𝑛𝐴) = (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)))
357356oveq1d 7463 . . . . . 6 (𝜑 → ((2 · (𝐼 + 1) / 𝑛𝐴) · 𝑅) = ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) · 𝑅))
358 2cnd 12371 . . . . . . 7 (𝜑 → 2 ∈ ℂ)
359358, 126, 280mul32d 11500 . . . . . 6 (𝜑 → ((2 · (𝐼 + 1) / 𝑛𝐴) · 𝑅) = ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴))
360214recnd 11318 . . . . . . 7 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) ∈ ℂ)
361221recnd 11318 . . . . . . 7 (𝜑 → ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) ∈ ℂ)
362360, 361, 280adddird 11315 . . . . . 6 (𝜑 → ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) · 𝑅) = ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) + (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅)))
363357, 359, 3623eqtr3d 2788 . . . . 5 (𝜑 → ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴) = ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) + (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅)))
364351, 363breqtrrd 5194 . . . 4 (𝜑 → ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))) ≤ ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴))
36590, 157, 100, 213, 364letrd 11447 . . 3 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ≤ ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴))
366 2nn0 12570 . . . . . 6 2 ∈ ℕ0
367 nn0ge0 12578 . . . . . 6 (2 ∈ ℕ0 → 0 ≤ 2)
368366, 367mp1i 13 . . . . 5 (𝜑 → 0 ≤ 2)
369 0red 11293 . . . . . 6 (𝜑 → 0 ∈ ℝ)
370124absge0d 15493 . . . . . 6 (𝜑 → 0 ≤ (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))))
371369, 258, 93, 370, 262letrd 11447 . . . . 5 (𝜑 → 0 ≤ 𝑅)
37292, 93, 368, 371mulge0d 11867 . . . 4 (𝜑 → 0 ≤ (2 · 𝑅))
3734nnrpd 13097 . . . . 5 (𝜑 → (𝐼 + 1) ∈ ℝ+)
374 nfv 1913 . . . . . . . . 9 𝑛(𝑀𝑈𝑈𝑥)
375304, 305, 103nfbr 5213 . . . . . . . . 9 𝑛 𝐵𝑈 / 𝑛𝐴
376374, 375nfim 1895 . . . . . . . 8 𝑛((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)
377302, 376nfralw 3317 . . . . . . 7 𝑛𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)
378 breq2 5170 . . . . . . . . . 10 (𝑛 = 𝑈 → (𝑀𝑛𝑀𝑈))
379 breq1 5169 . . . . . . . . . 10 (𝑛 = 𝑈 → (𝑛𝑥𝑈𝑥))
380378, 379anbi12d 631 . . . . . . . . 9 (𝑛 = 𝑈 → ((𝑀𝑛𝑛𝑥) ↔ (𝑀𝑈𝑈𝑥)))
381105breq2d 5178 . . . . . . . . 9 (𝑛 = 𝑈 → (𝐵𝐴𝐵𝑈 / 𝑛𝐴))
382380, 381imbi12d 344 . . . . . . . 8 (𝑛 = 𝑈 → (((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)))
383382ralbidv 3184 . . . . . . 7 (𝑛 = 𝑈 → (∀𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)))
384377, 383rspc 3623 . . . . . 6 (𝑈 ∈ ℝ+ → (∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) → ∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)))
385101, 300, 384sylc 65 . . . . 5 (𝜑 → ∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴))
386245, 246jca 511 . . . . 5 (𝜑 → (𝑀𝑈𝑈 ≤ (𝐼 + 1)))
387 breq2 5170 . . . . . . . 8 (𝑥 = (𝐼 + 1) → (𝑈𝑥𝑈 ≤ (𝐼 + 1)))
388387anbi2d 629 . . . . . . 7 (𝑥 = (𝐼 + 1) → ((𝑀𝑈𝑈𝑥) ↔ (𝑀𝑈𝑈 ≤ (𝐼 + 1))))
389 eqvisset 3508 . . . . . . . . . 10 (𝑥 = (𝐼 + 1) → (𝐼 + 1) ∈ V)
390 eqtr3 2766 . . . . . . . . . . 11 ((𝑥 = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) → 𝑥 = 𝑛)
391390, 323syl 17 . . . . . . . . . 10 ((𝑥 = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) → 𝐴 = 𝐵)
392389, 391csbied 3959 . . . . . . . . 9 (𝑥 = (𝐼 + 1) → (𝐼 + 1) / 𝑛𝐴 = 𝐵)
393392eqcomd 2746 . . . . . . . 8 (𝑥 = (𝐼 + 1) → 𝐵 = (𝐼 + 1) / 𝑛𝐴)
394393breq1d 5176 . . . . . . 7 (𝑥 = (𝐼 + 1) → (𝐵𝑈 / 𝑛𝐴(𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴))
395388, 394imbi12d 344 . . . . . 6 (𝑥 = (𝐼 + 1) → (((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴) ↔ ((𝑀𝑈𝑈 ≤ (𝐼 + 1)) → (𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴)))
396395rspcv 3631 . . . . 5 ((𝐼 + 1) ∈ ℝ+ → (∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴) → ((𝑀𝑈𝑈 ≤ (𝐼 + 1)) → (𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴)))
397373, 385, 386, 396syl3c 66 . . . 4 (𝜑(𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴)
39899, 108, 94, 372, 397lemul2ad 12235 . . 3 (𝜑 → ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴) ≤ ((2 · 𝑅) · 𝑈 / 𝑛𝐴))
39990, 100, 109, 365, 398letrd 11447 . 2 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ≤ ((2 · 𝑅) · 𝑈 / 𝑛𝐴))
40089, 399eqbrtrd 5188 1 (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) ≤ ((2 · 𝑅) · 𝑈 / 𝑛𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1537  wcel 2108  wne 2946  wral 3067  Vcvv 3488  csb 3921  cun 3974  cin 3975  c0 4352   class class class wbr 5166  cmpt 5249  cfv 6573  (class class class)co 7448  Fincfn 9003  cc 11182  cr 11183  0cc0 11184  1c1 11185   + caddc 11187   · cmul 11189  +∞cpnf 11321  cle 11325  cmin 11520  cn 12293  2c2 12348  0cn0 12553  cz 12639  cuz 12903  +crp 13057  [,)cico 13409  ...cfz 13567  ..^cfzo 13711  seqcseq 14052  abscabs 15283  𝑟 crli 15531  Σcsu 15734  Basecbs 17258  0gc0g 17499  ℤRHomczrh 21533  ℤ/nczn 21536  DChrcdchr 27294
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-inf2 9710  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262  ax-addf 11263  ax-mulf 11264
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-of 7714  df-om 7904  df-1st 8030  df-2nd 8031  df-tpos 8267  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-oadd 8526  df-er 8763  df-ec 8765  df-qs 8769  df-map 8886  df-pm 8887  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-sup 9511  df-inf 9512  df-oi 9579  df-card 10008  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361  df-8 12362  df-9 12363  df-n0 12554  df-xnn0 12626  df-z 12640  df-dec 12759  df-uz 12904  df-rp 13058  df-ico 13413  df-fz 13568  df-fzo 13712  df-fl 13843  df-mod 13921  df-seq 14053  df-exp 14113  df-hash 14380  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285  df-clim 15534  df-rlim 15535  df-sum 15735  df-dvds 16303  df-gcd 16541  df-phi 16813  df-struct 17194  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-ress 17288  df-plusg 17324  df-mulr 17325  df-starv 17326  df-sca 17327  df-vsca 17328  df-ip 17329  df-tset 17330  df-ple 17331  df-ds 17333  df-unif 17334  df-0g 17501  df-imas 17568  df-qus 17569  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-mhm 18818  df-grp 18976  df-minusg 18977  df-sbg 18978  df-mulg 19108  df-subg 19163  df-nsg 19164  df-eqg 19165  df-ghm 19253  df-cmn 19824  df-abl 19825  df-mgp 20162  df-rng 20180  df-ur 20209  df-ring 20262  df-cring 20263  df-oppr 20360  df-dvdsr 20383  df-unit 20384  df-invr 20414  df-rhm 20498  df-subrng 20572  df-subrg 20597  df-lmod 20882  df-lss 20953  df-lsp 20993  df-sra 21195  df-rgmod 21196  df-lidl 21241  df-rsp 21242  df-2idl 21283  df-cnfld 21388  df-zring 21481  df-zrh 21537  df-zn 21540  df-dchr 27295
This theorem is referenced by:  dchrisumlem3  27553
  Copyright terms: Public domain W3C validator