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

Theorem dchrisumlem2 25748
Description: Lemma for dchrisum 25750. 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 12921 . . . . . . . . 9 ((1..^(𝐼 + 1)) ∩ ((𝐼 + 1)..^(𝐽 + 1))) = ∅
21a1i 11 . . . . . . . 8 (𝜑 → ((1..^(𝐼 + 1)) ∩ ((𝐼 + 1)..^(𝐽 + 1))) = ∅)
3 dchrisumlem2.4 . . . . . . . . . . . 12 (𝜑𝐼 ∈ ℕ)
43peano2nnd 11503 . . . . . . . . . . 11 (𝜑 → (𝐼 + 1) ∈ ℕ)
5 nnuz 12130 . . . . . . . . . . 11 ℕ = (ℤ‘1)
64, 5syl6eleq 2893 . . . . . . . . . 10 (𝜑 → (𝐼 + 1) ∈ (ℤ‘1))
7 dchrisumlem2.5 . . . . . . . . . . 11 (𝜑𝐽 ∈ (ℤ𝐼))
8 eluzp1p1 12119 . . . . . . . . . . 11 (𝐽 ∈ (ℤ𝐼) → (𝐽 + 1) ∈ (ℤ‘(𝐼 + 1)))
97, 8syl 17 . . . . . . . . . 10 (𝜑 → (𝐽 + 1) ∈ (ℤ‘(𝐼 + 1)))
10 elfzuzb 12752 . . . . . . . . . 10 ((𝐼 + 1) ∈ (1...(𝐽 + 1)) ↔ ((𝐼 + 1) ∈ (ℤ‘1) ∧ (𝐽 + 1) ∈ (ℤ‘(𝐼 + 1))))
116, 9, 10sylanbrc 583 . . . . . . . . 9 (𝜑 → (𝐼 + 1) ∈ (1...(𝐽 + 1)))
12 fzosplit 12920 . . . . . . . . 9 ((𝐼 + 1) ∈ (1...(𝐽 + 1)) → (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1))))
1311, 12syl 17 . . . . . . . 8 (𝜑 → (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1))))
14 fzofi 13192 . . . . . . . . 9 (1..^(𝐽 + 1)) ∈ Fin
1514a1i 11 . . . . . . . 8 (𝜑 → (1..^(𝐽 + 1)) ∈ Fin)
16 elfzouz 12892 . . . . . . . . . 10 (𝑖 ∈ (1..^(𝐽 + 1)) → 𝑖 ∈ (ℤ‘1))
1716, 5syl6eleqr 2894 . . . . . . . . 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 11853 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → 𝑖 ∈ ℤ)
2524adantl 482 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℤ)
2618, 19, 20, 21, 23, 25dchrzrhcl 25503 . . . . . . . . . 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 25746 . . . . . . . . . . . . 13 (𝜑 → ((𝑖 ∈ ℝ+𝑖 / 𝑛𝐴 ∈ ℝ) ∧ (𝑖 ∈ (𝑀[,)+∞) → 0 ≤ 𝑖 / 𝑛𝐴)))
3736simpld 495 . . . . . . . . . . . 12 (𝜑 → (𝑖 ∈ ℝ+𝑖 / 𝑛𝐴 ∈ ℝ))
38 nnrp 12250 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → 𝑖 ∈ ℝ+)
3937, 38impel 506 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 𝑖 / 𝑛𝐴 ∈ ℝ)
4039recnd 10515 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → 𝑖 / 𝑛𝐴 ∈ ℂ)
4126, 40mulcld 10507 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
4217, 41sylan2 592 . . . . . . . 8 ((𝜑𝑖 ∈ (1..^(𝐽 + 1))) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
432, 13, 15, 42fsumsplit 14930 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (1..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
44 eluzelz 12103 . . . . . . . . 9 (𝐽 ∈ (ℤ𝐼) → 𝐽 ∈ ℤ)
45 fzval3 12956 . . . . . . . . 9 (𝐽 ∈ ℤ → (1...𝐽) = (1..^(𝐽 + 1)))
467, 44, 453syl 18 . . . . . . . 8 (𝜑 → (1...𝐽) = (1..^(𝐽 + 1)))
4746sumeq1d 14891 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = Σ𝑖 ∈ (1..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
483nnzd 11935 . . . . . . . . . 10 (𝜑𝐼 ∈ ℤ)
49 fzval3 12956 . . . . . . . . . 10 (𝐼 ∈ ℤ → (1...𝐼) = (1..^(𝐼 + 1)))
5048, 49syl 17 . . . . . . . . 9 (𝜑 → (1...𝐼) = (1..^(𝐼 + 1)))
5150sumeq1d 14891 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
5251oveq1d 7031 . . . . . . 7 (𝜑 → (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
5343, 47, 523eqtr4d 2841 . . . . . 6 (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
54 elfznn 12786 . . . . . . . 8 (𝑖 ∈ (1...𝐽) → 𝑖 ∈ ℕ)
55 simpr 485 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
56 nfcv 2949 . . . . . . . . . 10 𝑛𝑖
57 nfcv 2949 . . . . . . . . . . 11 𝑛(𝑋‘(𝐿𝑖))
58 nfcv 2949 . . . . . . . . . . 11 𝑛 ·
59 nfcsb1v 3833 . . . . . . . . . . 11 𝑛𝑖 / 𝑛𝐴
6057, 58, 59nfov 7046 . . . . . . . . . 10 𝑛((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)
61 2fveq3 6543 . . . . . . . . . . 11 (𝑛 = 𝑖 → (𝑋‘(𝐿𝑛)) = (𝑋‘(𝐿𝑖)))
62 csbeq1a 3824 . . . . . . . . . . 11 (𝑛 = 𝑖𝐴 = 𝑖 / 𝑛𝐴)
6361, 62oveq12d 7034 . . . . . . . . . 10 (𝑛 = 𝑖 → ((𝑋‘(𝐿𝑛)) · 𝐴) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
6456, 60, 63, 35fvmptf 6655 . . . . . . . . 9 ((𝑖 ∈ ℕ ∧ ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
6555, 41, 64syl2anc 584 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
6654, 65sylan2 592 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝐽)) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
673, 5syl6eleq 2893 . . . . . . . 8 (𝜑𝐼 ∈ (ℤ‘1))
68 uztrn 12110 . . . . . . . 8 ((𝐽 ∈ (ℤ𝐼) ∧ 𝐼 ∈ (ℤ‘1)) → 𝐽 ∈ (ℤ‘1))
697, 67, 68syl2anc 584 . . . . . . 7 (𝜑𝐽 ∈ (ℤ‘1))
7054, 41sylan2 592 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝐽)) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
7166, 69, 70fsumser 14920 . . . . . 6 (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (seq1( + , 𝐹)‘𝐽))
7253, 71eqtr3d 2833 . . . . 5 (𝜑 → (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = (seq1( + , 𝐹)‘𝐽))
73 elfznn 12786 . . . . . . 7 (𝑖 ∈ (1...𝐼) → 𝑖 ∈ ℕ)
7473, 65sylan2 592 . . . . . 6 ((𝜑𝑖 ∈ (1...𝐼)) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
7573, 41sylan2 592 . . . . . 6 ((𝜑𝑖 ∈ (1...𝐼)) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
7674, 67, 75fsumser 14920 . . . . 5 (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (seq1( + , 𝐹)‘𝐼))
7772, 76oveq12d 7034 . . . 4 (𝜑 → ((Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) − Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = ((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼)))
78 fzfid 13191 . . . . . 6 (𝜑 → (1...𝐼) ∈ Fin)
7978, 75fsumcl 14923 . . . . 5 (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
80 fzofi 13192 . . . . . . 7 ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin
8180a1i 11 . . . . . 6 (𝜑 → ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin)
82 ssun2 4070 . . . . . . . . 9 ((𝐼 + 1)..^(𝐽 + 1)) ⊆ ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1)))
8382, 13sseqtrrid 3941 . . . . . . . 8 (𝜑 → ((𝐼 + 1)..^(𝐽 + 1)) ⊆ (1..^(𝐽 + 1)))
8483sselda 3889 . . . . . . 7 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ (1..^(𝐽 + 1)))
8584, 42syldan 591 . . . . . 6 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
8681, 85fsumcl 14923 . . . . 5 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
8779, 86pncan2d 10847 . . . 4 (𝜑 → ((Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) − Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
8877, 87eqtr3d 2833 . . 3 (𝜑 → ((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
8988fveq2d 6542 . 2 (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) = (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)))
9086abscld 14630 . . 3 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ∈ ℝ)
91 2re 11559 . . . . . 6 2 ∈ ℝ
9291a1i 11 . . . . 5 (𝜑 → 2 ∈ ℝ)
93 dchrisum.9 . . . . 5 (𝜑𝑅 ∈ ℝ)
9492, 93remulcld 10517 . . . 4 (𝜑 → (2 · 𝑅) ∈ ℝ)
9539ralrimiva 3149 . . . . 5 (𝜑 → ∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℝ)
96 csbeq1 3814 . . . . . . 7 (𝑖 = (𝐼 + 1) → 𝑖 / 𝑛𝐴 = (𝐼 + 1) / 𝑛𝐴)
9796eleq1d 2867 . . . . . 6 (𝑖 = (𝐼 + 1) → (𝑖 / 𝑛𝐴 ∈ ℝ ↔ (𝐼 + 1) / 𝑛𝐴 ∈ ℝ))
9897rspcv 3555 . . . . 5 ((𝐼 + 1) ∈ ℕ → (∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℝ → (𝐼 + 1) / 𝑛𝐴 ∈ ℝ))
994, 95, 98sylc 65 . . . 4 (𝜑(𝐼 + 1) / 𝑛𝐴 ∈ ℝ)
10094, 99remulcld 10517 . . 3 (𝜑 → ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴) ∈ ℝ)
101 dchrisumlem2.1 . . . . 5 (𝜑𝑈 ∈ ℝ+)
10232ralrimiva 3149 . . . . 5 (𝜑 → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ)
103 nfcsb1v 3833 . . . . . . 7 𝑛𝑈 / 𝑛𝐴
104103nfel1 2963 . . . . . 6 𝑛𝑈 / 𝑛𝐴 ∈ ℝ
105 csbeq1a 3824 . . . . . . 7 (𝑛 = 𝑈𝐴 = 𝑈 / 𝑛𝐴)
106105eleq1d 2867 . . . . . 6 (𝑛 = 𝑈 → (𝐴 ∈ ℝ ↔ 𝑈 / 𝑛𝐴 ∈ ℝ))
107104, 106rspc 3553 . . . . 5 (𝑈 ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → 𝑈 / 𝑛𝐴 ∈ ℝ))
108101, 102, 107sylc 65 . . . 4 (𝜑𝑈 / 𝑛𝐴 ∈ ℝ)
10994, 108remulcld 10517 . . 3 (𝜑 → ((2 · 𝑅) · 𝑈 / 𝑛𝐴) ∈ ℝ)
11069, 5syl6eleqr 2894 . . . . . . . . . . . 12 (𝜑𝐽 ∈ ℕ)
111110peano2nnd 11503 . . . . . . . . . . 11 (𝜑 → (𝐽 + 1) ∈ ℕ)
112111nnrpd 12279 . . . . . . . . . 10 (𝜑 → (𝐽 + 1) ∈ ℝ+)
11319, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35dchrisumlema 25746 . . . . . . . . . . 11 (𝜑 → (((𝐽 + 1) ∈ ℝ+(𝐽 + 1) / 𝑛𝐴 ∈ ℝ) ∧ ((𝐽 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐽 + 1) / 𝑛𝐴)))
114113simpld 495 . . . . . . . . . 10 (𝜑 → ((𝐽 + 1) ∈ ℝ+(𝐽 + 1) / 𝑛𝐴 ∈ ℝ))
115112, 114mpd 15 . . . . . . . . 9 (𝜑(𝐽 + 1) / 𝑛𝐴 ∈ ℝ)
116115recnd 10515 . . . . . . . 8 (𝜑(𝐽 + 1) / 𝑛𝐴 ∈ ℂ)
117 fzofi 13192 . . . . . . . . . 10 (0..^(𝐽 + 1)) ∈ Fin
118117a1i 11 . . . . . . . . 9 (𝜑 → (0..^(𝐽 + 1)) ∈ Fin)
119 elfzoelz 12888 . . . . . . . . . 10 (𝑛 ∈ (0..^(𝐽 + 1)) → 𝑛 ∈ ℤ)
12022adantr 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℤ) → 𝑋𝐷)
121 simpr 485 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℤ) → 𝑛 ∈ ℤ)
12218, 19, 20, 21, 120, 121dchrzrhcl 25503 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℤ) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
123119, 122sylan2 592 . . . . . . . . 9 ((𝜑𝑛 ∈ (0..^(𝐽 + 1))) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
124118, 123fsumcl 14923 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
125116, 124mulcld 10507 . . . . . . 7 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
12699recnd 10515 . . . . . . . 8 (𝜑(𝐼 + 1) / 𝑛𝐴 ∈ ℂ)
127 fzofi 13192 . . . . . . . . . 10 (0..^(𝐼 + 1)) ∈ Fin
128127a1i 11 . . . . . . . . 9 (𝜑 → (0..^(𝐼 + 1)) ∈ Fin)
129 elfzoelz 12888 . . . . . . . . . 10 (𝑛 ∈ (0..^(𝐼 + 1)) → 𝑛 ∈ ℤ)
130129, 122sylan2 592 . . . . . . . . 9 ((𝜑𝑛 ∈ (0..^(𝐼 + 1))) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
131128, 130fsumcl 14923 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
132126, 131mulcld 10507 . . . . . . 7 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
133125, 132subcld 10845 . . . . . 6 (𝜑 → (((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℂ)
134133abscld 14630 . . . . 5 (𝜑 → (abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ∈ ℝ)
13584, 17syl 17 . . . . . . . 8 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ ℕ)
136 peano2nn 11498 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℕ)
137136nnrpd 12279 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℝ+)
138 nfcsb1v 3833 . . . . . . . . . . . . . . 15 𝑛(𝑖 + 1) / 𝑛𝐴
139138nfel1 2963 . . . . . . . . . . . . . 14 𝑛(𝑖 + 1) / 𝑛𝐴 ∈ ℝ
140 csbeq1a 3824 . . . . . . . . . . . . . . 15 (𝑛 = (𝑖 + 1) → 𝐴 = (𝑖 + 1) / 𝑛𝐴)
141140eleq1d 2867 . . . . . . . . . . . . . 14 (𝑛 = (𝑖 + 1) → (𝐴 ∈ ℝ ↔ (𝑖 + 1) / 𝑛𝐴 ∈ ℝ))
142139, 141rspc 3553 . . . . . . . . . . . . 13 ((𝑖 + 1) ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ))
143142impcom 408 . . . . . . . . . . . 12 ((∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ ∧ (𝑖 + 1) ∈ ℝ+) → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ)
144102, 137, 143syl2an 595 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ)
145144, 39resubcld 10916 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → ((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) ∈ ℝ)
146145recnd 10515 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) ∈ ℂ)
147 fzofi 13192 . . . . . . . . . . . 12 (0..^(𝑖 + 1)) ∈ Fin
148147a1i 11 . . . . . . . . . . 11 (𝜑 → (0..^(𝑖 + 1)) ∈ Fin)
149 elfzoelz 12888 . . . . . . . . . . . 12 (𝑛 ∈ (0..^(𝑖 + 1)) → 𝑛 ∈ ℤ)
150149, 122sylan2 592 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (0..^(𝑖 + 1))) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
151148, 150fsumcl 14923 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
152151adantr 481 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
153146, 152mulcld 10507 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ) → (((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
154135, 153syldan 591 . . . . . . 7 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
15581, 154fsumcl 14923 . . . . . 6 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℂ)
156155abscld 14630 . . . . 5 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
157134, 156readdcld 10516 . . . 4 (𝜑 → ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))) ∈ ℝ)
15826, 40mulcomd 10508 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (𝑖 / 𝑛𝐴 · (𝑋‘(𝐿𝑖))))
159 nnnn0 11752 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → 𝑖 ∈ ℕ0)
160159adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ0)
161 nn0uz 12129 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
162160, 161syl6eleq 2893 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ (ℤ‘0))
163 elfzelz 12758 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0...𝑖) → 𝑛 ∈ ℤ)
164122adantlr 711 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
165163, 164sylan2 592 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ ℕ) ∧ 𝑛 ∈ (0...𝑖)) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
166162, 165, 61fzosump1 14940 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) = (Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) + (𝑋‘(𝐿𝑖))))
167166oveq1d 7031 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))) = ((Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) + (𝑋‘(𝐿𝑖))) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))))
168 fzofi 13192 . . . . . . . . . . . . . . 15 (0..^𝑖) ∈ Fin
169168a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → (0..^𝑖) ∈ Fin)
170 elfzoelz 12888 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0..^𝑖) → 𝑛 ∈ ℤ)
171170, 164sylan2 592 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ ℕ) ∧ 𝑛 ∈ (0..^𝑖)) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
172169, 171fsumcl 14923 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) ∈ ℂ)
173172, 26pncan2d 10847 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)) + (𝑋‘(𝐿𝑖))) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))) = (𝑋‘(𝐿𝑖)))
174167, 173eqtr2d 2832 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (𝑋‘(𝐿𝑖)) = (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))))
175174oveq2d 7032 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → (𝑖 / 𝑛𝐴 · (𝑋‘(𝐿𝑖))) = (𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
176158, 175eqtrd 2831 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
177135, 176syldan 591 . . . . . . . 8 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = (𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
178177sumeq2dv 14893 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))))
179 csbeq1 3814 . . . . . . . . 9 (𝑘 = 𝑖𝑘 / 𝑛𝐴 = 𝑖 / 𝑛𝐴)
180 oveq2 7024 . . . . . . . . . 10 (𝑘 = 𝑖 → (0..^𝑘) = (0..^𝑖))
181180sumeq1d 14891 . . . . . . . . 9 (𝑘 = 𝑖 → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))
182179, 181jca 512 . . . . . . . 8 (𝑘 = 𝑖 → (𝑘 / 𝑛𝐴 = 𝑖 / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛))))
183 csbeq1 3814 . . . . . . . . 9 (𝑘 = (𝑖 + 1) → 𝑘 / 𝑛𝐴 = (𝑖 + 1) / 𝑛𝐴)
184 oveq2 7024 . . . . . . . . . 10 (𝑘 = (𝑖 + 1) → (0..^𝑘) = (0..^(𝑖 + 1)))
185184sumeq1d 14891 . . . . . . . . 9 (𝑘 = (𝑖 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))
186183, 185jca 512 . . . . . . . 8 (𝑘 = (𝑖 + 1) → (𝑘 / 𝑛𝐴 = (𝑖 + 1) / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))
187 csbeq1 3814 . . . . . . . . 9 (𝑘 = (𝐼 + 1) → 𝑘 / 𝑛𝐴 = (𝐼 + 1) / 𝑛𝐴)
188 oveq2 7024 . . . . . . . . . 10 (𝑘 = (𝐼 + 1) → (0..^𝑘) = (0..^(𝐼 + 1)))
189188sumeq1d 14891 . . . . . . . . 9 (𝑘 = (𝐼 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))
190187, 189jca 512 . . . . . . . 8 (𝑘 = (𝐼 + 1) → (𝑘 / 𝑛𝐴 = (𝐼 + 1) / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))
191 csbeq1 3814 . . . . . . . . 9 (𝑘 = (𝐽 + 1) → 𝑘 / 𝑛𝐴 = (𝐽 + 1) / 𝑛𝐴)
192 oveq2 7024 . . . . . . . . . 10 (𝑘 = (𝐽 + 1) → (0..^𝑘) = (0..^(𝐽 + 1)))
193192sumeq1d 14891 . . . . . . . . 9 (𝑘 = (𝐽 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))
194191, 193jca 512 . . . . . . . 8 (𝑘 = (𝐽 + 1) → (𝑘 / 𝑛𝐴 = (𝐽 + 1) / 𝑛𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))))
19540ralrimiva 3149 . . . . . . . . 9 (𝜑 → ∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℂ)
196 elfzuz 12754 . . . . . . . . . 10 (𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1)) → 𝑘 ∈ (ℤ‘(𝐼 + 1)))
197 eluznn 12167 . . . . . . . . . 10 (((𝐼 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(𝐼 + 1))) → 𝑘 ∈ ℕ)
1984, 196, 197syl2an 595 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → 𝑘 ∈ ℕ)
199 csbeq1 3814 . . . . . . . . . . 11 (𝑖 = 𝑘𝑖 / 𝑛𝐴 = 𝑘 / 𝑛𝐴)
200199eleq1d 2867 . . . . . . . . . 10 (𝑖 = 𝑘 → (𝑖 / 𝑛𝐴 ∈ ℂ ↔ 𝑘 / 𝑛𝐴 ∈ ℂ))
201200rspccva 3558 . . . . . . . . 9 ((∀𝑖 ∈ ℕ 𝑖 / 𝑛𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) → 𝑘 / 𝑛𝐴 ∈ ℂ)
202195, 198, 201syl2an2r 681 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → 𝑘 / 𝑛𝐴 ∈ ℂ)
203 fzofi 13192 . . . . . . . . . . 11 (0..^𝑘) ∈ Fin
204203a1i 11 . . . . . . . . . 10 (𝜑 → (0..^𝑘) ∈ Fin)
205 elfzoelz 12888 . . . . . . . . . . 11 (𝑛 ∈ (0..^𝑘) → 𝑛 ∈ ℤ)
206205, 122sylan2 592 . . . . . . . . . 10 ((𝜑𝑛 ∈ (0..^𝑘)) → (𝑋‘(𝐿𝑛)) ∈ ℂ)
207204, 206fsumcl 14923 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) ∈ ℂ)
208207adantr 481 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿𝑛)) ∈ ℂ)
209182, 186, 190, 194, 9, 202, 208fsumparts 14994 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿𝑛)))) = ((((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
210178, 209eqtrd 2831 . . . . . 6 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) = ((((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
211210fveq2d 6542 . . . . 5 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) = (abs‘((((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))))
212133, 155abs2dif2d 14652 . . . . 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 4984 . . . 4 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ≤ ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))))
214115, 99readdcld 10516 . . . . . . 7 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) ∈ ℝ)
215214, 93remulcld 10517 . . . . . 6 (𝜑 → (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) ∈ ℝ)
216179, 183, 187, 191, 9, 202telfsumo 14990 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) = ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴))
217135, 39syldan 591 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 / 𝑛𝐴 ∈ ℝ)
218135, 144syldan 591 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) / 𝑛𝐴 ∈ ℝ)
219217, 218resubcld 10916 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ∈ ℝ)
22081, 219fsumrecl 14924 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ∈ ℝ)
221216, 220eqeltrrd 2884 . . . . . . 7 (𝜑 → ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) ∈ ℝ)
222221, 93remulcld 10517 . . . . . 6 (𝜑 → (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅) ∈ ℝ)
223125abscld 14630 . . . . . . . 8 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
224132abscld 14630 . . . . . . . 8 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
225223, 224readdcld 10516 . . . . . . 7 (𝜑 → ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ∈ ℝ)
226125, 132abs2dif2d 14652 . . . . . . 7 (𝜑 → (abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))))
227115, 93remulcld 10517 . . . . . . . . 9 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 · 𝑅) ∈ ℝ)
22899, 93remulcld 10517 . . . . . . . . 9 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 · 𝑅) ∈ ℝ)
229116, 124absmuld 14648 . . . . . . . . . . 11 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) = ((abs‘(𝐽 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))))
230 eluzelre 12104 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (ℤ𝑀) → 𝑖 ∈ ℝ)
231230adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℝ)
232 eluzle 12106 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (ℤ𝑀) → 𝑀𝑖)
233232adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀𝑖)
23431nnred 11501 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℝ)
235234adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ)
236 elicopnf 12683 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℝ → (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀𝑖)))
237235, 236syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀𝑖)))
238231, 233, 237mpbir2and 709 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ (𝑀[,)+∞))
239238ex 413 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑖 ∈ (ℤ𝑀) → 𝑖 ∈ (𝑀[,)+∞)))
240239ssrdv 3895 . . . . . . . . . . . . . . 15 (𝜑 → (ℤ𝑀) ⊆ (𝑀[,)+∞))
24131nnzd 11935 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℤ)
24248peano2zd 11939 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐼 + 1) ∈ ℤ)
243101rpred 12281 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 ∈ ℝ)
2444nnred 11501 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐼 + 1) ∈ ℝ)
245 dchrisumlem2.2 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀𝑈)
246 dchrisumlem2.3 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 ≤ (𝐼 + 1))
247234, 243, 244, 245, 246letrd 10644 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ≤ (𝐼 + 1))
248 eluz2 12099 . . . . . . . . . . . . . . . . 17 ((𝐼 + 1) ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝐼 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝐼 + 1)))
249241, 242, 247, 248syl3anbrc 1336 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐼 + 1) ∈ (ℤ𝑀))
250 uztrn 12110 . . . . . . . . . . . . . . . 16 (((𝐽 + 1) ∈ (ℤ‘(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (ℤ𝑀)) → (𝐽 + 1) ∈ (ℤ𝑀))
2519, 249, 250syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → (𝐽 + 1) ∈ (ℤ𝑀))
252240, 251sseldd 3890 . . . . . . . . . . . . . 14 (𝜑 → (𝐽 + 1) ∈ (𝑀[,)+∞))
253113simprd 496 . . . . . . . . . . . . . 14 (𝜑 → ((𝐽 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐽 + 1) / 𝑛𝐴))
254252, 253mpd 15 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ (𝐽 + 1) / 𝑛𝐴)
255115, 254absidd 14616 . . . . . . . . . . . 12 (𝜑 → (abs‘(𝐽 + 1) / 𝑛𝐴) = (𝐽 + 1) / 𝑛𝐴)
256255oveq1d 7031 . . . . . . . . . . 11 (𝜑 → ((abs‘(𝐽 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐽 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))))
257229, 256eqtrd 2831 . . . . . . . . . 10 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐽 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))))
258124abscld 14630 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ∈ ℝ)
259111nnnn0d 11803 . . . . . . . . . . . 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 25747 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐽 + 1) ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
262259, 261mpdan 683 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
263258, 93, 115, 254, 262lemul2ad 11428 . . . . . . . . . 10 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐽 + 1) / 𝑛𝐴 · 𝑅))
264257, 263eqbrtrd 4984 . . . . . . . . 9 (𝜑 → (abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐽 + 1) / 𝑛𝐴 · 𝑅))
265126, 131absmuld 14648 . . . . . . . . . . 11 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) = ((abs‘(𝐼 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))))
266240, 249sseldd 3890 . . . . . . . . . . . . . 14 (𝜑 → (𝐼 + 1) ∈ (𝑀[,)+∞))
26719, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35dchrisumlema 25746 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐼 + 1) ∈ ℝ+(𝐼 + 1) / 𝑛𝐴 ∈ ℝ) ∧ ((𝐼 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐼 + 1) / 𝑛𝐴)))
268267simprd 496 . . . . . . . . . . . . . 14 (𝜑 → ((𝐼 + 1) ∈ (𝑀[,)+∞) → 0 ≤ (𝐼 + 1) / 𝑛𝐴))
269266, 268mpd 15 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ (𝐼 + 1) / 𝑛𝐴)
27099, 269absidd 14616 . . . . . . . . . . . 12 (𝜑 → (abs‘(𝐼 + 1) / 𝑛𝐴) = (𝐼 + 1) / 𝑛𝐴)
271270oveq1d 7031 . . . . . . . . . . 11 (𝜑 → ((abs‘(𝐼 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐼 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))))
272265, 271eqtrd 2831 . . . . . . . . . 10 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) = ((𝐼 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))))
273131abscld 14630 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ∈ ℝ)
2744nnnn0d 11803 . . . . . . . . . . . 12 (𝜑 → (𝐼 + 1) ∈ ℕ0)
27519, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35, 93, 260dchrisumlem1 25747 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐼 + 1) ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
276274, 275mpdan 683 . . . . . . . . . . 11 (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
277273, 93, 99, 269, 276lemul2ad 11428 . . . . . . . . . 10 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐼 + 1) / 𝑛𝐴 · 𝑅))
278272, 277eqbrtrd 4984 . . . . . . . . 9 (𝜑 → (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝐼 + 1) / 𝑛𝐴 · 𝑅))
279223, 224, 227, 228, 264, 278le2addd 11107 . . . . . . . 8 (𝜑 → ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ (((𝐽 + 1) / 𝑛𝐴 · 𝑅) + ((𝐼 + 1) / 𝑛𝐴 · 𝑅)))
28093recnd 10515 . . . . . . . . 9 (𝜑𝑅 ∈ ℂ)
281116, 126, 280adddird 10512 . . . . . . . 8 (𝜑 → (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) = (((𝐽 + 1) / 𝑛𝐴 · 𝑅) + ((𝐼 + 1) / 𝑛𝐴 · 𝑅)))
282279, 281breqtrrd 4990 . . . . . . 7 (𝜑 → ((abs‘((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛)))) + (abs‘((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅))
283134, 225, 215, 226, 282letrd 10644 . . . . . 6 (𝜑 → (abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) ≤ (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅))
284154abscld 14630 . . . . . . . 8 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
28581, 284fsumrecl 14924 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ∈ ℝ)
28681, 154fsumabs 14989 . . . . . . 7 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
28793adantr 481 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑅 ∈ ℝ)
288219, 287remulcld 10517 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) ∈ ℝ)
289135, 146syldan 591 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) ∈ ℂ)
290151adantr 481 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)) ∈ ℂ)
291289, 290absmuld 14648 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) = ((abs‘((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
292 elfzouz 12892 . . . . . . . . . . . . . . 15 (𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1)) → 𝑖 ∈ (ℤ‘(𝐼 + 1)))
293 uztrn 12110 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (ℤ‘(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (ℤ𝑀)) → 𝑖 ∈ (ℤ𝑀))
294292, 249, 293syl2anr 596 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ (ℤ𝑀))
295 eluznn 12167 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℕ ∧ 𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℕ)
29631, 295sylan 580 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℕ)
297296, 137syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑖 + 1) ∈ ℝ+)
298296nnrpd 12279 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℝ+)
299333expia 1114 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+)) → ((𝑀𝑛𝑛𝑥) → 𝐵𝐴))
300299ralrimivva 3158 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴))
301300adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → ∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴))
302 nfcv 2949 . . . . . . . . . . . . . . . . . 18 𝑛+
303 nfv 1892 . . . . . . . . . . . . . . . . . . 19 𝑛(𝑀𝑖𝑖𝑥)
304 nfcv 2949 . . . . . . . . . . . . . . . . . . . 20 𝑛𝐵
305 nfcv 2949 . . . . . . . . . . . . . . . . . . . 20 𝑛
306304, 305, 59nfbr 5009 . . . . . . . . . . . . . . . . . . 19 𝑛 𝐵𝑖 / 𝑛𝐴
307303, 306nfim 1878 . . . . . . . . . . . . . . . . . 18 𝑛((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)
308302, 307nfral 3191 . . . . . . . . . . . . . . . . 17 𝑛𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)
309 breq2 4966 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑖 → (𝑀𝑛𝑀𝑖))
310 breq1 4965 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑖 → (𝑛𝑥𝑖𝑥))
311309, 310anbi12d 630 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑖 → ((𝑀𝑛𝑛𝑥) ↔ (𝑀𝑖𝑖𝑥)))
31262breq2d 4974 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑖 → (𝐵𝐴𝐵𝑖 / 𝑛𝐴))
313311, 312imbi12d 346 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑖 → (((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)))
314313ralbidv 3164 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 → (∀𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)))
315308, 314rspc 3553 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℝ+ → (∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) → ∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴)))
316298, 301, 315sylc 65 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → ∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴))
317231lep1d 11419 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ≤ (𝑖 + 1))
318233, 317jca 512 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑀𝑖𝑖 ≤ (𝑖 + 1)))
319 breq2 4966 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑖 + 1) → (𝑖𝑥𝑖 ≤ (𝑖 + 1)))
320319anbi2d 628 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑖 + 1) → ((𝑀𝑖𝑖𝑥) ↔ (𝑀𝑖𝑖 ≤ (𝑖 + 1))))
321 eqvisset 3454 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑖 + 1) → (𝑖 + 1) ∈ V)
322 eqtr3 2818 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) → 𝑥 = 𝑛)
32330equcoms 2004 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑛𝐴 = 𝐵)
324322, 323syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) → 𝐴 = 𝐵)
325321, 324csbied 3844 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑖 + 1) → (𝑖 + 1) / 𝑛𝐴 = 𝐵)
326325eqcomd 2801 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑖 + 1) → 𝐵 = (𝑖 + 1) / 𝑛𝐴)
327326breq1d 4972 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑖 + 1) → (𝐵𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴))
328320, 327imbi12d 346 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑖 + 1) → (((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴) ↔ ((𝑀𝑖𝑖 ≤ (𝑖 + 1)) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)))
329328rspcv 3555 . . . . . . . . . . . . . . 15 ((𝑖 + 1) ∈ ℝ+ → (∀𝑥 ∈ ℝ+ ((𝑀𝑖𝑖𝑥) → 𝐵𝑖 / 𝑛𝐴) → ((𝑀𝑖𝑖 ≤ (𝑖 + 1)) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)))
330297, 316, 318, 329syl3c 66 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)
331294, 330syldan 591 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)
332218, 217, 331abssuble0d 14626 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)) = (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴))
333332oveq1d 7031 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((abs‘((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴)) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) = ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
334291, 333eqtrd 2831 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) = ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))))
335290abscld 14630 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ∈ ℝ)
336217, 218subge0d 11078 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (0 ≤ (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ↔ (𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴))
337331, 336mpbird 258 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 0 ≤ (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴))
338135peano2nnd 11503 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) ∈ ℕ)
339338nnnn0d 11803 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) ∈ ℕ0)
34019, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35, 93, 260dchrisumlem1 25747 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 + 1) ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
341339, 340syldan 591 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))) ≤ 𝑅)
342335, 287, 219, 337, 341lemul2ad 11428 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
343334, 342eqbrtrd 4984 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ ((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
34481, 284, 288, 343fsumle 14987 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
345219recnd 10515 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) ∈ ℂ)
34681, 280, 345fsummulc1 14973 . . . . . . . . 9 (𝜑 → (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅))
347216oveq1d 7031 . . . . . . . . 9 (𝜑 → (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) = (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
348346, 347eqtr3d 2833 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑖 / 𝑛𝐴(𝑖 + 1) / 𝑛𝐴) · 𝑅) = (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
349344, 348breqtrd 4988 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
350156, 285, 222, 286, 349letrd 10644 . . . . . 6 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛)))) ≤ (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅))
351134, 156, 215, 222, 283, 350le2addd 11107 . . . . 5 (𝜑 → ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))) ≤ ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) + (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅)))
3521262timesd 11728 . . . . . . . 8 (𝜑 → (2 · (𝐼 + 1) / 𝑛𝐴) = ((𝐼 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴))
353126, 116, 126ppncand 10885 . . . . . . . 8 (𝜑 → (((𝐼 + 1) / 𝑛𝐴 + (𝐽 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) = ((𝐼 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴))
354126, 116addcomd 10689 . . . . . . . . 9 (𝜑 → ((𝐼 + 1) / 𝑛𝐴 + (𝐽 + 1) / 𝑛𝐴) = ((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴))
355354oveq1d 7031 . . . . . . . 8 (𝜑 → (((𝐼 + 1) / 𝑛𝐴 + (𝐽 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) = (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)))
356352, 353, 3553eqtr2d 2837 . . . . . . 7 (𝜑 → (2 · (𝐼 + 1) / 𝑛𝐴) = (((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)))
357356oveq1d 7031 . . . . . 6 (𝜑 → ((2 · (𝐼 + 1) / 𝑛𝐴) · 𝑅) = ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) · 𝑅))
358 2cnd 11563 . . . . . . 7 (𝜑 → 2 ∈ ℂ)
359358, 126, 280mul32d 10697 . . . . . 6 (𝜑 → ((2 · (𝐼 + 1) / 𝑛𝐴) · 𝑅) = ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴))
360214recnd 10515 . . . . . . 7 (𝜑 → ((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) ∈ ℂ)
361221recnd 10515 . . . . . . 7 (𝜑 → ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) ∈ ℂ)
362360, 361, 280adddird 10512 . . . . . 6 (𝜑 → ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) + ((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴)) · 𝑅) = ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) + (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅)))
363357, 359, 3623eqtr3d 2839 . . . . 5 (𝜑 → ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴) = ((((𝐽 + 1) / 𝑛𝐴 + (𝐼 + 1) / 𝑛𝐴) · 𝑅) + (((𝐼 + 1) / 𝑛𝐴(𝐽 + 1) / 𝑛𝐴) · 𝑅)))
364351, 363breqtrrd 4990 . . . 4 (𝜑 → ((abs‘(((𝐽 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))) − ((𝐼 + 1) / 𝑛𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(((𝑖 + 1) / 𝑛𝐴𝑖 / 𝑛𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿𝑛))))) ≤ ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴))
36590, 157, 100, 213, 364letrd 10644 . . 3 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ≤ ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴))
366 2nn0 11762 . . . . . 6 2 ∈ ℕ0
367 nn0ge0 11770 . . . . . 6 (2 ∈ ℕ0 → 0 ≤ 2)
368366, 367mp1i 13 . . . . 5 (𝜑 → 0 ≤ 2)
369 0red 10490 . . . . . 6 (𝜑 → 0 ∈ ℝ)
370124absge0d 14638 . . . . . 6 (𝜑 → 0 ≤ (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿𝑛))))
371369, 258, 93, 370, 262letrd 10644 . . . . 5 (𝜑 → 0 ≤ 𝑅)
37292, 93, 368, 371mulge0d 11065 . . . 4 (𝜑 → 0 ≤ (2 · 𝑅))
3734nnrpd 12279 . . . . 5 (𝜑 → (𝐼 + 1) ∈ ℝ+)
374 nfv 1892 . . . . . . . . 9 𝑛(𝑀𝑈𝑈𝑥)
375304, 305, 103nfbr 5009 . . . . . . . . 9 𝑛 𝐵𝑈 / 𝑛𝐴
376374, 375nfim 1878 . . . . . . . 8 𝑛((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)
377302, 376nfral 3191 . . . . . . 7 𝑛𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)
378 breq2 4966 . . . . . . . . . 10 (𝑛 = 𝑈 → (𝑀𝑛𝑀𝑈))
379 breq1 4965 . . . . . . . . . 10 (𝑛 = 𝑈 → (𝑛𝑥𝑈𝑥))
380378, 379anbi12d 630 . . . . . . . . 9 (𝑛 = 𝑈 → ((𝑀𝑛𝑛𝑥) ↔ (𝑀𝑈𝑈𝑥)))
381105breq2d 4974 . . . . . . . . 9 (𝑛 = 𝑈 → (𝐵𝐴𝐵𝑈 / 𝑛𝐴))
382380, 381imbi12d 346 . . . . . . . 8 (𝑛 = 𝑈 → (((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)))
383382ralbidv 3164 . . . . . . 7 (𝑛 = 𝑈 → (∀𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) ↔ ∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)))
384377, 383rspc 3553 . . . . . 6 (𝑈 ∈ ℝ+ → (∀𝑛 ∈ ℝ+𝑥 ∈ ℝ+ ((𝑀𝑛𝑛𝑥) → 𝐵𝐴) → ∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴)))
385101, 300, 384sylc 65 . . . . 5 (𝜑 → ∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴))
386245, 246jca 512 . . . . 5 (𝜑 → (𝑀𝑈𝑈 ≤ (𝐼 + 1)))
387 breq2 4966 . . . . . . . 8 (𝑥 = (𝐼 + 1) → (𝑈𝑥𝑈 ≤ (𝐼 + 1)))
388387anbi2d 628 . . . . . . 7 (𝑥 = (𝐼 + 1) → ((𝑀𝑈𝑈𝑥) ↔ (𝑀𝑈𝑈 ≤ (𝐼 + 1))))
389 eqvisset 3454 . . . . . . . . . 10 (𝑥 = (𝐼 + 1) → (𝐼 + 1) ∈ V)
390 eqtr3 2818 . . . . . . . . . . 11 ((𝑥 = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) → 𝑥 = 𝑛)
391390, 323syl 17 . . . . . . . . . 10 ((𝑥 = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) → 𝐴 = 𝐵)
392389, 391csbied 3844 . . . . . . . . 9 (𝑥 = (𝐼 + 1) → (𝐼 + 1) / 𝑛𝐴 = 𝐵)
393392eqcomd 2801 . . . . . . . 8 (𝑥 = (𝐼 + 1) → 𝐵 = (𝐼 + 1) / 𝑛𝐴)
394393breq1d 4972 . . . . . . 7 (𝑥 = (𝐼 + 1) → (𝐵𝑈 / 𝑛𝐴(𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴))
395388, 394imbi12d 346 . . . . . 6 (𝑥 = (𝐼 + 1) → (((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴) ↔ ((𝑀𝑈𝑈 ≤ (𝐼 + 1)) → (𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴)))
396395rspcv 3555 . . . . 5 ((𝐼 + 1) ∈ ℝ+ → (∀𝑥 ∈ ℝ+ ((𝑀𝑈𝑈𝑥) → 𝐵𝑈 / 𝑛𝐴) → ((𝑀𝑈𝑈 ≤ (𝐼 + 1)) → (𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴)))
397373, 385, 386, 396syl3c 66 . . . 4 (𝜑(𝐼 + 1) / 𝑛𝐴𝑈 / 𝑛𝐴)
39899, 108, 94, 372, 397lemul2ad 11428 . . 3 (𝜑 → ((2 · 𝑅) · (𝐼 + 1) / 𝑛𝐴) ≤ ((2 · 𝑅) · 𝑈 / 𝑛𝐴))
39990, 100, 109, 365, 398letrd 10644 . 2 (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)) ≤ ((2 · 𝑅) · 𝑈 / 𝑛𝐴))
40089, 399eqbrtrd 4984 1 (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) ≤ ((2 · 𝑅) · 𝑈 / 𝑛𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1080   = wceq 1522  wcel 2081  wne 2984  wral 3105  Vcvv 3437  csb 3811  cun 3857  cin 3858  c0 4211   class class class wbr 4962  cmpt 5041  cfv 6225  (class class class)co 7016  Fincfn 8357  cc 10381  cr 10382  0cc0 10383  1c1 10384   + caddc 10386   · cmul 10388  +∞cpnf 10518  cle 10522  cmin 10717  cn 11486  2c2 11540  0cn0 11745  cz 11829  cuz 12093  +crp 12239  [,)cico 12590  ...cfz 12742  ..^cfzo 12883  seqcseq 13219  abscabs 14427  𝑟 crli 14676  Σcsu 14876  Basecbs 16312  0gc0g 16542  ℤRHomczrh 20329  ℤ/nczn 20332  DChrcdchr 25490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-inf2 8950  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460  ax-pre-sup 10461  ax-addf 10462  ax-mulf 10463
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-fal 1535  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-se 5403  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-isom 6234  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-of 7267  df-om 7437  df-1st 7545  df-2nd 7546  df-tpos 7743  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-oadd 7957  df-er 8139  df-ec 8141  df-qs 8145  df-map 8258  df-pm 8259  df-en 8358  df-dom 8359  df-sdom 8360  df-fin 8361  df-sup 8752  df-inf 8753  df-oi 8820  df-card 9214  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-div 11146  df-nn 11487  df-2 11548  df-3 11549  df-4 11550  df-5 11551  df-6 11552  df-7 11553  df-8 11554  df-9 11555  df-n0 11746  df-xnn0 11816  df-z 11830  df-dec 11948  df-uz 12094  df-rp 12240  df-ico 12594  df-fz 12743  df-fzo 12884  df-fl 13012  df-mod 13088  df-seq 13220  df-exp 13280  df-hash 13541  df-cj 14292  df-re 14293  df-im 14294  df-sqrt 14428  df-abs 14429  df-clim 14679  df-rlim 14680  df-sum 14877  df-dvds 15441  df-gcd 15677  df-phi 15932  df-struct 16314  df-ndx 16315  df-slot 16316  df-base 16318  df-sets 16319  df-ress 16320  df-plusg 16407  df-mulr 16408  df-starv 16409  df-sca 16410  df-vsca 16411  df-ip 16412  df-tset 16413  df-ple 16414  df-ds 16416  df-unif 16417  df-0g 16544  df-imas 16610  df-qus 16611  df-mgm 17681  df-sgrp 17723  df-mnd 17734  df-mhm 17774  df-grp 17864  df-minusg 17865  df-sbg 17866  df-mulg 17982  df-subg 18030  df-nsg 18031  df-eqg 18032  df-ghm 18097  df-cmn 18635  df-abl 18636  df-mgp 18930  df-ur 18942  df-ring 18989  df-cring 18990  df-oppr 19063  df-dvdsr 19081  df-unit 19082  df-invr 19112  df-rnghom 19157  df-subrg 19223  df-lmod 19326  df-lss 19394  df-lsp 19434  df-sra 19634  df-rgmod 19635  df-lidl 19636  df-rsp 19637  df-2idl 19694  df-cnfld 20228  df-zring 20300  df-zrh 20333  df-zn 20336  df-dchr 25491
This theorem is referenced by:  dchrisumlem3  25749
  Copyright terms: Public domain W3C validator