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

Theorem dchrisumlem2 26088
 Description: Lemma for dchrisum 26090. 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 13073 . . . . . . . . 9 ((1..^(𝐼 + 1)) ∩ ((𝐼 + 1)..^(𝐽 + 1))) = ∅
21a1i 11 . . . . . . . 8 (𝜑 → ((1..^(𝐼 + 1)) ∩ ((𝐼 + 1)..^(𝐽 + 1))) = ∅)
3 dchrisumlem2.4 . . . . . . . . . . . 12 (𝜑𝐼 ∈ ℕ)
43peano2nnd 11649 . . . . . . . . . . 11 (𝜑 → (𝐼 + 1) ∈ ℕ)
5 nnuz 12276 . . . . . . . . . . 11 ℕ = (ℤ‘1)
64, 5eleqtrdi 2900 . . . . . . . . . 10 (𝜑 → (𝐼 + 1) ∈ (ℤ‘1))
7 dchrisumlem2.5 . . . . . . . . . . 11 (𝜑𝐽 ∈ (ℤ𝐼))
8 eluzp1p1 12265 . . . . . . . . . . 11 (𝐽 ∈ (ℤ𝐼) → (𝐽 + 1) ∈ (ℤ‘(𝐼 + 1)))
97, 8syl 17 . . . . . . . . . 10 (𝜑 → (𝐽 + 1) ∈ (ℤ‘(𝐼 + 1)))
10 elfzuzb 12903 . . . . . . . . . 10 ((𝐼 + 1) ∈ (1...(𝐽 + 1)) ↔ ((𝐼 + 1) ∈ (ℤ‘1) ∧ (𝐽 + 1) ∈ (ℤ‘(𝐼 + 1))))
116, 9, 10sylanbrc 586 . . . . . . . . 9 (𝜑 → (𝐼 + 1) ∈ (1...(𝐽 + 1)))
12 fzosplit 13072 . . . . . . . . 9 ((𝐼 + 1) ∈ (1...(𝐽 + 1)) → (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1))))
1311, 12syl 17 . . . . . . . 8 (𝜑 → (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1))))
14 fzofi 13344 . . . . . . . . 9 (1..^(𝐽 + 1)) ∈ Fin
1514a1i 11 . . . . . . . 8 (𝜑 → (1..^(𝐽 + 1)) ∈ Fin)
16 elfzouz 13044 . . . . . . . . . 10 (𝑖 ∈ (1..^(𝐽 + 1)) → 𝑖 ∈ (ℤ‘1))
1716, 5eleqtrrdi 2901 . . . . . . . . 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 484 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 𝑋𝐷)
24 nnz 11999 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → 𝑖 ∈ ℤ)
2524adantl 485 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℤ)
2618, 19, 20, 21, 23, 25dchrzrhcl 25843 . . . . . . . . . 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 26086 . . . . . . . . . . . . 13 (𝜑 → ((𝑖 ∈ ℝ+𝑖 / 𝑛𝐴 ∈ ℝ) ∧ (𝑖 ∈ (𝑀[,)+∞) → 0 ≤ 𝑖 / 𝑛𝐴)))
3736simpld 498 . . . . . . . . . . . 12 (𝜑 → (𝑖 ∈ ℝ+𝑖 / 𝑛𝐴 ∈ ℝ))
38 nnrp 12395 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → 𝑖 ∈ ℝ+)
3937, 38impel 509 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 𝑖 / 𝑛𝐴 ∈ ℝ)
4039recnd 10665 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → 𝑖 / 𝑛𝐴 ∈ ℂ)
4126, 40mulcld 10657 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
4217, 41sylan2 595 . . . . . . . 8 ((𝜑𝑖 ∈ (1..^(𝐽 + 1))) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
432, 13, 15, 42fsumsplit 15096 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (1..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
44 eluzelz 12248 . . . . . . . . 9 (𝐽 ∈ (ℤ𝐼) → 𝐽 ∈ ℤ)
45 fzval3 13108 . . . . . . . . 9 (𝐽 ∈ ℤ → (1...𝐽) = (1..^(𝐽 + 1)))
467, 44, 453syl 18 . . . . . . . 8 (𝜑 → (1...𝐽) = (1..^(𝐽 + 1)))
4746sumeq1d 15057 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = Σ𝑖 ∈ (1..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
483nnzd 12081 . . . . . . . . . 10 (𝜑𝐼 ∈ ℤ)
49 fzval3 13108 . . . . . . . . . 10 (𝐼 ∈ ℤ → (1...𝐼) = (1..^(𝐼 + 1)))
5048, 49syl 17 . . . . . . . . 9 (𝜑 → (1...𝐼) = (1..^(𝐼 + 1)))
5150sumeq1d 15057 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
5251oveq1d 7155 . . . . . . 7 (𝜑 → (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
5343, 47, 523eqtr4d 2843 . . . . . 6 (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
54 elfznn 12938 . . . . . . . 8 (𝑖 ∈ (1...𝐽) → 𝑖 ∈ ℕ)
55 simpr 488 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
56 nfcv 2955 . . . . . . . . . 10 𝑛𝑖
57 nfcv 2955 . . . . . . . . . . 11 𝑛(𝑋‘(𝐿𝑖))
58 nfcv 2955 . . . . . . . . . . 11 𝑛 ·
59 nfcsb1v 3852 . . . . . . . . . . 11 𝑛𝑖 / 𝑛𝐴
6057, 58, 59nfov 7170 . . . . . . . . . 10 𝑛((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)
61 2fveq3 6655 . . . . . . . . . . 11 (𝑛 = 𝑖 → (𝑋‘(𝐿𝑛)) = (𝑋‘(𝐿𝑖)))
62 csbeq1a 3842 . . . . . . . . . . 11 (𝑛 = 𝑖𝐴 = 𝑖 / 𝑛𝐴)
6361, 62oveq12d 7158 . . . . . . . . . 10 (𝑛 = 𝑖 → ((𝑋‘(𝐿𝑛)) · 𝐴) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
6456, 60, 63, 35fvmptf 6771 . . . . . . . . 9 ((𝑖 ∈ ℕ ∧ ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
6555, 41, 64syl2anc 587 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
6654, 65sylan2 595 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝐽)) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
673, 5eleqtrdi 2900 . . . . . . . 8 (𝜑𝐼 ∈ (ℤ‘1))
68 uztrn 12256 . . . . . . . 8 ((𝐽 ∈ (ℤ𝐼) ∧ 𝐼 ∈ (ℤ‘1)) → 𝐽 ∈ (ℤ‘1))
697, 67, 68syl2anc 587 . . . . . . 7 (𝜑𝐽 ∈ (ℤ‘1))
7054, 41sylan2 595 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝐽)) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
7166, 69, 70fsumser 15086 . . . . . 6 (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (seq1( + , 𝐹)‘𝐽))
7253, 71eqtr3d 2835 . . . . 5 (𝜑 → (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = (seq1( + , 𝐹)‘𝐽))
73 elfznn 12938 . . . . . . 7 (𝑖 ∈ (1...𝐼) → 𝑖 ∈ ℕ)
7473, 65sylan2 595 . . . . . 6 ((𝜑𝑖 ∈ (1...𝐼)) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
7573, 41sylan2 595 . . . . . 6 ((𝜑𝑖 ∈ (1...𝐼)) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
7674, 67, 75fsumser 15086 . . . . 5 (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (seq1( + , 𝐹)‘𝐼))
7772, 76oveq12d 7158 . . . 4 (𝜑 → ((Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) − Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = ((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼)))
78 fzfid 13343 . . . . . 6 (𝜑 → (1...𝐼) ∈ Fin)
7978, 75fsumcl 15089 . . . . 5 (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
80 fzofi 13344 . . . . . . 7 ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin
8180a1i 11 . . . . . 6 (𝜑 → ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin)
82 ssun2 4100 . . . . . . . . 9 ((𝐼 + 1)..^(𝐽 + 1)) ⊆ ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1)))
8382, 13sseqtrrid 3968 . . . . . . . 8 (𝜑 → ((𝐼 + 1)..^(𝐽 + 1)) ⊆ (1..^(𝐽 + 1)))
8483sselda 3915 . . . . . . 7 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ (1..^(𝐽 + 1)))
8584, 42syldan 594 . . . . . 6 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
8681, 85fsumcl 15089 . . . . 5 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
8779, 86pncan2d 10995 . . . 4 (𝜑 → ((Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) − Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
8877, 87eqtr3d 2835 . . 3 (𝜑 → ((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
8988fveq2d 6654 . 2 (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) = (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
9086abscld 14795 . . 3 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ∈ ℝ)
91 2re 11706 . . . . . 6 2 ∈ ℝ
9291a1i 11 . . . . 5 (𝜑 → 2 ∈ ℝ)
93 dchrisum.9 . . . . 5 (𝜑𝑅 ∈ ℝ)
9492, 93remulcld 10667 . . . 4 (𝜑 → (2 · 𝑅) ∈ ℝ)
9539ralrimiva 3149 . . . . 5 (𝜑 → ∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℝ)
96 csbeq1 3831 . . . . . . 7 (𝑖 = (𝐼 + 1) → 𝑖 / 𝑛𝐴 = (𝐼 + 1) / 𝑛𝐴)
9796eleq1d 2874 . . . . . 6 (𝑖 = (𝐼 + 1) → (𝑖 / 𝑛𝐴 ∈ ℝ ↔ (𝐼 + 1) / 𝑛𝐴 ∈ ℝ))
9897rspcv 3566 . . . . 5 ((𝐼 + 1) ∈ ℕ → (∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℝ → (𝐼 + 1) / 𝑛𝐴 ∈ ℝ))
994, 95, 98sylc 65 . . . 4 (𝜑(𝐼 + 1) / 𝑛𝐴 ∈ ℝ)
10094, 99remulcld 10667 . . 3 (𝜑 → ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴) ∈ ℝ)
101 dchrisumlem2.1 . . . . 5 (𝜑𝑈 ∈ ℝ+)
10232ralrimiva 3149 . . . . 5 (𝜑 → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ)
103 nfcsb1v 3852 . . . . . . 7 𝑛𝑈 / 𝑛𝐴
104103nfel1 2971 . . . . . 6 𝑛𝑈 / 𝑛𝐴 ∈ ℝ
105 csbeq1a 3842 . . . . . . 7 (𝑛 = 𝑈𝐴 = 𝑈 / 𝑛𝐴)
106105eleq1d 2874 . . . . . 6 (𝑛 = 𝑈 → (𝐴 ∈ ℝ ↔ 𝑈 / 𝑛𝐴 ∈ ℝ))
107104, 106rspc 3559 . . . . 5 (𝑈 ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → 𝑈 / 𝑛𝐴 ∈ ℝ))
108101, 102, 107sylc 65 . . . 4 (𝜑𝑈 / 𝑛𝐴 ∈ ℝ)
10994, 108remulcld 10667 . . 3 (𝜑 → ((2 · 𝑅) · 𝑈 / 𝑛𝐴) ∈ ℝ)
11069, 5eleqtrrdi 2901 . . . . . . . . . . . 12 (𝜑𝐽 ∈ ℕ)
111110peano2nnd 11649 . . . . . . . . . . 11 (𝜑 → (𝐽 + 1) ∈ ℕ)
112111nnrpd 12424 . . . . . . . . . 10 (𝜑 → (𝐽 + 1) ∈ ℝ+)
11319, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35dchrisumlema 26086 . . . . . . . . . . 11 (𝜑 → (((𝐽 + 1) ∈ ℝ+(𝐽 + 1) / 𝑛𝐴 ∈ ℝ) ∧ ((𝐽 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐽 + 1) / 𝑛𝐴)))
114113simpld 498 . . . . . . . . . 10 (𝜑 → ((𝐽 + 1) ∈ ℝ+(𝐽 + 1) / 𝑛𝐴 ∈ ℝ))
115112, 114mpd 15 . . . . . . . . 9 (𝜑(𝐽 + 1) / 𝑛𝐴 ∈ ℝ)
116115recnd 10665 . . . . . . . 8 (𝜑(𝐽 + 1) / 𝑛𝐴 ∈ ℂ)
117 fzofi 13344 . . . . . . . . . 10 (0..^(𝐽 + 1)) ∈ Fin
118117a1i 11 . . . . . . . . 9 (𝜑 → (0..^(𝐽 + 1)) ∈ Fin)
119 elfzoelz 13040 . . . . . . . . . 10 (𝑛 ∈ (0..^(𝐽 + 1)) → 𝑛 ∈ ℤ)
12022adantr 484 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℤ) → 𝑋𝐷)
121 simpr 488 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℤ) → 𝑛 ∈ ℤ)
12218, 19, 20, 21, 120, 121dchrzrhcl 25843 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℤ) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
123119, 122sylan2 595 . . . . . . . . 9 ((𝜑𝑛 ∈ (0..^(𝐽 + 1))) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
124118, 123fsumcl 15089 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
125116, 124mulcld 10657 . . . . . . 7 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
12699recnd 10665 . . . . . . . 8 (𝜑(𝐼 + 1) / 𝑛𝐴 ∈ ℂ)
127 fzofi 13344 . . . . . . . . . 10 (0..^(𝐼 + 1)) ∈ Fin
128127a1i 11 . . . . . . . . 9 (𝜑 → (0..^(𝐼 + 1)) ∈ Fin)
129 elfzoelz 13040 . . . . . . . . . 10 (𝑛 ∈ (0..^(𝐼 + 1)) → 𝑛 ∈ ℤ)
130129, 122sylan2 595 . . . . . . . . 9 ((𝜑𝑛 ∈ (0..^(𝐼 + 1))) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
131128, 130fsumcl 15089 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
132126, 131mulcld 10657 . . . . . . 7 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
133125, 132subcld 10993 . . . . . 6 (𝜑 → (((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℂ)
134133abscld 14795 . . . . 5 (𝜑 → (abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ∈ ℝ)
13584, 17syl 17 . . . . . . . 8 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ ℕ)
136 peano2nn 11644 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℕ)
137136nnrpd 12424 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℝ+)
138 nfcsb1v 3852 . . . . . . . . . . . . . . 15 𝑛(𝑖 + 1) / 𝑛𝐴
139138nfel1 2971 . . . . . . . . . . . . . 14 𝑛(𝑖 + 1) / 𝑛𝐴 ∈ ℝ
140 csbeq1a 3842 . . . . . . . . . . . . . . 15 (𝑛 = (𝑖 + 1) → 𝐴 = (𝑖 + 1) / 𝑛𝐴)
141140eleq1d 2874 . . . . . . . . . . . . . 14 (𝑛 = (𝑖 + 1) → (𝐴 ∈ ℝ ↔ (𝑖 + 1) / 𝑛𝐴 ∈ ℝ))
142139, 141rspc 3559 . . . . . . . . . . . . 13 ((𝑖 + 1) ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ))
143142impcom 411 . . . . . . . . . . . 12 ((∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ ∧ (𝑖 + 1) ∈ ℝ+) → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ)
144102, 137, 143syl2an 598 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ)
145144, 39resubcld 11064 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → ((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) ∈ ℝ)
146145recnd 10665 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) ∈ ℂ)
147 fzofi 13344 . . . . . . . . . . . 12 (0..^(𝑖 + 1)) ∈ Fin
148147a1i 11 . . . . . . . . . . 11 (𝜑 → (0..^(𝑖 + 1)) ∈ Fin)
149 elfzoelz 13040 . . . . . . . . . . . 12 (𝑛 ∈ (0..^(𝑖 + 1)) → 𝑛 ∈ ℤ)
150149, 122sylan2 595 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (0..^(𝑖 + 1))) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
151148, 150fsumcl 15089 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
152151adantr 484 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
153146, 152mulcld 10657 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ) → (((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
154135, 153syldan 594 . . . . . . 7 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
15581, 154fsumcl 15089 . . . . . 6 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
156155abscld 14795 . . . . 5 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
157134, 156readdcld 10666 . . . 4 (𝜑 → ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))) ∈ ℝ)
15826, 40mulcomd 10658 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (𝑖 / 𝑛𝐴 · (𝑋‘(𝐿𝑖))))
159 nnnn0 11899 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → 𝑖 ∈ ℕ0)
160159adantl 485 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ0)
161 nn0uz 12275 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
162160, 161eleqtrdi 2900 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ (ℤ‘0))
163 elfzelz 12909 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0...𝑖) → 𝑛 ∈ ℤ)
164122adantlr 714 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
165163, 164sylan2 595 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ ℕ) ∧ 𝑛 ∈ (0...𝑖)) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
166162, 165, 61fzosump1 15106 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) = (Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) + (𝑋‘(𝐿𝑖))))
167166oveq1d 7155 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))) = ((Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) + (𝑋‘(𝐿𝑖))) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))))
168 fzofi 13344 . . . . . . . . . . . . . . 15 (0..^𝑖) ∈ Fin
169168a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → (0..^𝑖) ∈ Fin)
170 elfzoelz 13040 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0..^𝑖) → 𝑛 ∈ ℤ)
171170, 164sylan2 595 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ ℕ) ∧ 𝑛 ∈ (0..^𝑖)) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
172169, 171fsumcl 15089 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) ∈ ℂ)
173172, 26pncan2d 10995 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) + (𝑋‘(𝐿𝑖))) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))) = (𝑋‘(𝐿𝑖)))
174167, 173eqtr2d 2834 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (𝑋‘(𝐿𝑖)) = (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))))
175174oveq2d 7156 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → (𝑖 / 𝑛𝐴 · (𝑋‘(𝐿𝑖))) = (𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
176158, 175eqtrd 2833 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
177135, 176syldan 594 . . . . . . . 8 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
178177sumeq2dv 15059 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
179 csbeq1 3831 . . . . . . . . 9 (𝑘 = 𝑖𝑘 / 𝑛𝐴 = 𝑖 / 𝑛𝐴)
180 oveq2 7148 . . . . . . . . . 10 (𝑘 = 𝑖 → (0..^𝑘) = (0..^𝑖))
181180sumeq1d 15057 . . . . . . . . 9 (𝑘 = 𝑖 → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))
182179, 181jca 515 . . . . . . . 8 (𝑘 = 𝑖 → (𝑘 / 𝑛𝐴 = 𝑖 / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))))
183 csbeq1 3831 . . . . . . . . 9 (𝑘 = (𝑖 + 1) → 𝑘 / 𝑛𝐴 = (𝑖 + 1) / 𝑛𝐴)
184 oveq2 7148 . . . . . . . . . 10 (𝑘 = (𝑖 + 1) → (0..^𝑘) = (0..^(𝑖 + 1)))
185184sumeq1d 15057 . . . . . . . . 9 (𝑘 = (𝑖 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))
186183, 185jca 515 . . . . . . . 8 (𝑘 = (𝑖 + 1) → (𝑘 / 𝑛𝐴 = (𝑖 + 1) / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))
187 csbeq1 3831 . . . . . . . . 9 (𝑘 = (𝐼 + 1) → 𝑘 / 𝑛𝐴 = (𝐼 + 1) / 𝑛𝐴)
188 oveq2 7148 . . . . . . . . . 10 (𝑘 = (𝐼 + 1) → (0..^𝑘) = (0..^(𝐼 + 1)))
189188sumeq1d 15057 . . . . . . . . 9 (𝑘 = (𝐼 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))
190187, 189jca 515 . . . . . . . 8 (𝑘 = (𝐼 + 1) → (𝑘 / 𝑛𝐴 = (𝐼 + 1) / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))
191 csbeq1 3831 . . . . . . . . 9 (𝑘 = (𝐽 + 1) → 𝑘 / 𝑛𝐴 = (𝐽 + 1) / 𝑛𝐴)
192 oveq2 7148 . . . . . . . . . 10 (𝑘 = (𝐽 + 1) → (0..^𝑘) = (0..^(𝐽 + 1)))
193192sumeq1d 15057 . . . . . . . . 9 (𝑘 = (𝐽 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))
194191, 193jca 515 . . . . . . . 8 (𝑘 = (𝐽 + 1) → (𝑘 / 𝑛𝐴 = (𝐽 + 1) / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))))
19540ralrimiva 3149 . . . . . . . . 9 (𝜑 → ∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℂ)
196 elfzuz 12905 . . . . . . . . . 10 (𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1)) → 𝑘 ∈ (ℤ‘(𝐼 + 1)))
197 eluznn 12313 . . . . . . . . . 10 (((𝐼 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(𝐼 + 1))) → 𝑘 ∈ ℕ)
1984, 196, 197syl2an 598 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → 𝑘 ∈ ℕ)
199 csbeq1 3831 . . . . . . . . . . 11 (𝑖 = 𝑘𝑖 / 𝑛𝐴 = 𝑘 / 𝑛𝐴)
200199eleq1d 2874 . . . . . . . . . 10 (𝑖 = 𝑘 → (𝑖 / 𝑛𝐴 ∈ ℂ ↔ 𝑘 / 𝑛𝐴 ∈ ℂ))
201200rspccva 3570 . . . . . . . . 9 ((∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) → 𝑘 / 𝑛𝐴 ∈ ℂ)
202195, 198, 201syl2an2r 684 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → 𝑘 / 𝑛𝐴 ∈ ℂ)
203 fzofi 13344 . . . . . . . . . . 11 (0..^𝑘) ∈ Fin
204203a1i 11 . . . . . . . . . 10 (𝜑 → (0..^𝑘) ∈ Fin)
205 elfzoelz 13040 . . . . . . . . . . 11 (𝑛 ∈ (0..^𝑘) → 𝑛 ∈ ℤ)
206205, 122sylan2 595 . . . . . . . . . 10 ((𝜑𝑛 ∈ (0..^𝑘)) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
207204, 206fsumcl 15089 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) ∈ ℂ)
208207adantr 484 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) ∈ ℂ)
209182, 186, 190, 194, 9, 202, 208fsumparts 15160 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))) = ((((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
210178, 209eqtrd 2833 . . . . . 6 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = ((((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
211210fveq2d 6654 . . . . 5 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = (abs‘((((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))))
212133, 155abs2dif2d 14817 . . . . 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 5053 . . . 4 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ≤ ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))))
214115, 99readdcld 10666 . . . . . . 7 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) ∈ ℝ)
215214, 93remulcld 10667 . . . . . 6 (𝜑 → (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) ∈ ℝ)
216179, 183, 187, 191, 9, 202telfsumo 15156 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) = ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴))
217135, 39syldan 594 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 / 𝑛𝐴 ∈ ℝ)
218135, 144syldan 594 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ)
219217, 218resubcld 11064 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ∈ ℝ)
22081, 219fsumrecl 15090 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ∈ ℝ)
221216, 220eqeltrrd 2891 . . . . . . 7 (𝜑 → ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) ∈ ℝ)
222221, 93remulcld 10667 . . . . . 6 (𝜑 → (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅) ∈ ℝ)
223125abscld 14795 . . . . . . . 8 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
224132abscld 14795 . . . . . . . 8 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
225223, 224readdcld 10666 . . . . . . 7 (𝜑 → ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ∈ ℝ)
226125, 132abs2dif2d 14817 . . . . . . 7 (𝜑 → (abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))))
227115, 93remulcld 10667 . . . . . . . . 9 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 · 𝑅) ∈ ℝ)
22899, 93remulcld 10667 . . . . . . . . 9 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 · 𝑅) ∈ ℝ)
229116, 124absmuld 14813 . . . . . . . . . . 11 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) = ((abs‘(𝐽 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))))
230 eluzelre 12249 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (ℤ𝑀) → 𝑖 ∈ ℝ)
231230adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℝ)
232 eluzle 12251 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (ℤ𝑀) → 𝑀𝑖)
233232adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀𝑖)
23431nnred 11647 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℝ)
235234adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ)
236 elicopnf 12830 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℝ → (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀𝑖)))
237235, 236syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀𝑖)))
238231, 233, 237mpbir2and 712 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ (𝑀[,)+∞))
239238ex 416 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑖 ∈ (ℤ𝑀) → 𝑖 ∈ (𝑀[,)+∞)))
240239ssrdv 3921 . . . . . . . . . . . . . . 15 (𝜑 → (ℤ𝑀) ⊆ (𝑀[,)+∞))
24131nnzd 12081 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℤ)
24248peano2zd 12085 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐼 + 1) ∈ ℤ)
243101rpred 12426 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 ∈ ℝ)
2444nnred 11647 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐼 + 1) ∈ ℝ)
245 dchrisumlem2.2 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀𝑈)
246 dchrisumlem2.3 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 ≤ (𝐼 + 1))
247234, 243, 244, 245, 246letrd 10793 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ≤ (𝐼 + 1))
248 eluz2 12244 . . . . . . . . . . . . . . . . 17 ((𝐼 + 1) ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝐼 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝐼 + 1)))
249241, 242, 247, 248syl3anbrc 1340 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐼 + 1) ∈ (ℤ𝑀))
250 uztrn 12256 . . . . . . . . . . . . . . . 16 (((𝐽 + 1) ∈ (ℤ‘(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (ℤ𝑀)) → (𝐽 + 1) ∈ (ℤ𝑀))
2519, 249, 250syl2anc 587 . . . . . . . . . . . . . . 15 (𝜑 → (𝐽 + 1) ∈ (ℤ𝑀))
252240, 251sseldd 3916 . . . . . . . . . . . . . 14 (𝜑 → (𝐽 + 1) ∈ (𝑀[,)+∞))
253113simprd 499 . . . . . . . . . . . . . 14 (𝜑 → ((𝐽 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐽 + 1) / 𝑛𝐴))
254252, 253mpd 15 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ (𝐽 + 1) / 𝑛𝐴)
255115, 254absidd 14781 . . . . . . . . . . . 12 (𝜑 → (abs‘(𝐽 + 1) / 𝑛𝐴) = (𝐽 + 1) / 𝑛𝐴)
256255oveq1d 7155 . . . . . . . . . . 11 (𝜑 → ((abs‘(𝐽 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐽 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))))
257229, 256eqtrd 2833 . . . . . . . . . 10 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐽 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))))
258124abscld 14795 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ∈ ℝ)
259111nnnn0d 11950 . . . . . . . . . . . 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 26087 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐽 + 1) ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
262259, 261mpdan 686 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
263258, 93, 115, 254, 262lemul2ad 11576 . . . . . . . . . 10 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐽 + 1) / 𝑛𝐴 · 𝑅))
264257, 263eqbrtrd 5053 . . . . . . . . 9 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐽 + 1) / 𝑛𝐴 · 𝑅))
265126, 131absmuld 14813 . . . . . . . . . . 11 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) = ((abs‘(𝐼 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))))
266240, 249sseldd 3916 . . . . . . . . . . . . . 14 (𝜑 → (𝐼 + 1) ∈ (𝑀[,)+∞))
26719, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35dchrisumlema 26086 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐼 + 1) ∈ ℝ+(𝐼 + 1) / 𝑛𝐴 ∈ ℝ) ∧ ((𝐼 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐼 + 1) / 𝑛𝐴)))
268267simprd 499 . . . . . . . . . . . . . 14 (𝜑 → ((𝐼 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐼 + 1) / 𝑛𝐴))
269266, 268mpd 15 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ (𝐼 + 1) / 𝑛𝐴)
27099, 269absidd 14781 . . . . . . . . . . . 12 (𝜑 → (abs‘(𝐼 + 1) / 𝑛𝐴) = (𝐼 + 1) / 𝑛𝐴)
271270oveq1d 7155 . . . . . . . . . . 11 (𝜑 → ((abs‘(𝐼 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐼 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))))
272265, 271eqtrd 2833 . . . . . . . . . 10 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐼 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))))
273131abscld 14795 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ∈ ℝ)
2744nnnn0d 11950 . . . . . . . . . . . 12 (𝜑 → (𝐼 + 1) ∈ ℕ0)
27519, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35, 93, 260dchrisumlem1 26087 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐼 + 1) ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
276274, 275mpdan 686 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
277273, 93, 99, 269, 276lemul2ad 11576 . . . . . . . . . 10 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐼 + 1) / 𝑛𝐴 · 𝑅))
278272, 277eqbrtrd 5053 . . . . . . . . 9 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐼 + 1) / 𝑛𝐴 · 𝑅))
279223, 224, 227, 228, 264, 278le2addd 11255 . . . . . . . 8 (𝜑 → ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ (((𝐽 + 1) / 𝑛𝐴 · 𝑅) + ((𝐼 + 1) / 𝑛𝐴 · 𝑅)))
28093recnd 10665 . . . . . . . . 9 (𝜑𝑅 ∈ ℂ)
281116, 126, 280adddird 10662 . . . . . . . 8 (𝜑 → (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) = (((𝐽 + 1) / 𝑛𝐴 · 𝑅) + ((𝐼 + 1) / 𝑛𝐴 · 𝑅)))
282279, 281breqtrrd 5059 . . . . . . 7 (𝜑 → ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅))
283134, 225, 215, 226, 282letrd 10793 . . . . . 6 (𝜑 → (abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅))
284154abscld 14795 . . . . . . . 8 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
28581, 284fsumrecl 15090 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
28681, 154fsumabs 15155 . . . . . . 7 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
28793adantr 484 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑅 ∈ ℝ)
288219, 287remulcld 10667 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) ∈ ℝ)
289135, 146syldan 594 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) ∈ ℂ)
290151adantr 484 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
291289, 290absmuld 14813 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) = ((abs‘((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
292 elfzouz 13044 . . . . . . . . . . . . . . 15 (𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1)) → 𝑖 ∈ (ℤ‘(𝐼 + 1)))
293 uztrn 12256 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (ℤ‘(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (ℤ𝑀)) → 𝑖 ∈ (ℤ𝑀))
294292, 249, 293syl2anr 599 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ (ℤ𝑀))
295 eluznn 12313 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℕ ∧ 𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℕ)
29631, 295sylan 583 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℕ)
297296, 137syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑖 + 1) ∈ ℝ+)
298296nnrpd 12424 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℝ+)
299333expia 1118 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+)) → ((𝑀𝑛𝑛𝑥) → 𝐵𝐴))
300299ralrimivva 3156 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴))
301300adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → ∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴))
302 nfcv 2955 . . . . . . . . . . . . . . . . . 18 𝑛+
303 nfv 1915 . . . . . . . . . . . . . . . . . . 19 𝑛(𝑀𝑖𝑖𝑥)
304 nfcv 2955 . . . . . . . . . . . . . . . . . . . 20 𝑛𝐵
305 nfcv 2955 . . . . . . . . . . . . . . . . . . . 20 𝑛
306304, 305, 59nfbr 5078 . . . . . . . . . . . . . . . . . . 19 𝑛 𝐵𝑖 / 𝑛𝐴
307303, 306nfim 1897 . . . . . . . . . . . . . . . . . 18 𝑛((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)
308302, 307nfralw 3189 . . . . . . . . . . . . . . . . 17 𝑛𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)
309 breq2 5035 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑖 → (𝑀𝑛𝑀𝑖))
310 breq1 5034 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑖 → (𝑛𝑥𝑖𝑥))
311309, 310anbi12d 633 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑖 → ((𝑀𝑛𝑛𝑥) ↔ (𝑀𝑖𝑖𝑥)))
31262breq2d 5043 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑖 → (𝐵𝐴𝐵𝑖 / 𝑛𝐴))
313311, 312imbi12d 348 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑖 → (((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)))
314313ralbidv 3162 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 → (∀𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)))
315308, 314rspc 3559 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℝ+ → (∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) → ∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)))
316298, 301, 315sylc 65 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → ∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴))
317231lep1d 11567 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ≤ (𝑖 + 1))
318233, 317jca 515 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑀𝑖𝑖 ≤ (𝑖 + 1)))
319 breq2 5035 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑖 + 1) → (𝑖𝑥𝑖 ≤ (𝑖 + 1)))
320319anbi2d 631 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑖 + 1) → ((𝑀𝑖𝑖𝑥) ↔ (𝑀𝑖𝑖 ≤ (𝑖 + 1))))
321 eqvisset 3458 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑖 + 1) → (𝑖 + 1) ∈ V)
322 eqtr3 2820 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) → 𝑥 = 𝑛)
32330equcoms 2027 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑛𝐴 = 𝐵)
324322, 323syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) → 𝐴 = 𝐵)
325321, 324csbied 3864 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑖 + 1) → (𝑖 + 1) / 𝑛𝐴 = 𝐵)
326325eqcomd 2804 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑖 + 1) → 𝐵 = (𝑖 + 1) / 𝑛𝐴)
327326breq1d 5041 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑖 + 1) → (𝐵𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴))
328320, 327imbi12d 348 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑖 + 1) → (((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴) ↔ ((𝑀𝑖𝑖 ≤ (𝑖 + 1)) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)))
329328rspcv 3566 . . . . . . . . . . . . . . 15 ((𝑖 + 1) ∈ ℝ+ → (∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴) → ((𝑀𝑖𝑖 ≤ (𝑖 + 1)) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)))
330297, 316, 318, 329syl3c 66 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)
331294, 330syldan 594 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)
332218, 217, 331abssuble0d 14791 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)) = (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴))
333332oveq1d 7155 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((abs‘((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) = ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
334291, 333eqtrd 2833 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) = ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
335290abscld 14795 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℝ)
336217, 218subge0d 11226 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (0 ≤ (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ↔ (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴))
337331, 336mpbird 260 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 0 ≤ (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴))
338135peano2nnd 11649 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) ∈ ℕ)
339338nnnn0d 11950 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) ∈ ℕ0)
34019, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35, 93, 260dchrisumlem1 26087 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 + 1) ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
341339, 340syldan 594 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
342335, 287, 219, 337, 341lemul2ad 11576 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
343334, 342eqbrtrd 5053 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
34481, 284, 288, 343fsumle 15153 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
345219recnd 10665 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ∈ ℂ)
34681, 280, 345fsummulc1 15139 . . . . . . . . 9 (𝜑 → (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
347216oveq1d 7155 . . . . . . . . 9 (𝜑 → (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) = (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
348346, 347eqtr3d 2835 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) = (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
349344, 348breqtrd 5057 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
350156, 285, 222, 286, 349letrd 10793 . . . . . 6 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
351134, 156, 215, 222, 283, 350le2addd 11255 . . . . 5 (𝜑 → ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))) ≤ ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) + (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅)))
3521262timesd 11875 . . . . . . . 8 (𝜑 → (2 · (𝐼 + 1) / 𝑛𝐴) = ((𝐼 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴))
353126, 116, 126ppncand 11033 . . . . . . . 8 (𝜑 → (((𝐼 + 1) / 𝑛𝐴 + (𝐽 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) = ((𝐼 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴))
354126, 116addcomd 10838 . . . . . . . . 9 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 + (𝐽 + 1) / 𝑛𝐴) = ((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴))
355354oveq1d 7155 . . . . . . . 8 (𝜑 → (((𝐼 + 1) / 𝑛𝐴 + (𝐽 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) = (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)))
356352, 353, 3553eqtr2d 2839 . . . . . . 7 (𝜑 → (2 · (𝐼 + 1) / 𝑛𝐴) = (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)))
357356oveq1d 7155 . . . . . 6 (𝜑 → ((2 · (𝐼 + 1) / 𝑛𝐴) · 𝑅) = ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) · 𝑅))
358 2cnd 11710 . . . . . . 7 (𝜑 → 2 ∈ ℂ)
359358, 126, 280mul32d 10846 . . . . . 6 (𝜑 → ((2 · (𝐼 + 1) / 𝑛𝐴) · 𝑅) = ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴))
360214recnd 10665 . . . . . . 7 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) ∈ ℂ)
361221recnd 10665 . . . . . . 7 (𝜑 → ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) ∈ ℂ)
362360, 361, 280adddird 10662 . . . . . 6 (𝜑 → ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) · 𝑅) = ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) + (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅)))
363357, 359, 3623eqtr3d 2841 . . . . 5 (𝜑 → ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴) = ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) + (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅)))
364351, 363breqtrrd 5059 . . . 4 (𝜑 → ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))) ≤ ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴))
36590, 157, 100, 213, 364letrd 10793 . . 3 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ≤ ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴))
366 2nn0 11909 . . . . . 6 2 ∈ ℕ0
367 nn0ge0 11917 . . . . . 6 (2 ∈ ℕ0 → 0 ≤ 2)
368366, 367mp1i 13 . . . . 5 (𝜑 → 0 ≤ 2)
369 0red 10640 . . . . . 6 (𝜑 → 0 ∈ ℝ)
370124absge0d 14803 . . . . . 6 (𝜑 → 0 ≤ (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))))
371369, 258, 93, 370, 262letrd 10793 . . . . 5 (𝜑 → 0 ≤ 𝑅)
37292, 93, 368, 371mulge0d 11213 . . . 4 (𝜑 → 0 ≤ (2 · 𝑅))
3734nnrpd 12424 . . . . 5 (𝜑 → (𝐼 + 1) ∈ ℝ+)
374 nfv 1915 . . . . . . . . 9 𝑛(𝑀𝑈𝑈𝑥)
375304, 305, 103nfbr 5078 . . . . . . . . 9 𝑛 𝐵𝑈 / 𝑛𝐴
376374, 375nfim 1897 . . . . . . . 8 𝑛((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)
377302, 376nfralw 3189 . . . . . . 7 𝑛𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)
378 breq2 5035 . . . . . . . . . 10 (𝑛 = 𝑈 → (𝑀𝑛𝑀𝑈))
379 breq1 5034 . . . . . . . . . 10 (𝑛 = 𝑈 → (𝑛𝑥𝑈𝑥))
380378, 379anbi12d 633 . . . . . . . . 9 (𝑛 = 𝑈 → ((𝑀𝑛𝑛𝑥) ↔ (𝑀𝑈𝑈𝑥)))
381105breq2d 5043 . . . . . . . . 9 (𝑛 = 𝑈 → (𝐵𝐴𝐵𝑈 / 𝑛𝐴))
382380, 381imbi12d 348 . . . . . . . 8 (𝑛 = 𝑈 → (((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)))
383382ralbidv 3162 . . . . . . 7 (𝑛 = 𝑈 → (∀𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)))
384377, 383rspc 3559 . . . . . 6 (𝑈 ∈ ℝ+ → (∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) → ∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)))
385101, 300, 384sylc 65 . . . . 5 (𝜑 → ∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴))
386245, 246jca 515 . . . . 5 (𝜑 → (𝑀𝑈𝑈 ≤ (𝐼 + 1)))
387 breq2 5035 . . . . . . . 8 (𝑥 = (𝐼 + 1) → (𝑈𝑥𝑈 ≤ (𝐼 + 1)))
388387anbi2d 631 . . . . . . 7 (𝑥 = (𝐼 + 1) → ((𝑀𝑈𝑈𝑥) ↔ (𝑀𝑈𝑈 ≤ (𝐼 + 1))))
389 eqvisset 3458 . . . . . . . . . 10 (𝑥 = (𝐼 + 1) → (𝐼 + 1) ∈ V)
390 eqtr3 2820 . . . . . . . . . . 11 ((𝑥 = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) → 𝑥 = 𝑛)
391390, 323syl 17 . . . . . . . . . 10 ((𝑥 = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) → 𝐴 = 𝐵)
392389, 391csbied 3864 . . . . . . . . 9 (𝑥 = (𝐼 + 1) → (𝐼 + 1) / 𝑛𝐴 = 𝐵)
393392eqcomd 2804 . . . . . . . 8 (𝑥 = (𝐼 + 1) → 𝐵 = (𝐼 + 1) / 𝑛𝐴)
394393breq1d 5041 . . . . . . 7 (𝑥 = (𝐼 + 1) → (𝐵𝑈 / 𝑛𝐴(𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴))
395388, 394imbi12d 348 . . . . . 6 (𝑥 = (𝐼 + 1) → (((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴) ↔ ((𝑀𝑈𝑈 ≤ (𝐼 + 1)) → (𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴)))
396395rspcv 3566 . . . . 5 ((𝐼 + 1) ∈ ℝ+ → (∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴) → ((𝑀𝑈𝑈 ≤ (𝐼 + 1)) → (𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴)))
397373, 385, 386, 396syl3c 66 . . . 4 (𝜑(𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴)
39899, 108, 94, 372, 397lemul2ad 11576 . . 3 (𝜑 → ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴) ≤ ((2 · 𝑅) · 𝑈 / 𝑛𝐴))
39990, 100, 109, 365, 398letrd 10793 . 2 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ≤ ((2 · 𝑅) · 𝑈 / 𝑛𝐴))
40089, 399eqbrtrd 5053 1 (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) ≤ ((2 · 𝑅) · 𝑈 / 𝑛𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  Vcvv 3441  ⦋csb 3828   ∪ cun 3879   ∩ cin 3880  ∅c0 4243   class class class wbr 5031   ↦ cmpt 5111  ‘cfv 6327  (class class class)co 7140  Fincfn 8499  ℂcc 10531  ℝcr 10532  0cc0 10533  1c1 10534   + caddc 10536   · cmul 10538  +∞cpnf 10668   ≤ cle 10672   − cmin 10866  ℕcn 11632  2c2 11687  ℕ0cn0 11892  ℤcz 11976  ℤ≥cuz 12238  ℝ+crp 12384  [,)cico 12735  ...cfz 12892  ..^cfzo 13035  seqcseq 13371  abscabs 14592   ⇝𝑟 crli 14841  Σcsu 15041  Basecbs 16482  0gc0g 16712  ℤRHomczrh 20202  ℤ/nℤczn 20205  DChrcdchr 25830 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7448  ax-inf2 9095  ax-cnex 10589  ax-resscn 10590  ax-1cn 10591  ax-icn 10592  ax-addcl 10593  ax-addrcl 10594  ax-mulcl 10595  ax-mulrcl 10596  ax-mulcom 10597  ax-addass 10598  ax-mulass 10599  ax-distr 10600  ax-i2m1 10601  ax-1ne0 10602  ax-1rid 10603  ax-rnegex 10604  ax-rrecex 10605  ax-cnre 10606  ax-pre-lttri 10607  ax-pre-lttrn 10608  ax-pre-ltadd 10609  ax-pre-mulgt0 10610  ax-pre-sup 10611  ax-addf 10612  ax-mulf 10613 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-se 5480  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6286  df-fun 6329  df-fn 6330  df-f 6331  df-f1 6332  df-fo 6333  df-f1o 6334  df-fv 6335  df-isom 6336  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-of 7395  df-om 7568  df-1st 7678  df-2nd 7679  df-tpos 7882  df-wrecs 7937  df-recs 7998  df-rdg 8036  df-1o 8092  df-oadd 8096  df-er 8279  df-ec 8281  df-qs 8285  df-map 8398  df-pm 8399  df-en 8500  df-dom 8501  df-sdom 8502  df-fin 8503  df-sup 8897  df-inf 8898  df-oi 8965  df-card 9359  df-pnf 10673  df-mnf 10674  df-xr 10675  df-ltxr 10676  df-le 10677  df-sub 10868  df-neg 10869  df-div 11294  df-nn 11633  df-2 11695  df-3 11696  df-4 11697  df-5 11698  df-6 11699  df-7 11700  df-8 11701  df-9 11702  df-n0 11893  df-xnn0 11963  df-z 11977  df-dec 12094  df-uz 12239  df-rp 12385  df-ico 12739  df-fz 12893  df-fzo 13036  df-fl 13164  df-mod 13240  df-seq 13372  df-exp 13433  df-hash 13694  df-cj 14457  df-re 14458  df-im 14459  df-sqrt 14593  df-abs 14594  df-clim 14844  df-rlim 14845  df-sum 15042  df-dvds 15607  df-gcd 15841  df-phi 16100  df-struct 16484  df-ndx 16485  df-slot 16486  df-base 16488  df-sets 16489  df-ress 16490  df-plusg 16577  df-mulr 16578  df-starv 16579  df-sca 16580  df-vsca 16581  df-ip 16582  df-tset 16583  df-ple 16584  df-ds 16586  df-unif 16587  df-0g 16714  df-imas 16780  df-qus 16781  df-mgm 17851  df-sgrp 17900  df-mnd 17911  df-mhm 17955  df-grp 18105  df-minusg 18106  df-sbg 18107  df-mulg 18225  df-subg 18276  df-nsg 18277  df-eqg 18278  df-ghm 18356  df-cmn 18908  df-abl 18909  df-mgp 19241  df-ur 19253  df-ring 19300  df-cring 19301  df-oppr 19377  df-dvdsr 19395  df-unit 19396  df-invr 19426  df-rnghom 19471  df-subrg 19534  df-lmod 19637  df-lss 19705  df-lsp 19745  df-sra 19945  df-rgmod 19946  df-lidl 19947  df-rsp 19948  df-2idl 20006  df-cnfld 20100  df-zring 20172  df-zrh 20206  df-zn 20209  df-dchr 25831 This theorem is referenced by:  dchrisumlem3  26089
 Copyright terms: Public domain W3C validator