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

Theorem dchrisumlem2 26736
Description: Lemma for dchrisum 26738. 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 13514 . . . . . . . . 9 ((1..^(𝐼 + 1)) ∩ ((𝐼 + 1)..^(𝐽 + 1))) = ∅
21a1i 11 . . . . . . . 8 (𝜑 → ((1..^(𝐼 + 1)) ∩ ((𝐼 + 1)..^(𝐽 + 1))) = ∅)
3 dchrisumlem2.4 . . . . . . . . . . . 12 (𝜑𝐼 ∈ ℕ)
43peano2nnd 12083 . . . . . . . . . . 11 (𝜑 → (𝐼 + 1) ∈ ℕ)
5 nnuz 12714 . . . . . . . . . . 11 ℕ = (ℤ‘1)
64, 5eleqtrdi 2847 . . . . . . . . . 10 (𝜑 → (𝐼 + 1) ∈ (ℤ‘1))
7 dchrisumlem2.5 . . . . . . . . . . 11 (𝜑𝐽 ∈ (ℤ𝐼))
8 eluzp1p1 12703 . . . . . . . . . . 11 (𝐽 ∈ (ℤ𝐼) → (𝐽 + 1) ∈ (ℤ‘(𝐼 + 1)))
97, 8syl 17 . . . . . . . . . 10 (𝜑 → (𝐽 + 1) ∈ (ℤ‘(𝐼 + 1)))
10 elfzuzb 13343 . . . . . . . . . 10 ((𝐼 + 1) ∈ (1...(𝐽 + 1)) ↔ ((𝐼 + 1) ∈ (ℤ‘1) ∧ (𝐽 + 1) ∈ (ℤ‘(𝐼 + 1))))
116, 9, 10sylanbrc 583 . . . . . . . . 9 (𝜑 → (𝐼 + 1) ∈ (1...(𝐽 + 1)))
12 fzosplit 13513 . . . . . . . . 9 ((𝐼 + 1) ∈ (1...(𝐽 + 1)) → (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1))))
1311, 12syl 17 . . . . . . . 8 (𝜑 → (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1))))
14 fzofi 13787 . . . . . . . . 9 (1..^(𝐽 + 1)) ∈ Fin
1514a1i 11 . . . . . . . 8 (𝜑 → (1..^(𝐽 + 1)) ∈ Fin)
16 elfzouz 13484 . . . . . . . . . 10 (𝑖 ∈ (1..^(𝐽 + 1)) → 𝑖 ∈ (ℤ‘1))
1716, 5eleqtrrdi 2848 . . . . . . . . 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 481 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 𝑋𝐷)
24 nnz 12435 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → 𝑖 ∈ ℤ)
2524adantl 482 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℤ)
2618, 19, 20, 21, 23, 25dchrzrhcl 26491 . . . . . . . . . 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 26734 . . . . . . . . . . . . 13 (𝜑 → ((𝑖 ∈ ℝ+𝑖 / 𝑛𝐴 ∈ ℝ) ∧ (𝑖 ∈ (𝑀[,)+∞) → 0 ≤ 𝑖 / 𝑛𝐴)))
3736simpld 495 . . . . . . . . . . . 12 (𝜑 → (𝑖 ∈ ℝ+𝑖 / 𝑛𝐴 ∈ ℝ))
38 nnrp 12834 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → 𝑖 ∈ ℝ+)
3937, 38impel 506 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 𝑖 / 𝑛𝐴 ∈ ℝ)
4039recnd 11096 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → 𝑖 / 𝑛𝐴 ∈ ℂ)
4126, 40mulcld 11088 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
4217, 41sylan2 593 . . . . . . . 8 ((𝜑𝑖 ∈ (1..^(𝐽 + 1))) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
432, 13, 15, 42fsumsplit 15544 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (1..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
44 eluzelz 12685 . . . . . . . . 9 (𝐽 ∈ (ℤ𝐼) → 𝐽 ∈ ℤ)
45 fzval3 13549 . . . . . . . . 9 (𝐽 ∈ ℤ → (1...𝐽) = (1..^(𝐽 + 1)))
467, 44, 453syl 18 . . . . . . . 8 (𝜑 → (1...𝐽) = (1..^(𝐽 + 1)))
4746sumeq1d 15504 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = Σ𝑖 ∈ (1..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
483nnzd 12518 . . . . . . . . . 10 (𝜑𝐼 ∈ ℤ)
49 fzval3 13549 . . . . . . . . . 10 (𝐼 ∈ ℤ → (1...𝐼) = (1..^(𝐼 + 1)))
5048, 49syl 17 . . . . . . . . 9 (𝜑 → (1...𝐼) = (1..^(𝐼 + 1)))
5150sumeq1d 15504 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
5251oveq1d 7344 . . . . . . 7 (𝜑 → (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
5343, 47, 523eqtr4d 2786 . . . . . 6 (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
54 elfznn 13378 . . . . . . . 8 (𝑖 ∈ (1...𝐽) → 𝑖 ∈ ℕ)
55 simpr 485 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
56 nfcv 2904 . . . . . . . . . 10 𝑛𝑖
57 nfcv 2904 . . . . . . . . . . 11 𝑛(𝑋‘(𝐿𝑖))
58 nfcv 2904 . . . . . . . . . . 11 𝑛 ·
59 nfcsb1v 3867 . . . . . . . . . . 11 𝑛𝑖 / 𝑛𝐴
6057, 58, 59nfov 7359 . . . . . . . . . 10 𝑛((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)
61 2fveq3 6824 . . . . . . . . . . 11 (𝑛 = 𝑖 → (𝑋‘(𝐿𝑛)) = (𝑋‘(𝐿𝑖)))
62 csbeq1a 3856 . . . . . . . . . . 11 (𝑛 = 𝑖𝐴 = 𝑖 / 𝑛𝐴)
6361, 62oveq12d 7347 . . . . . . . . . 10 (𝑛 = 𝑖 → ((𝑋‘(𝐿𝑛)) · 𝐴) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
6456, 60, 63, 35fvmptf 6946 . . . . . . . . 9 ((𝑖 ∈ ℕ ∧ ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
6555, 41, 64syl2anc 584 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
6654, 65sylan2 593 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝐽)) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
673, 5eleqtrdi 2847 . . . . . . . 8 (𝜑𝐼 ∈ (ℤ‘1))
68 uztrn 12693 . . . . . . . 8 ((𝐽 ∈ (ℤ𝐼) ∧ 𝐼 ∈ (ℤ‘1)) → 𝐽 ∈ (ℤ‘1))
697, 67, 68syl2anc 584 . . . . . . 7 (𝜑𝐽 ∈ (ℤ‘1))
7054, 41sylan2 593 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝐽)) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
7166, 69, 70fsumser 15533 . . . . . 6 (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (seq1( + , 𝐹)‘𝐽))
7253, 71eqtr3d 2778 . . . . 5 (𝜑 → (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = (seq1( + , 𝐹)‘𝐽))
73 elfznn 13378 . . . . . . 7 (𝑖 ∈ (1...𝐼) → 𝑖 ∈ ℕ)
7473, 65sylan2 593 . . . . . 6 ((𝜑𝑖 ∈ (1...𝐼)) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
7573, 41sylan2 593 . . . . . 6 ((𝜑𝑖 ∈ (1...𝐼)) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
7674, 67, 75fsumser 15533 . . . . 5 (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (seq1( + , 𝐹)‘𝐼))
7772, 76oveq12d 7347 . . . 4 (𝜑 → ((Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) − Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = ((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼)))
78 fzfid 13786 . . . . . 6 (𝜑 → (1...𝐼) ∈ Fin)
7978, 75fsumcl 15536 . . . . 5 (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
80 fzofi 13787 . . . . . . 7 ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin
8180a1i 11 . . . . . 6 (𝜑 → ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin)
82 ssun2 4119 . . . . . . . . 9 ((𝐼 + 1)..^(𝐽 + 1)) ⊆ ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1)))
8382, 13sseqtrrid 3984 . . . . . . . 8 (𝜑 → ((𝐼 + 1)..^(𝐽 + 1)) ⊆ (1..^(𝐽 + 1)))
8483sselda 3931 . . . . . . 7 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ (1..^(𝐽 + 1)))
8584, 42syldan 591 . . . . . 6 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
8681, 85fsumcl 15536 . . . . 5 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
8779, 86pncan2d 11427 . . . 4 (𝜑 → ((Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) − Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
8877, 87eqtr3d 2778 . . 3 (𝜑 → ((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
8988fveq2d 6823 . 2 (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) = (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
9086abscld 15239 . . 3 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ∈ ℝ)
91 2re 12140 . . . . . 6 2 ∈ ℝ
9291a1i 11 . . . . 5 (𝜑 → 2 ∈ ℝ)
93 dchrisum.9 . . . . 5 (𝜑𝑅 ∈ ℝ)
9492, 93remulcld 11098 . . . 4 (𝜑 → (2 · 𝑅) ∈ ℝ)
9539ralrimiva 3139 . . . . 5 (𝜑 → ∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℝ)
96 csbeq1 3845 . . . . . . 7 (𝑖 = (𝐼 + 1) → 𝑖 / 𝑛𝐴 = (𝐼 + 1) / 𝑛𝐴)
9796eleq1d 2821 . . . . . 6 (𝑖 = (𝐼 + 1) → (𝑖 / 𝑛𝐴 ∈ ℝ ↔ (𝐼 + 1) / 𝑛𝐴 ∈ ℝ))
9897rspcv 3566 . . . . 5 ((𝐼 + 1) ∈ ℕ → (∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℝ → (𝐼 + 1) / 𝑛𝐴 ∈ ℝ))
994, 95, 98sylc 65 . . . 4 (𝜑(𝐼 + 1) / 𝑛𝐴 ∈ ℝ)
10094, 99remulcld 11098 . . 3 (𝜑 → ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴) ∈ ℝ)
101 dchrisumlem2.1 . . . . 5 (𝜑𝑈 ∈ ℝ+)
10232ralrimiva 3139 . . . . 5 (𝜑 → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ)
103 nfcsb1v 3867 . . . . . . 7 𝑛𝑈 / 𝑛𝐴
104103nfel1 2920 . . . . . 6 𝑛𝑈 / 𝑛𝐴 ∈ ℝ
105 csbeq1a 3856 . . . . . . 7 (𝑛 = 𝑈𝐴 = 𝑈 / 𝑛𝐴)
106105eleq1d 2821 . . . . . 6 (𝑛 = 𝑈 → (𝐴 ∈ ℝ ↔ 𝑈 / 𝑛𝐴 ∈ ℝ))
107104, 106rspc 3558 . . . . 5 (𝑈 ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → 𝑈 / 𝑛𝐴 ∈ ℝ))
108101, 102, 107sylc 65 . . . 4 (𝜑𝑈 / 𝑛𝐴 ∈ ℝ)
10994, 108remulcld 11098 . . 3 (𝜑 → ((2 · 𝑅) · 𝑈 / 𝑛𝐴) ∈ ℝ)
11069, 5eleqtrrdi 2848 . . . . . . . . . . . 12 (𝜑𝐽 ∈ ℕ)
111110peano2nnd 12083 . . . . . . . . . . 11 (𝜑 → (𝐽 + 1) ∈ ℕ)
112111nnrpd 12863 . . . . . . . . . 10 (𝜑 → (𝐽 + 1) ∈ ℝ+)
11319, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35dchrisumlema 26734 . . . . . . . . . . 11 (𝜑 → (((𝐽 + 1) ∈ ℝ+(𝐽 + 1) / 𝑛𝐴 ∈ ℝ) ∧ ((𝐽 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐽 + 1) / 𝑛𝐴)))
114113simpld 495 . . . . . . . . . 10 (𝜑 → ((𝐽 + 1) ∈ ℝ+(𝐽 + 1) / 𝑛𝐴 ∈ ℝ))
115112, 114mpd 15 . . . . . . . . 9 (𝜑(𝐽 + 1) / 𝑛𝐴 ∈ ℝ)
116115recnd 11096 . . . . . . . 8 (𝜑(𝐽 + 1) / 𝑛𝐴 ∈ ℂ)
117 fzofi 13787 . . . . . . . . . 10 (0..^(𝐽 + 1)) ∈ Fin
118117a1i 11 . . . . . . . . 9 (𝜑 → (0..^(𝐽 + 1)) ∈ Fin)
119 elfzoelz 13480 . . . . . . . . . 10 (𝑛 ∈ (0..^(𝐽 + 1)) → 𝑛 ∈ ℤ)
12022adantr 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℤ) → 𝑋𝐷)
121 simpr 485 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℤ) → 𝑛 ∈ ℤ)
12218, 19, 20, 21, 120, 121dchrzrhcl 26491 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℤ) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
123119, 122sylan2 593 . . . . . . . . 9 ((𝜑𝑛 ∈ (0..^(𝐽 + 1))) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
124118, 123fsumcl 15536 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
125116, 124mulcld 11088 . . . . . . 7 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
12699recnd 11096 . . . . . . . 8 (𝜑(𝐼 + 1) / 𝑛𝐴 ∈ ℂ)
127 fzofi 13787 . . . . . . . . . 10 (0..^(𝐼 + 1)) ∈ Fin
128127a1i 11 . . . . . . . . 9 (𝜑 → (0..^(𝐼 + 1)) ∈ Fin)
129 elfzoelz 13480 . . . . . . . . . 10 (𝑛 ∈ (0..^(𝐼 + 1)) → 𝑛 ∈ ℤ)
130129, 122sylan2 593 . . . . . . . . 9 ((𝜑𝑛 ∈ (0..^(𝐼 + 1))) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
131128, 130fsumcl 15536 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
132126, 131mulcld 11088 . . . . . . 7 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
133125, 132subcld 11425 . . . . . 6 (𝜑 → (((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℂ)
134133abscld 15239 . . . . 5 (𝜑 → (abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ∈ ℝ)
13584, 17syl 17 . . . . . . . 8 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ ℕ)
136 peano2nn 12078 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℕ)
137136nnrpd 12863 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℝ+)
138 nfcsb1v 3867 . . . . . . . . . . . . . . 15 𝑛(𝑖 + 1) / 𝑛𝐴
139138nfel1 2920 . . . . . . . . . . . . . 14 𝑛(𝑖 + 1) / 𝑛𝐴 ∈ ℝ
140 csbeq1a 3856 . . . . . . . . . . . . . . 15 (𝑛 = (𝑖 + 1) → 𝐴 = (𝑖 + 1) / 𝑛𝐴)
141140eleq1d 2821 . . . . . . . . . . . . . 14 (𝑛 = (𝑖 + 1) → (𝐴 ∈ ℝ ↔ (𝑖 + 1) / 𝑛𝐴 ∈ ℝ))
142139, 141rspc 3558 . . . . . . . . . . . . 13 ((𝑖 + 1) ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ))
143142impcom 408 . . . . . . . . . . . 12 ((∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ ∧ (𝑖 + 1) ∈ ℝ+) → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ)
144102, 137, 143syl2an 596 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ)
145144, 39resubcld 11496 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → ((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) ∈ ℝ)
146145recnd 11096 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) ∈ ℂ)
147 fzofi 13787 . . . . . . . . . . . 12 (0..^(𝑖 + 1)) ∈ Fin
148147a1i 11 . . . . . . . . . . 11 (𝜑 → (0..^(𝑖 + 1)) ∈ Fin)
149 elfzoelz 13480 . . . . . . . . . . . 12 (𝑛 ∈ (0..^(𝑖 + 1)) → 𝑛 ∈ ℤ)
150149, 122sylan2 593 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (0..^(𝑖 + 1))) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
151148, 150fsumcl 15536 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
152151adantr 481 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
153146, 152mulcld 11088 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ) → (((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
154135, 153syldan 591 . . . . . . 7 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
15581, 154fsumcl 15536 . . . . . 6 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
156155abscld 15239 . . . . 5 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
157134, 156readdcld 11097 . . . 4 (𝜑 → ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))) ∈ ℝ)
15826, 40mulcomd 11089 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (𝑖 / 𝑛𝐴 · (𝑋‘(𝐿𝑖))))
159 nnnn0 12333 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → 𝑖 ∈ ℕ0)
160159adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ0)
161 nn0uz 12713 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
162160, 161eleqtrdi 2847 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ (ℤ‘0))
163 elfzelz 13349 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0...𝑖) → 𝑛 ∈ ℤ)
164122adantlr 712 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
165163, 164sylan2 593 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ ℕ) ∧ 𝑛 ∈ (0...𝑖)) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
166162, 165, 61fzosump1 15555 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) = (Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) + (𝑋‘(𝐿𝑖))))
167166oveq1d 7344 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))) = ((Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) + (𝑋‘(𝐿𝑖))) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))))
168 fzofi 13787 . . . . . . . . . . . . . . 15 (0..^𝑖) ∈ Fin
169168a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → (0..^𝑖) ∈ Fin)
170 elfzoelz 13480 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0..^𝑖) → 𝑛 ∈ ℤ)
171170, 164sylan2 593 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ ℕ) ∧ 𝑛 ∈ (0..^𝑖)) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
172169, 171fsumcl 15536 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) ∈ ℂ)
173172, 26pncan2d 11427 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) + (𝑋‘(𝐿𝑖))) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))) = (𝑋‘(𝐿𝑖)))
174167, 173eqtr2d 2777 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (𝑋‘(𝐿𝑖)) = (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))))
175174oveq2d 7345 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → (𝑖 / 𝑛𝐴 · (𝑋‘(𝐿𝑖))) = (𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
176158, 175eqtrd 2776 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
177135, 176syldan 591 . . . . . . . 8 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
178177sumeq2dv 15506 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
179 csbeq1 3845 . . . . . . . . 9 (𝑘 = 𝑖𝑘 / 𝑛𝐴 = 𝑖 / 𝑛𝐴)
180 oveq2 7337 . . . . . . . . . 10 (𝑘 = 𝑖 → (0..^𝑘) = (0..^𝑖))
181180sumeq1d 15504 . . . . . . . . 9 (𝑘 = 𝑖 → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))
182179, 181jca 512 . . . . . . . 8 (𝑘 = 𝑖 → (𝑘 / 𝑛𝐴 = 𝑖 / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))))
183 csbeq1 3845 . . . . . . . . 9 (𝑘 = (𝑖 + 1) → 𝑘 / 𝑛𝐴 = (𝑖 + 1) / 𝑛𝐴)
184 oveq2 7337 . . . . . . . . . 10 (𝑘 = (𝑖 + 1) → (0..^𝑘) = (0..^(𝑖 + 1)))
185184sumeq1d 15504 . . . . . . . . 9 (𝑘 = (𝑖 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))
186183, 185jca 512 . . . . . . . 8 (𝑘 = (𝑖 + 1) → (𝑘 / 𝑛𝐴 = (𝑖 + 1) / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))
187 csbeq1 3845 . . . . . . . . 9 (𝑘 = (𝐼 + 1) → 𝑘 / 𝑛𝐴 = (𝐼 + 1) / 𝑛𝐴)
188 oveq2 7337 . . . . . . . . . 10 (𝑘 = (𝐼 + 1) → (0..^𝑘) = (0..^(𝐼 + 1)))
189188sumeq1d 15504 . . . . . . . . 9 (𝑘 = (𝐼 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))
190187, 189jca 512 . . . . . . . 8 (𝑘 = (𝐼 + 1) → (𝑘 / 𝑛𝐴 = (𝐼 + 1) / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))
191 csbeq1 3845 . . . . . . . . 9 (𝑘 = (𝐽 + 1) → 𝑘 / 𝑛𝐴 = (𝐽 + 1) / 𝑛𝐴)
192 oveq2 7337 . . . . . . . . . 10 (𝑘 = (𝐽 + 1) → (0..^𝑘) = (0..^(𝐽 + 1)))
193192sumeq1d 15504 . . . . . . . . 9 (𝑘 = (𝐽 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))
194191, 193jca 512 . . . . . . . 8 (𝑘 = (𝐽 + 1) → (𝑘 / 𝑛𝐴 = (𝐽 + 1) / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))))
19540ralrimiva 3139 . . . . . . . . 9 (𝜑 → ∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℂ)
196 elfzuz 13345 . . . . . . . . . 10 (𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1)) → 𝑘 ∈ (ℤ‘(𝐼 + 1)))
197 eluznn 12751 . . . . . . . . . 10 (((𝐼 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(𝐼 + 1))) → 𝑘 ∈ ℕ)
1984, 196, 197syl2an 596 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → 𝑘 ∈ ℕ)
199 csbeq1 3845 . . . . . . . . . . 11 (𝑖 = 𝑘𝑖 / 𝑛𝐴 = 𝑘 / 𝑛𝐴)
200199eleq1d 2821 . . . . . . . . . 10 (𝑖 = 𝑘 → (𝑖 / 𝑛𝐴 ∈ ℂ ↔ 𝑘 / 𝑛𝐴 ∈ ℂ))
201200rspccva 3569 . . . . . . . . 9 ((∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) → 𝑘 / 𝑛𝐴 ∈ ℂ)
202195, 198, 201syl2an2r 682 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → 𝑘 / 𝑛𝐴 ∈ ℂ)
203 fzofi 13787 . . . . . . . . . . 11 (0..^𝑘) ∈ Fin
204203a1i 11 . . . . . . . . . 10 (𝜑 → (0..^𝑘) ∈ Fin)
205 elfzoelz 13480 . . . . . . . . . . 11 (𝑛 ∈ (0..^𝑘) → 𝑛 ∈ ℤ)
206205, 122sylan2 593 . . . . . . . . . 10 ((𝜑𝑛 ∈ (0..^𝑘)) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
207204, 206fsumcl 15536 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) ∈ ℂ)
208207adantr 481 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) ∈ ℂ)
209182, 186, 190, 194, 9, 202, 208fsumparts 15609 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))) = ((((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
210178, 209eqtrd 2776 . . . . . 6 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = ((((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
211210fveq2d 6823 . . . . 5 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = (abs‘((((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))))
212133, 155abs2dif2d 15261 . . . . 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 5111 . . . 4 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ≤ ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))))
214115, 99readdcld 11097 . . . . . . 7 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) ∈ ℝ)
215214, 93remulcld 11098 . . . . . 6 (𝜑 → (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) ∈ ℝ)
216179, 183, 187, 191, 9, 202telfsumo 15605 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) = ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴))
217135, 39syldan 591 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 / 𝑛𝐴 ∈ ℝ)
218135, 144syldan 591 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ)
219217, 218resubcld 11496 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ∈ ℝ)
22081, 219fsumrecl 15537 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ∈ ℝ)
221216, 220eqeltrrd 2838 . . . . . . 7 (𝜑 → ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) ∈ ℝ)
222221, 93remulcld 11098 . . . . . 6 (𝜑 → (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅) ∈ ℝ)
223125abscld 15239 . . . . . . . 8 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
224132abscld 15239 . . . . . . . 8 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
225223, 224readdcld 11097 . . . . . . 7 (𝜑 → ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ∈ ℝ)
226125, 132abs2dif2d 15261 . . . . . . 7 (𝜑 → (abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))))
227115, 93remulcld 11098 . . . . . . . . 9 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 · 𝑅) ∈ ℝ)
22899, 93remulcld 11098 . . . . . . . . 9 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 · 𝑅) ∈ ℝ)
229116, 124absmuld 15257 . . . . . . . . . . 11 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) = ((abs‘(𝐽 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))))
230 eluzelre 12686 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (ℤ𝑀) → 𝑖 ∈ ℝ)
231230adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℝ)
232 eluzle 12688 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (ℤ𝑀) → 𝑀𝑖)
233232adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀𝑖)
23431nnred 12081 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℝ)
235234adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ)
236 elicopnf 13270 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℝ → (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀𝑖)))
237235, 236syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀𝑖)))
238231, 233, 237mpbir2and 710 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ (𝑀[,)+∞))
239238ex 413 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑖 ∈ (ℤ𝑀) → 𝑖 ∈ (𝑀[,)+∞)))
240239ssrdv 3937 . . . . . . . . . . . . . . 15 (𝜑 → (ℤ𝑀) ⊆ (𝑀[,)+∞))
24131nnzd 12518 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℤ)
24248peano2zd 12522 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐼 + 1) ∈ ℤ)
243101rpred 12865 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 ∈ ℝ)
2444nnred 12081 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐼 + 1) ∈ ℝ)
245 dchrisumlem2.2 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀𝑈)
246 dchrisumlem2.3 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 ≤ (𝐼 + 1))
247234, 243, 244, 245, 246letrd 11225 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ≤ (𝐼 + 1))
248 eluz2 12681 . . . . . . . . . . . . . . . . 17 ((𝐼 + 1) ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝐼 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝐼 + 1)))
249241, 242, 247, 248syl3anbrc 1342 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐼 + 1) ∈ (ℤ𝑀))
250 uztrn 12693 . . . . . . . . . . . . . . . 16 (((𝐽 + 1) ∈ (ℤ‘(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (ℤ𝑀)) → (𝐽 + 1) ∈ (ℤ𝑀))
2519, 249, 250syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → (𝐽 + 1) ∈ (ℤ𝑀))
252240, 251sseldd 3932 . . . . . . . . . . . . . 14 (𝜑 → (𝐽 + 1) ∈ (𝑀[,)+∞))
253113simprd 496 . . . . . . . . . . . . . 14 (𝜑 → ((𝐽 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐽 + 1) / 𝑛𝐴))
254252, 253mpd 15 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ (𝐽 + 1) / 𝑛𝐴)
255115, 254absidd 15225 . . . . . . . . . . . 12 (𝜑 → (abs‘(𝐽 + 1) / 𝑛𝐴) = (𝐽 + 1) / 𝑛𝐴)
256255oveq1d 7344 . . . . . . . . . . 11 (𝜑 → ((abs‘(𝐽 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐽 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))))
257229, 256eqtrd 2776 . . . . . . . . . 10 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐽 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))))
258124abscld 15239 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ∈ ℝ)
259111nnnn0d 12386 . . . . . . . . . . . 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 26735 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐽 + 1) ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
262259, 261mpdan 684 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
263258, 93, 115, 254, 262lemul2ad 12008 . . . . . . . . . 10 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐽 + 1) / 𝑛𝐴 · 𝑅))
264257, 263eqbrtrd 5111 . . . . . . . . 9 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐽 + 1) / 𝑛𝐴 · 𝑅))
265126, 131absmuld 15257 . . . . . . . . . . 11 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) = ((abs‘(𝐼 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))))
266240, 249sseldd 3932 . . . . . . . . . . . . . 14 (𝜑 → (𝐼 + 1) ∈ (𝑀[,)+∞))
26719, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35dchrisumlema 26734 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐼 + 1) ∈ ℝ+(𝐼 + 1) / 𝑛𝐴 ∈ ℝ) ∧ ((𝐼 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐼 + 1) / 𝑛𝐴)))
268267simprd 496 . . . . . . . . . . . . . 14 (𝜑 → ((𝐼 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐼 + 1) / 𝑛𝐴))
269266, 268mpd 15 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ (𝐼 + 1) / 𝑛𝐴)
27099, 269absidd 15225 . . . . . . . . . . . 12 (𝜑 → (abs‘(𝐼 + 1) / 𝑛𝐴) = (𝐼 + 1) / 𝑛𝐴)
271270oveq1d 7344 . . . . . . . . . . 11 (𝜑 → ((abs‘(𝐼 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐼 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))))
272265, 271eqtrd 2776 . . . . . . . . . 10 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐼 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))))
273131abscld 15239 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ∈ ℝ)
2744nnnn0d 12386 . . . . . . . . . . . 12 (𝜑 → (𝐼 + 1) ∈ ℕ0)
27519, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35, 93, 260dchrisumlem1 26735 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐼 + 1) ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
276274, 275mpdan 684 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
277273, 93, 99, 269, 276lemul2ad 12008 . . . . . . . . . 10 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐼 + 1) / 𝑛𝐴 · 𝑅))
278272, 277eqbrtrd 5111 . . . . . . . . 9 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐼 + 1) / 𝑛𝐴 · 𝑅))
279223, 224, 227, 228, 264, 278le2addd 11687 . . . . . . . 8 (𝜑 → ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ (((𝐽 + 1) / 𝑛𝐴 · 𝑅) + ((𝐼 + 1) / 𝑛𝐴 · 𝑅)))
28093recnd 11096 . . . . . . . . 9 (𝜑𝑅 ∈ ℂ)
281116, 126, 280adddird 11093 . . . . . . . 8 (𝜑 → (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) = (((𝐽 + 1) / 𝑛𝐴 · 𝑅) + ((𝐼 + 1) / 𝑛𝐴 · 𝑅)))
282279, 281breqtrrd 5117 . . . . . . 7 (𝜑 → ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅))
283134, 225, 215, 226, 282letrd 11225 . . . . . 6 (𝜑 → (abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅))
284154abscld 15239 . . . . . . . 8 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
28581, 284fsumrecl 15537 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
28681, 154fsumabs 15604 . . . . . . 7 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
28793adantr 481 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑅 ∈ ℝ)
288219, 287remulcld 11098 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) ∈ ℝ)
289135, 146syldan 591 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) ∈ ℂ)
290151adantr 481 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
291289, 290absmuld 15257 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) = ((abs‘((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
292 elfzouz 13484 . . . . . . . . . . . . . . 15 (𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1)) → 𝑖 ∈ (ℤ‘(𝐼 + 1)))
293 uztrn 12693 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (ℤ‘(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (ℤ𝑀)) → 𝑖 ∈ (ℤ𝑀))
294292, 249, 293syl2anr 597 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ (ℤ𝑀))
295 eluznn 12751 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℕ ∧ 𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℕ)
29631, 295sylan 580 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℕ)
297296, 137syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑖 + 1) ∈ ℝ+)
298296nnrpd 12863 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℝ+)
299333expia 1120 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+)) → ((𝑀𝑛𝑛𝑥) → 𝐵𝐴))
300299ralrimivva 3193 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴))
301300adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → ∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴))
302 nfcv 2904 . . . . . . . . . . . . . . . . . 18 𝑛+
303 nfv 1916 . . . . . . . . . . . . . . . . . . 19 𝑛(𝑀𝑖𝑖𝑥)
304 nfcv 2904 . . . . . . . . . . . . . . . . . . . 20 𝑛𝐵
305 nfcv 2904 . . . . . . . . . . . . . . . . . . . 20 𝑛
306304, 305, 59nfbr 5136 . . . . . . . . . . . . . . . . . . 19 𝑛 𝐵𝑖 / 𝑛𝐴
307303, 306nfim 1898 . . . . . . . . . . . . . . . . . 18 𝑛((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)
308302, 307nfralw 3290 . . . . . . . . . . . . . . . . 17 𝑛𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)
309 breq2 5093 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑖 → (𝑀𝑛𝑀𝑖))
310 breq1 5092 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑖 → (𝑛𝑥𝑖𝑥))
311309, 310anbi12d 631 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑖 → ((𝑀𝑛𝑛𝑥) ↔ (𝑀𝑖𝑖𝑥)))
31262breq2d 5101 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑖 → (𝐵𝐴𝐵𝑖 / 𝑛𝐴))
313311, 312imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑖 → (((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)))
314313ralbidv 3170 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 → (∀𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)))
315308, 314rspc 3558 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℝ+ → (∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) → ∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)))
316298, 301, 315sylc 65 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → ∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴))
317231lep1d 11999 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ≤ (𝑖 + 1))
318233, 317jca 512 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑀𝑖𝑖 ≤ (𝑖 + 1)))
319 breq2 5093 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑖 + 1) → (𝑖𝑥𝑖 ≤ (𝑖 + 1)))
320319anbi2d 629 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑖 + 1) → ((𝑀𝑖𝑖𝑥) ↔ (𝑀𝑖𝑖 ≤ (𝑖 + 1))))
321 eqvisset 3458 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑖 + 1) → (𝑖 + 1) ∈ V)
322 eqtr3 2762 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) → 𝑥 = 𝑛)
32330equcoms 2022 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑛𝐴 = 𝐵)
324322, 323syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) → 𝐴 = 𝐵)
325321, 324csbied 3880 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑖 + 1) → (𝑖 + 1) / 𝑛𝐴 = 𝐵)
326325eqcomd 2742 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑖 + 1) → 𝐵 = (𝑖 + 1) / 𝑛𝐴)
327326breq1d 5099 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑖 + 1) → (𝐵𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴))
328320, 327imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑖 + 1) → (((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴) ↔ ((𝑀𝑖𝑖 ≤ (𝑖 + 1)) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)))
329328rspcv 3566 . . . . . . . . . . . . . . 15 ((𝑖 + 1) ∈ ℝ+ → (∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴) → ((𝑀𝑖𝑖 ≤ (𝑖 + 1)) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)))
330297, 316, 318, 329syl3c 66 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)
331294, 330syldan 591 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)
332218, 217, 331abssuble0d 15235 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)) = (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴))
333332oveq1d 7344 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((abs‘((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) = ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
334291, 333eqtrd 2776 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) = ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
335290abscld 15239 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℝ)
336217, 218subge0d 11658 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (0 ≤ (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ↔ (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴))
337331, 336mpbird 256 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 0 ≤ (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴))
338135peano2nnd 12083 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) ∈ ℕ)
339338nnnn0d 12386 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) ∈ ℕ0)
34019, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35, 93, 260dchrisumlem1 26735 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 + 1) ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
341339, 340syldan 591 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
342335, 287, 219, 337, 341lemul2ad 12008 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
343334, 342eqbrtrd 5111 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
34481, 284, 288, 343fsumle 15602 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
345219recnd 11096 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ∈ ℂ)
34681, 280, 345fsummulc1 15588 . . . . . . . . 9 (𝜑 → (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
347216oveq1d 7344 . . . . . . . . 9 (𝜑 → (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) = (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
348346, 347eqtr3d 2778 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) = (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
349344, 348breqtrd 5115 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
350156, 285, 222, 286, 349letrd 11225 . . . . . 6 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
351134, 156, 215, 222, 283, 350le2addd 11687 . . . . 5 (𝜑 → ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))) ≤ ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) + (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅)))
3521262timesd 12309 . . . . . . . 8 (𝜑 → (2 · (𝐼 + 1) / 𝑛𝐴) = ((𝐼 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴))
353126, 116, 126ppncand 11465 . . . . . . . 8 (𝜑 → (((𝐼 + 1) / 𝑛𝐴 + (𝐽 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) = ((𝐼 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴))
354126, 116addcomd 11270 . . . . . . . . 9 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 + (𝐽 + 1) / 𝑛𝐴) = ((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴))
355354oveq1d 7344 . . . . . . . 8 (𝜑 → (((𝐼 + 1) / 𝑛𝐴 + (𝐽 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) = (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)))
356352, 353, 3553eqtr2d 2782 . . . . . . 7 (𝜑 → (2 · (𝐼 + 1) / 𝑛𝐴) = (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)))
357356oveq1d 7344 . . . . . 6 (𝜑 → ((2 · (𝐼 + 1) / 𝑛𝐴) · 𝑅) = ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) · 𝑅))
358 2cnd 12144 . . . . . . 7 (𝜑 → 2 ∈ ℂ)
359358, 126, 280mul32d 11278 . . . . . 6 (𝜑 → ((2 · (𝐼 + 1) / 𝑛𝐴) · 𝑅) = ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴))
360214recnd 11096 . . . . . . 7 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) ∈ ℂ)
361221recnd 11096 . . . . . . 7 (𝜑 → ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) ∈ ℂ)
362360, 361, 280adddird 11093 . . . . . 6 (𝜑 → ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) · 𝑅) = ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) + (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅)))
363357, 359, 3623eqtr3d 2784 . . . . 5 (𝜑 → ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴) = ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) + (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅)))
364351, 363breqtrrd 5117 . . . 4 (𝜑 → ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))) ≤ ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴))
36590, 157, 100, 213, 364letrd 11225 . . 3 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ≤ ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴))
366 2nn0 12343 . . . . . 6 2 ∈ ℕ0
367 nn0ge0 12351 . . . . . 6 (2 ∈ ℕ0 → 0 ≤ 2)
368366, 367mp1i 13 . . . . 5 (𝜑 → 0 ≤ 2)
369 0red 11071 . . . . . 6 (𝜑 → 0 ∈ ℝ)
370124absge0d 15247 . . . . . 6 (𝜑 → 0 ≤ (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))))
371369, 258, 93, 370, 262letrd 11225 . . . . 5 (𝜑 → 0 ≤ 𝑅)
37292, 93, 368, 371mulge0d 11645 . . . 4 (𝜑 → 0 ≤ (2 · 𝑅))
3734nnrpd 12863 . . . . 5 (𝜑 → (𝐼 + 1) ∈ ℝ+)
374 nfv 1916 . . . . . . . . 9 𝑛(𝑀𝑈𝑈𝑥)
375304, 305, 103nfbr 5136 . . . . . . . . 9 𝑛 𝐵𝑈 / 𝑛𝐴
376374, 375nfim 1898 . . . . . . . 8 𝑛((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)
377302, 376nfralw 3290 . . . . . . 7 𝑛𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)
378 breq2 5093 . . . . . . . . . 10 (𝑛 = 𝑈 → (𝑀𝑛𝑀𝑈))
379 breq1 5092 . . . . . . . . . 10 (𝑛 = 𝑈 → (𝑛𝑥𝑈𝑥))
380378, 379anbi12d 631 . . . . . . . . 9 (𝑛 = 𝑈 → ((𝑀𝑛𝑛𝑥) ↔ (𝑀𝑈𝑈𝑥)))
381105breq2d 5101 . . . . . . . . 9 (𝑛 = 𝑈 → (𝐵𝐴𝐵𝑈 / 𝑛𝐴))
382380, 381imbi12d 344 . . . . . . . 8 (𝑛 = 𝑈 → (((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)))
383382ralbidv 3170 . . . . . . 7 (𝑛 = 𝑈 → (∀𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)))
384377, 383rspc 3558 . . . . . 6 (𝑈 ∈ ℝ+ → (∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) → ∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)))
385101, 300, 384sylc 65 . . . . 5 (𝜑 → ∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴))
386245, 246jca 512 . . . . 5 (𝜑 → (𝑀𝑈𝑈 ≤ (𝐼 + 1)))
387 breq2 5093 . . . . . . . 8 (𝑥 = (𝐼 + 1) → (𝑈𝑥𝑈 ≤ (𝐼 + 1)))
388387anbi2d 629 . . . . . . 7 (𝑥 = (𝐼 + 1) → ((𝑀𝑈𝑈𝑥) ↔ (𝑀𝑈𝑈 ≤ (𝐼 + 1))))
389 eqvisset 3458 . . . . . . . . . 10 (𝑥 = (𝐼 + 1) → (𝐼 + 1) ∈ V)
390 eqtr3 2762 . . . . . . . . . . 11 ((𝑥 = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) → 𝑥 = 𝑛)
391390, 323syl 17 . . . . . . . . . 10 ((𝑥 = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) → 𝐴 = 𝐵)
392389, 391csbied 3880 . . . . . . . . 9 (𝑥 = (𝐼 + 1) → (𝐼 + 1) / 𝑛𝐴 = 𝐵)
393392eqcomd 2742 . . . . . . . 8 (𝑥 = (𝐼 + 1) → 𝐵 = (𝐼 + 1) / 𝑛𝐴)
394393breq1d 5099 . . . . . . 7 (𝑥 = (𝐼 + 1) → (𝐵𝑈 / 𝑛𝐴(𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴))
395388, 394imbi12d 344 . . . . . 6 (𝑥 = (𝐼 + 1) → (((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴) ↔ ((𝑀𝑈𝑈 ≤ (𝐼 + 1)) → (𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴)))
396395rspcv 3566 . . . . 5 ((𝐼 + 1) ∈ ℝ+ → (∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴) → ((𝑀𝑈𝑈 ≤ (𝐼 + 1)) → (𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴)))
397373, 385, 386, 396syl3c 66 . . . 4 (𝜑(𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴)
39899, 108, 94, 372, 397lemul2ad 12008 . . 3 (𝜑 → ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴) ≤ ((2 · 𝑅) · 𝑈 / 𝑛𝐴))
39990, 100, 109, 365, 398letrd 11225 . 2 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ≤ ((2 · 𝑅) · 𝑈 / 𝑛𝐴))
40089, 399eqbrtrd 5111 1 (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) ≤ ((2 · 𝑅) · 𝑈 / 𝑛𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wcel 2105  wne 2940  wral 3061  Vcvv 3441  csb 3842  cun 3895  cin 3896  c0 4268   class class class wbr 5089  cmpt 5172  cfv 6473  (class class class)co 7329  Fincfn 8796  cc 10962  cr 10963  0cc0 10964  1c1 10965   + caddc 10967   · cmul 10969  +∞cpnf 11099  cle 11103  cmin 11298  cn 12066  2c2 12121  0cn0 12326  cz 12412  cuz 12675  +crp 12823  [,)cico 13174  ...cfz 13332  ..^cfzo 13475  seqcseq 13814  abscabs 15036  𝑟 crli 15285  Σcsu 15488  Basecbs 17001  0gc0g 17239  ℤRHomczrh 20799  ℤ/nczn 20802  DChrcdchr 26478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5226  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-inf2 9490  ax-cnex 11020  ax-resscn 11021  ax-1cn 11022  ax-icn 11023  ax-addcl 11024  ax-addrcl 11025  ax-mulcl 11026  ax-mulrcl 11027  ax-mulcom 11028  ax-addass 11029  ax-mulass 11030  ax-distr 11031  ax-i2m1 11032  ax-1ne0 11033  ax-1rid 11034  ax-rnegex 11035  ax-rrecex 11036  ax-cnre 11037  ax-pre-lttri 11038  ax-pre-lttrn 11039  ax-pre-ltadd 11040  ax-pre-mulgt0 11041  ax-pre-sup 11042  ax-addf 11043  ax-mulf 11044
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-tp 4577  df-op 4579  df-uni 4852  df-int 4894  df-iun 4940  df-br 5090  df-opab 5152  df-mpt 5173  df-tr 5207  df-id 5512  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-se 5570  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6232  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-isom 6482  df-riota 7286  df-ov 7332  df-oprab 7333  df-mpo 7334  df-of 7587  df-om 7773  df-1st 7891  df-2nd 7892  df-tpos 8104  df-frecs 8159  df-wrecs 8190  df-recs 8264  df-rdg 8303  df-1o 8359  df-oadd 8363  df-er 8561  df-ec 8563  df-qs 8567  df-map 8680  df-pm 8681  df-en 8797  df-dom 8798  df-sdom 8799  df-fin 8800  df-sup 9291  df-inf 9292  df-oi 9359  df-card 9788  df-pnf 11104  df-mnf 11105  df-xr 11106  df-ltxr 11107  df-le 11108  df-sub 11300  df-neg 11301  df-div 11726  df-nn 12067  df-2 12129  df-3 12130  df-4 12131  df-5 12132  df-6 12133  df-7 12134  df-8 12135  df-9 12136  df-n0 12327  df-xnn0 12399  df-z 12413  df-dec 12531  df-uz 12676  df-rp 12824  df-ico 13178  df-fz 13333  df-fzo 13476  df-fl 13605  df-mod 13683  df-seq 13815  df-exp 13876  df-hash 14138  df-cj 14901  df-re 14902  df-im 14903  df-sqrt 15037  df-abs 15038  df-clim 15288  df-rlim 15289  df-sum 15489  df-dvds 16055  df-gcd 16293  df-phi 16556  df-struct 16937  df-sets 16954  df-slot 16972  df-ndx 16984  df-base 17002  df-ress 17031  df-plusg 17064  df-mulr 17065  df-starv 17066  df-sca 17067  df-vsca 17068  df-ip 17069  df-tset 17070  df-ple 17071  df-ds 17073  df-unif 17074  df-0g 17241  df-imas 17308  df-qus 17309  df-mgm 18415  df-sgrp 18464  df-mnd 18475  df-mhm 18519  df-grp 18668  df-minusg 18669  df-sbg 18670  df-mulg 18789  df-subg 18840  df-nsg 18841  df-eqg 18842  df-ghm 18920  df-cmn 19475  df-abl 19476  df-mgp 19808  df-ur 19825  df-ring 19872  df-cring 19873  df-oppr 19949  df-dvdsr 19970  df-unit 19971  df-invr 20001  df-rnghom 20046  df-subrg 20119  df-lmod 20223  df-lss 20292  df-lsp 20332  df-sra 20532  df-rgmod 20533  df-lidl 20534  df-rsp 20535  df-2idl 20601  df-cnfld 20696  df-zring 20769  df-zrh 20803  df-zn 20806  df-dchr 26479
This theorem is referenced by:  dchrisumlem3  26737
  Copyright terms: Public domain W3C validator