This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dchrisumlem2

Description: Lemma for dchrisum . Lemma 9.4.1 of Shapiro, p. 377. (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses 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 dchrisumlem2 ( 𝜑 → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝐽 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝐼 ) ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2 rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3 rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 rpvmasum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
5 rpvmasum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
6 rpvmasum.1 ⊢ 1 = ( 0g ‘ 𝐺 )
7 dchrisum.b ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8 dchrisum.n1 ⊢ ( 𝜑 → 𝑋 ≠ 1 )
9 dchrisum.2 ⊢ ( 𝑛 = 𝑥 → 𝐴 = 𝐵 )
10 dchrisum.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
11 dchrisum.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
12 dchrisum.5 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
13 dchrisum.6 ⊢ ( 𝜑 → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
14 dchrisum.7 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · 𝐴 ) )
15 dchrisum.9 ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
16 dchrisum.10 ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( 0 ..^ 𝑁 ) ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
17 dchrisumlem2.1 ⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
18 dchrisumlem2.2 ⊢ ( 𝜑 → 𝑀 ≤ 𝑈 )
19 dchrisumlem2.3 ⊢ ( 𝜑 → 𝑈 ≤ ( 𝐼 + 1 ) )
20 dchrisumlem2.4 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
21 dchrisumlem2.5 ⊢ ( 𝜑 → 𝐽 ∈ ( ℤ≥ ‘ 𝐼 ) )
22 fzodisj ⊢ ( ( 1 ..^ ( 𝐼 + 1 ) ) ∩ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) = ∅
23 22 a1i ⊢ ( 𝜑 → ( ( 1 ..^ ( 𝐼 + 1 ) ) ∩ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) = ∅ )
24 20 peano2nnd ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ℕ )
25 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
26 24 25 eleqtrdi ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
27 eluzp1p1 ⊢ ( 𝐽 ∈ ( ℤ≥ ‘ 𝐼 ) → ( 𝐽 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) )
28 21 27 syl ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) )
29 elfzuzb ⊢ ( ( 𝐼 + 1 ) ∈ ( 1 ... ( 𝐽 + 1 ) ) ↔ ( ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ ( 𝐽 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) ) )
30 26 28 29 sylanbrc ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ( 1 ... ( 𝐽 + 1 ) ) )
31 fzosplit ⊢ ( ( 𝐼 + 1 ) ∈ ( 1 ... ( 𝐽 + 1 ) ) → ( 1 ..^ ( 𝐽 + 1 ) ) = ( ( 1 ..^ ( 𝐼 + 1 ) ) ∪ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) )
32 30 31 syl ⊢ ( 𝜑 → ( 1 ..^ ( 𝐽 + 1 ) ) = ( ( 1 ..^ ( 𝐼 + 1 ) ) ∪ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) )
33 fzofi ⊢ ( 1 ..^ ( 𝐽 + 1 ) ) ∈ Fin
34 33 a1i ⊢ ( 𝜑 → ( 1 ..^ ( 𝐽 + 1 ) ) ∈ Fin )
35 elfzouz ⊢ ( 𝑖 ∈ ( 1 ..^ ( 𝐽 + 1 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 1 ) )
36 35 25 eleqtrrdi ⊢ ( 𝑖 ∈ ( 1 ..^ ( 𝐽 + 1 ) ) → 𝑖 ∈ ℕ )
37 7 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑋 ∈ 𝐷 )
38 nnz ⊢ ( 𝑖 ∈ ℕ → 𝑖 ∈ ℤ )
39 38 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ℤ )
40 4 1 5 2 37 39 dchrzrhcl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) ∈ ℂ )
41 1 2 3 4 5 6 7 8 9 10 11 12 13 14 dchrisumlema ⊢ ( 𝜑 → ( ( 𝑖 ∈ ℝ+ → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ ) ∧ ( 𝑖 ∈ ( 𝑀 [,) +∞ ) → 0 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) )
42 41 simpld ⊢ ( 𝜑 → ( 𝑖 ∈ ℝ+ → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
43 nnrp ⊢ ( 𝑖 ∈ ℕ → 𝑖 ∈ ℝ+ )
44 42 43 impel ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ )
45 44 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℂ )
46 40 45 mulcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ∈ ℂ )
47 36 46 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ..^ ( 𝐽 + 1 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ∈ ℂ )
48 23 32 34 47 fsumsplit ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) = ( Σ 𝑖 ∈ ( 1 ..^ ( 𝐼 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) + Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) )
49 eluzelz ⊢ ( 𝐽 ∈ ( ℤ≥ ‘ 𝐼 ) → 𝐽 ∈ ℤ )
50 fzval3 ⊢ ( 𝐽 ∈ ℤ → ( 1 ... 𝐽 ) = ( 1 ..^ ( 𝐽 + 1 ) ) )
51 21 49 50 3syl ⊢ ( 𝜑 → ( 1 ... 𝐽 ) = ( 1 ..^ ( 𝐽 + 1 ) ) )
52 51 sumeq1d ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝐽 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) = Σ 𝑖 ∈ ( 1 ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
53 20 nnzd ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
54 fzval3 ⊢ ( 𝐼 ∈ ℤ → ( 1 ... 𝐼 ) = ( 1 ..^ ( 𝐼 + 1 ) ) )
55 53 54 syl ⊢ ( 𝜑 → ( 1 ... 𝐼 ) = ( 1 ..^ ( 𝐼 + 1 ) ) )
56 55 sumeq1d ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝐼 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) = Σ 𝑖 ∈ ( 1 ..^ ( 𝐼 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
57 56 oveq1d ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 1 ... 𝐼 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) + Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) = ( Σ 𝑖 ∈ ( 1 ..^ ( 𝐼 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) + Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) )
58 48 52 57 3eqtr4d ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝐽 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) = ( Σ 𝑖 ∈ ( 1 ... 𝐼 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) + Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) )
59 elfznn ⊢ ( 𝑖 ∈ ( 1 ... 𝐽 ) → 𝑖 ∈ ℕ )
60 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ℕ )
61 nfcv ⊢ Ⅎ 𝑛 𝑖
62 nfcv ⊢ Ⅎ 𝑛 ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) )
63 nfcv ⊢ Ⅎ 𝑛 ·
64 nfcsb1v ⊢ Ⅎ 𝑛 ⦋ 𝑖 / 𝑛 ⦌ 𝐴
65 62 63 64 nfov ⊢ Ⅎ 𝑛 ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 )
66 2fveq3 ⊢ ( 𝑛 = 𝑖 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) )
67 csbeq1a ⊢ ( 𝑛 = 𝑖 → 𝐴 = ⦋ 𝑖 / 𝑛 ⦌ 𝐴 )
68 66 67 oveq12d ⊢ ( 𝑛 = 𝑖 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · 𝐴 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
69 61 65 68 14 fvmptf ⊢ ( ( 𝑖 ∈ ℕ ∧ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ∈ ℂ ) → ( 𝐹 ‘ 𝑖 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
70 60 46 69 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝐹 ‘ 𝑖 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
71 59 70 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝐽 ) ) → ( 𝐹 ‘ 𝑖 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
72 20 25 eleqtrdi ⊢ ( 𝜑 → 𝐼 ∈ ( ℤ≥ ‘ 1 ) )
73 uztrn ⊢ ( ( 𝐽 ∈ ( ℤ≥ ‘ 𝐼 ) ∧ 𝐼 ∈ ( ℤ≥ ‘ 1 ) ) → 𝐽 ∈ ( ℤ≥ ‘ 1 ) )
74 21 72 73 syl2anc ⊢ ( 𝜑 → 𝐽 ∈ ( ℤ≥ ‘ 1 ) )
75 59 46 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝐽 ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ∈ ℂ )
76 71 74 75 fsumser ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝐽 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) = ( seq 1 ( + , 𝐹 ) ‘ 𝐽 ) )
77 58 76 eqtr3d ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 1 ... 𝐼 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) + Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) = ( seq 1 ( + , 𝐹 ) ‘ 𝐽 ) )
78 elfznn ⊢ ( 𝑖 ∈ ( 1 ... 𝐼 ) → 𝑖 ∈ ℕ )
79 78 70 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝐼 ) ) → ( 𝐹 ‘ 𝑖 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
80 78 46 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝐼 ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ∈ ℂ )
81 79 72 80 fsumser ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝐼 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) = ( seq 1 ( + , 𝐹 ) ‘ 𝐼 ) )
82 77 81 oveq12d ⊢ ( 𝜑 → ( ( Σ 𝑖 ∈ ( 1 ... 𝐼 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) + Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) − Σ 𝑖 ∈ ( 1 ... 𝐼 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) = ( ( seq 1 ( + , 𝐹 ) ‘ 𝐽 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝐼 ) ) )
83 fzfid ⊢ ( 𝜑 → ( 1 ... 𝐼 ) ∈ Fin )
84 83 80 fsumcl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝐼 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ∈ ℂ )
85 fzofi ⊢ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ∈ Fin
86 85 a1i ⊢ ( 𝜑 → ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ∈ Fin )
87 ssun2 ⊢ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ⊆ ( ( 1 ..^ ( 𝐼 + 1 ) ) ∪ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) )
88 87 32 sseqtrrid ⊢ ( 𝜑 → ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ⊆ ( 1 ..^ ( 𝐽 + 1 ) ) )
89 88 sselda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → 𝑖 ∈ ( 1 ..^ ( 𝐽 + 1 ) ) )
90 89 47 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ∈ ℂ )
91 86 90 fsumcl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ∈ ℂ )
92 84 91 pncan2d ⊢ ( 𝜑 → ( ( Σ 𝑖 ∈ ( 1 ... 𝐼 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) + Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) − Σ 𝑖 ∈ ( 1 ... 𝐼 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) = Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
93 82 92 eqtr3d ⊢ ( 𝜑 → ( ( seq 1 ( + , 𝐹 ) ‘ 𝐽 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝐼 ) ) = Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
94 93 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝐽 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝐼 ) ) ) = ( abs ‘ Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) )
95 91 abscld ⊢ ( 𝜑 → ( abs ‘ Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) ∈ ℝ )
96 2re ⊢ 2 ∈ ℝ
97 96 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
98 97 15 remulcld ⊢ ( 𝜑 → ( 2 · 𝑅 ) ∈ ℝ )
99 44 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ℕ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ )
100 csbeq1 ⊢ ( 𝑖 = ( 𝐼 + 1 ) → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 = ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 )
101 100 eleq1d ⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ ↔ ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
102 101 rspcv ⊢ ( ( 𝐼 + 1 ) ∈ ℕ → ( ∀ 𝑖 ∈ ℕ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ → ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
103 24 99 102 sylc ⊢ ( 𝜑 → ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ∈ ℝ )
104 98 103 remulcld ⊢ ( 𝜑 → ( ( 2 · 𝑅 ) · ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
105 11 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ )
106 nfcsb1v ⊢ Ⅎ 𝑛 ⦋ 𝑈 / 𝑛 ⦌ 𝐴
107 106 nfel1 ⊢ Ⅎ 𝑛 ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ∈ ℝ
108 csbeq1a ⊢ ( 𝑛 = 𝑈 → 𝐴 = ⦋ 𝑈 / 𝑛 ⦌ 𝐴 )
109 108 eleq1d ⊢ ( 𝑛 = 𝑈 → ( 𝐴 ∈ ℝ ↔ ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
110 107 109 rspc ⊢ ( 𝑈 ∈ ℝ+ → ( ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
111 17 105 110 sylc ⊢ ( 𝜑 → ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ∈ ℝ )
112 98 111 remulcld ⊢ ( 𝜑 → ( ( 2 · 𝑅 ) · ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
113 74 25 eleqtrrdi ⊢ ( 𝜑 → 𝐽 ∈ ℕ )
114 113 peano2nnd ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ℕ )
115 114 nnrpd ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ℝ+ )
116 1 2 3 4 5 6 7 8 9 10 11 12 13 14 dchrisumlema ⊢ ( 𝜑 → ( ( ( 𝐽 + 1 ) ∈ ℝ+ → ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ∈ ℝ ) ∧ ( ( 𝐽 + 1 ) ∈ ( 𝑀 [,) +∞ ) → 0 ≤ ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) ) )
117 116 simpld ⊢ ( 𝜑 → ( ( 𝐽 + 1 ) ∈ ℝ+ → ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
118 115 117 mpd ⊢ ( 𝜑 → ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ∈ ℝ )
119 118 recnd ⊢ ( 𝜑 → ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ∈ ℂ )
120 fzofi ⊢ ( 0 ..^ ( 𝐽 + 1 ) ) ∈ Fin
121 120 a1i ⊢ ( 𝜑 → ( 0 ..^ ( 𝐽 + 1 ) ) ∈ Fin )
122 elfzoelz ⊢ ( 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) → 𝑛 ∈ ℤ )
123 7 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℤ ) → 𝑋 ∈ 𝐷 )
124 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℤ )
125 4 1 5 2 123 124 dchrzrhcl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℤ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
126 122 125 sylan2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
127 121 126 fsumcl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
128 119 127 mulcld ⊢ ( 𝜑 → ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ∈ ℂ )
129 103 recnd ⊢ ( 𝜑 → ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ∈ ℂ )
130 fzofi ⊢ ( 0 ..^ ( 𝐼 + 1 ) ) ∈ Fin
131 130 a1i ⊢ ( 𝜑 → ( 0 ..^ ( 𝐼 + 1 ) ) ∈ Fin )
132 elfzoelz ⊢ ( 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) → 𝑛 ∈ ℤ )
133 132 125 sylan2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
134 131 133 fsumcl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
135 129 134 mulcld ⊢ ( 𝜑 → ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ∈ ℂ )
136 128 135 subcld ⊢ ( 𝜑 → ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) − ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ∈ ℂ )
137 136 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) − ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ) ∈ ℝ )
138 89 36 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → 𝑖 ∈ ℕ )
139 peano2nn ⊢ ( 𝑖 ∈ ℕ → ( 𝑖 + 1 ) ∈ ℕ )
140 139 nnrpd ⊢ ( 𝑖 ∈ ℕ → ( 𝑖 + 1 ) ∈ ℝ+ )
141 nfcsb1v ⊢ Ⅎ 𝑛 ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴
142 141 nfel1 ⊢ Ⅎ 𝑛 ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ∈ ℝ
143 csbeq1a ⊢ ( 𝑛 = ( 𝑖 + 1 ) → 𝐴 = ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 )
144 143 eleq1d ⊢ ( 𝑛 = ( 𝑖 + 1 ) → ( 𝐴 ∈ ℝ ↔ ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
145 142 144 rspc ⊢ ( ( 𝑖 + 1 ) ∈ ℝ+ → ( ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
146 145 impcom ⊢ ( ( ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ ∧ ( 𝑖 + 1 ) ∈ ℝ+ ) → ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ∈ ℝ )
147 105 140 146 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ∈ ℝ )
148 147 44 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
149 148 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ∈ ℂ )
150 fzofi ⊢ ( 0 ..^ ( 𝑖 + 1 ) ) ∈ Fin
151 150 a1i ⊢ ( 𝜑 → ( 0 ..^ ( 𝑖 + 1 ) ) ∈ Fin )
152 elfzoelz ⊢ ( 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) → 𝑛 ∈ ℤ )
153 152 125 sylan2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
154 151 153 fsumcl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
155 154 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
156 149 155 mulcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ∈ ℂ )
157 138 156 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ∈ ℂ )
158 86 157 fsumcl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ∈ ℂ )
159 158 abscld ⊢ ( 𝜑 → ( abs ‘ Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ∈ ℝ )
160 137 159 readdcld ⊢ ( 𝜑 → ( ( abs ‘ ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) − ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ) + ( abs ‘ Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ) ∈ ℝ )
161 40 45 mulcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) = ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 · ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) ) )
162 nnnn0 ⊢ ( 𝑖 ∈ ℕ → 𝑖 ∈ ℕ0 )
163 162 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ℕ0 )
164 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
165 163 164 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) )
166 elfzelz ⊢ ( 𝑛 ∈ ( 0 ... 𝑖 ) → 𝑛 ∈ ℤ )
167 125 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
168 166 167 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ 𝑛 ∈ ( 0 ... 𝑖 ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
169 165 168 66 fzosump1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = ( Σ 𝑛 ∈ ( 0 ..^ 𝑖 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) + ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) ) )
170 169 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) − Σ 𝑛 ∈ ( 0 ..^ 𝑖 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) = ( ( Σ 𝑛 ∈ ( 0 ..^ 𝑖 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) + ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) ) − Σ 𝑛 ∈ ( 0 ..^ 𝑖 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
171 fzofi ⊢ ( 0 ..^ 𝑖 ) ∈ Fin
172 171 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 0 ..^ 𝑖 ) ∈ Fin )
173 elfzoelz ⊢ ( 𝑛 ∈ ( 0 ..^ 𝑖 ) → 𝑛 ∈ ℤ )
174 173 167 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ 𝑛 ∈ ( 0 ..^ 𝑖 ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
175 172 174 fsumcl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → Σ 𝑛 ∈ ( 0 ..^ 𝑖 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
176 175 40 pncan2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( Σ 𝑛 ∈ ( 0 ..^ 𝑖 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) + ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) ) − Σ 𝑛 ∈ ( 0 ..^ 𝑖 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) )
177 170 176 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) = ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) − Σ 𝑛 ∈ ( 0 ..^ 𝑖 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
178 177 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 · ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) ) = ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 · ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) − Σ 𝑛 ∈ ( 0 ..^ 𝑖 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) )
179 161 178 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) = ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 · ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) − Σ 𝑛 ∈ ( 0 ..^ 𝑖 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) )
180 138 179 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) = ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 · ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) − Σ 𝑛 ∈ ( 0 ..^ 𝑖 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) )
181 180 sumeq2dv ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) = Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 · ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) − Σ 𝑛 ∈ ( 0 ..^ 𝑖 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) )
182 csbeq1 ⊢ ( 𝑘 = 𝑖 → ⦋ 𝑘 / 𝑛 ⦌ 𝐴 = ⦋ 𝑖 / 𝑛 ⦌ 𝐴 )
183 oveq2 ⊢ ( 𝑘 = 𝑖 → ( 0 ..^ 𝑘 ) = ( 0 ..^ 𝑖 ) )
184 183 sumeq1d ⊢ ( 𝑘 = 𝑖 → Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ 𝑖 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
185 182 184 jca ⊢ ( 𝑘 = 𝑖 → ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 = ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∧ Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ 𝑖 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
186 csbeq1 ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ⦋ 𝑘 / 𝑛 ⦌ 𝐴 = ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 )
187 oveq2 ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( 0 ..^ 𝑘 ) = ( 0 ..^ ( 𝑖 + 1 ) ) )
188 187 sumeq1d ⊢ ( 𝑘 = ( 𝑖 + 1 ) → Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
189 186 188 jca ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 = ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ∧ Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
190 csbeq1 ⊢ ( 𝑘 = ( 𝐼 + 1 ) → ⦋ 𝑘 / 𝑛 ⦌ 𝐴 = ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 )
191 oveq2 ⊢ ( 𝑘 = ( 𝐼 + 1 ) → ( 0 ..^ 𝑘 ) = ( 0 ..^ ( 𝐼 + 1 ) ) )
192 191 sumeq1d ⊢ ( 𝑘 = ( 𝐼 + 1 ) → Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
193 190 192 jca ⊢ ( 𝑘 = ( 𝐼 + 1 ) → ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 = ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ∧ Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
194 csbeq1 ⊢ ( 𝑘 = ( 𝐽 + 1 ) → ⦋ 𝑘 / 𝑛 ⦌ 𝐴 = ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 )
195 oveq2 ⊢ ( 𝑘 = ( 𝐽 + 1 ) → ( 0 ..^ 𝑘 ) = ( 0 ..^ ( 𝐽 + 1 ) ) )
196 195 sumeq1d ⊢ ( 𝑘 = ( 𝐽 + 1 ) → Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
197 194 196 jca ⊢ ( 𝑘 = ( 𝐽 + 1 ) → ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 = ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ∧ Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
198 45 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ℕ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℂ )
199 elfzuz ⊢ ( 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 + 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) )
200 eluznn ⊢ ( ( ( 𝐼 + 1 ) ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) ) → 𝑘 ∈ ℕ )
201 24 199 200 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 + 1 ) ) ) → 𝑘 ∈ ℕ )
202 csbeq1 ⊢ ( 𝑖 = 𝑘 → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 = ⦋ 𝑘 / 𝑛 ⦌ 𝐴 )
203 202 eleq1d ⊢ ( 𝑖 = 𝑘 → ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℂ ↔ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ ℂ ) )
204 203 rspccva ⊢ ( ( ∀ 𝑖 ∈ ℕ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ ) → ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ ℂ )
205 198 201 204 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 + 1 ) ) ) → ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ ℂ )
206 fzofi ⊢ ( 0 ..^ 𝑘 ) ∈ Fin
207 206 a1i ⊢ ( 𝜑 → ( 0 ..^ 𝑘 ) ∈ Fin )
208 elfzoelz ⊢ ( 𝑛 ∈ ( 0 ..^ 𝑘 ) → 𝑛 ∈ ℤ )
209 208 125 sylan2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑘 ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
210 207 209 fsumcl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
211 210 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 + 1 ) ) ) → Σ 𝑛 ∈ ( 0 ..^ 𝑘 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
212 185 189 193 197 28 205 211 fsumparts ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 · ( Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) − Σ 𝑛 ∈ ( 0 ..^ 𝑖 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) = ( ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) − ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) − Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) )
213 181 212 eqtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) = ( ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) − ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) − Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) )
214 213 fveq2d ⊢ ( 𝜑 → ( abs ‘ Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) = ( abs ‘ ( ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) − ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) − Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ) )
215 136 158 abs2dif2d ⊢ ( 𝜑 → ( 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 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ) )
216 214 215 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) ≤ ( ( abs ‘ ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) − ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ) + ( abs ‘ Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ) )
217 118 103 readdcld ⊢ ( 𝜑 → ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
218 217 15 remulcld ⊢ ( 𝜑 → ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) ∈ ℝ )
219 182 186 190 194 28 205 telfsumo ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) = ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) )
220 138 44 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ )
221 138 147 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ∈ ℝ )
222 220 221 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
223 86 222 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
224 219 223 eqeltrrd ⊢ ( 𝜑 → ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
225 224 15 remulcld ⊢ ( 𝜑 → ( ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) ∈ ℝ )
226 128 abscld ⊢ ( 𝜑 → ( abs ‘ ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ∈ ℝ )
227 135 abscld ⊢ ( 𝜑 → ( abs ‘ ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ∈ ℝ )
228 226 227 readdcld ⊢ ( 𝜑 → ( ( abs ‘ ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) + ( abs ‘ ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ) ∈ ℝ )
229 128 135 abs2dif2d ⊢ ( 𝜑 → ( abs ‘ ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) − ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ) ≤ ( ( abs ‘ ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) + ( abs ‘ ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ) )
230 118 15 remulcld ⊢ ( 𝜑 → ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · 𝑅 ) ∈ ℝ )
231 103 15 remulcld ⊢ ( 𝜑 → ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · 𝑅 ) ∈ ℝ )
232 119 127 absmuld ⊢ ( 𝜑 → ( abs ‘ ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) = ( ( abs ‘ ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) · ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) )
233 eluzelre ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑖 ∈ ℝ )
234 233 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑖 ∈ ℝ )
235 eluzle ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑖 )
236 235 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ≤ 𝑖 )
237 10 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
238 237 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ∈ ℝ )
239 elicopnf ⊢ ( 𝑀 ∈ ℝ → ( 𝑖 ∈ ( 𝑀 [,) +∞ ) ↔ ( 𝑖 ∈ ℝ ∧ 𝑀 ≤ 𝑖 ) ) )
240 238 239 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑖 ∈ ( 𝑀 [,) +∞ ) ↔ ( 𝑖 ∈ ℝ ∧ 𝑀 ≤ 𝑖 ) ) )
241 234 236 240 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑖 ∈ ( 𝑀 [,) +∞ ) )
242 241 ex ⊢ ( 𝜑 → ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑖 ∈ ( 𝑀 [,) +∞ ) ) )
243 242 ssrdv ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑀 ) ⊆ ( 𝑀 [,) +∞ ) )
244 10 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
245 53 peano2zd ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ℤ )
246 17 rpred ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
247 24 nnred ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ℝ )
248 237 246 247 18 19 letrd ⊢ ( 𝜑 → 𝑀 ≤ ( 𝐼 + 1 ) )
249 eluz2 ⊢ ( ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝐼 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝐼 + 1 ) ) )
250 244 245 248 249 syl3anbrc ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
251 uztrn ⊢ ( ( ( 𝐽 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) ∧ ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐽 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
252 28 250 251 syl2anc ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
253 243 252 sseldd ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ( 𝑀 [,) +∞ ) )
254 116 simprd ⊢ ( 𝜑 → ( ( 𝐽 + 1 ) ∈ ( 𝑀 [,) +∞ ) → 0 ≤ ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) )
255 253 254 mpd ⊢ ( 𝜑 → 0 ≤ ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 )
256 118 255 absidd ⊢ ( 𝜑 → ( abs ‘ ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) = ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 )
257 256 oveq1d ⊢ ( 𝜑 → ( ( abs ‘ ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) · ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) = ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) )
258 232 257 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) = ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) )
259 127 abscld ⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ∈ ℝ )
260 114 nnnn0d ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ℕ0 )
261 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 dchrisumlem1 ⊢ ( ( 𝜑 ∧ ( 𝐽 + 1 ) ∈ ℕ0 ) → ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
262 260 261 mpdan ⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
263 259 15 118 255 262 lemul2ad ⊢ ( 𝜑 → ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ≤ ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · 𝑅 ) )
264 258 263 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ≤ ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · 𝑅 ) )
265 129 134 absmuld ⊢ ( 𝜑 → ( abs ‘ ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) = ( ( abs ‘ ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) · ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) )
266 243 250 sseldd ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ( 𝑀 [,) +∞ ) )
267 1 2 3 4 5 6 7 8 9 10 11 12 13 14 dchrisumlema ⊢ ( 𝜑 → ( ( ( 𝐼 + 1 ) ∈ ℝ+ → ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ∈ ℝ ) ∧ ( ( 𝐼 + 1 ) ∈ ( 𝑀 [,) +∞ ) → 0 ≤ ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) ) )
268 267 simprd ⊢ ( 𝜑 → ( ( 𝐼 + 1 ) ∈ ( 𝑀 [,) +∞ ) → 0 ≤ ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) )
269 266 268 mpd ⊢ ( 𝜑 → 0 ≤ ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 )
270 103 269 absidd ⊢ ( 𝜑 → ( abs ‘ ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) = ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 )
271 270 oveq1d ⊢ ( 𝜑 → ( ( abs ‘ ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) · ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) = ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) )
272 265 271 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) = ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) )
273 134 abscld ⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ∈ ℝ )
274 24 nnnn0d ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ℕ0 )
275 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 dchrisumlem1 ⊢ ( ( 𝜑 ∧ ( 𝐼 + 1 ) ∈ ℕ0 ) → ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
276 274 275 mpdan ⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
277 273 15 103 269 276 lemul2ad ⊢ ( 𝜑 → ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ≤ ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · 𝑅 ) )
278 272 277 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ≤ ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · 𝑅 ) )
279 226 227 230 231 264 278 le2addd ⊢ ( 𝜑 → ( ( abs ‘ ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) + ( abs ‘ ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ) ≤ ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · 𝑅 ) + ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · 𝑅 ) ) )
280 15 recnd ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
281 119 129 280 adddird ⊢ ( 𝜑 → ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) = ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · 𝑅 ) + ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · 𝑅 ) ) )
282 279 281 breqtrrd ⊢ ( 𝜑 → ( ( abs ‘ ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) + ( abs ‘ ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ) ≤ ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) )
283 137 228 218 229 282 letrd ⊢ ( 𝜑 → ( abs ‘ ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) − ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ) ≤ ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) )
284 157 abscld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( abs ‘ ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ∈ ℝ )
285 86 284 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( abs ‘ ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ∈ ℝ )
286 86 157 fsumabs ⊢ ( 𝜑 → ( abs ‘ Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ≤ Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( abs ‘ ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) )
287 15 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → 𝑅 ∈ ℝ )
288 222 287 remulcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) ∈ ℝ )
289 138 149 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ∈ ℂ )
290 154 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
291 289 290 absmuld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( abs ‘ ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) = ( ( abs ‘ ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) · ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) )
292 elfzouz ⊢ ( 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) → 𝑖 ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) )
293 uztrn ⊢ ( ( 𝑖 ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) ∧ ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
294 292 250 293 syl2anr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
295 eluznn ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑖 ∈ ℕ )
296 10 295 sylan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑖 ∈ ℕ )
297 296 140 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ℝ+ )
298 296 nnrpd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑖 ∈ ℝ+ )
299 12 3expia ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ) → ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) → 𝐵 ≤ 𝐴 ) )
300 299 ralrimivva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℝ+ ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) → 𝐵 ≤ 𝐴 ) )
301 300 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ∀ 𝑛 ∈ ℝ+ ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) → 𝐵 ≤ 𝐴 ) )
302 nfcv ⊢ Ⅎ 𝑛 ℝ+
303 nfv ⊢ Ⅎ 𝑛 ( 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥 )
304 nfcv ⊢ Ⅎ 𝑛 𝐵
305 nfcv ⊢ Ⅎ 𝑛 ≤
306 304 305 64 nfbr ⊢ Ⅎ 𝑛 𝐵 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴
307 303 306 nfim ⊢ Ⅎ 𝑛 ( ( 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 )
308 302 307 nfralw ⊢ Ⅎ 𝑛 ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 )
309 breq2 ⊢ ( 𝑛 = 𝑖 → ( 𝑀 ≤ 𝑛 ↔ 𝑀 ≤ 𝑖 ) )
310 breq1 ⊢ ( 𝑛 = 𝑖 → ( 𝑛 ≤ 𝑥 ↔ 𝑖 ≤ 𝑥 ) )
311 309 310 anbi12d ⊢ ( 𝑛 = 𝑖 → ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ↔ ( 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥 ) ) )
312 67 breq2d ⊢ ( 𝑛 = 𝑖 → ( 𝐵 ≤ 𝐴 ↔ 𝐵 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
313 311 312 imbi12d ⊢ ( 𝑛 = 𝑖 → ( ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) → 𝐵 ≤ 𝐴 ) ↔ ( ( 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) )
314 313 ralbidv ⊢ ( 𝑛 = 𝑖 → ( ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) → 𝐵 ≤ 𝐴 ) ↔ ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) )
315 308 314 rspc ⊢ ( 𝑖 ∈ ℝ+ → ( ∀ 𝑛 ∈ ℝ+ ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) → 𝐵 ≤ 𝐴 ) → ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) )
316 298 301 315 sylc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
317 234 lep1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑖 ≤ ( 𝑖 + 1 ) )
318 236 317 jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ ( 𝑖 + 1 ) ) )
319 breq2 ⊢ ( 𝑥 = ( 𝑖 + 1 ) → ( 𝑖 ≤ 𝑥 ↔ 𝑖 ≤ ( 𝑖 + 1 ) ) )
320 319 anbi2d ⊢ ( 𝑥 = ( 𝑖 + 1 ) → ( ( 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥 ) ↔ ( 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ ( 𝑖 + 1 ) ) ) )
321 eqvisset ⊢ ( 𝑥 = ( 𝑖 + 1 ) → ( 𝑖 + 1 ) ∈ V )
322 eqtr3 ⊢ ( ( 𝑥 = ( 𝑖 + 1 ) ∧ 𝑛 = ( 𝑖 + 1 ) ) → 𝑥 = 𝑛 )
323 9 equcoms ⊢ ( 𝑥 = 𝑛 → 𝐴 = 𝐵 )
324 322 323 syl ⊢ ( ( 𝑥 = ( 𝑖 + 1 ) ∧ 𝑛 = ( 𝑖 + 1 ) ) → 𝐴 = 𝐵 )
325 321 324 csbied ⊢ ( 𝑥 = ( 𝑖 + 1 ) → ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 = 𝐵 )
326 325 eqcomd ⊢ ( 𝑥 = ( 𝑖 + 1 ) → 𝐵 = ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 )
327 326 breq1d ⊢ ( 𝑥 = ( 𝑖 + 1 ) → ( 𝐵 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ↔ ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
328 320 327 imbi12d ⊢ ( 𝑥 = ( 𝑖 + 1 ) → ( ( ( 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ↔ ( ( 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ ( 𝑖 + 1 ) ) → ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) )
329 328 rspcv ⊢ ( ( 𝑖 + 1 ) ∈ ℝ+ → ( ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) → ( ( 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ ( 𝑖 + 1 ) ) → ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) )
330 297 316 318 329 syl3c ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 )
331 294 330 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 )
332 221 220 331 abssuble0d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( abs ‘ ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) = ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) )
333 332 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( ( abs ‘ ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) · ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) = ( ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) · ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) )
334 291 333 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( abs ‘ ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) = ( ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) · ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) )
335 290 abscld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ∈ ℝ )
336 220 221 subge0d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( 0 ≤ ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) ↔ ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ≤ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
337 331 336 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → 0 ≤ ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) )
338 138 peano2nnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℕ )
339 338 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℕ0 )
340 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 dchrisumlem1 ⊢ ( ( 𝜑 ∧ ( 𝑖 + 1 ) ∈ ℕ0 ) → ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
341 339 340 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
342 335 287 222 337 341 lemul2ad ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) · ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ≤ ( ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) )
343 334 342 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( abs ‘ ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ≤ ( ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) )
344 86 284 288 343 fsumle ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( abs ‘ ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ≤ Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) )
345 222 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ) → ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) ∈ ℂ )
346 86 280 345 fsummulc1 ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) = Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) )
347 219 oveq1d ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) = ( ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) )
348 346 347 eqtr3d ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( ⦋ 𝑖 / 𝑛 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) = ( ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) )
349 344 348 breqtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( abs ‘ ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ≤ ( ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) )
350 159 285 225 286 349 letrd ⊢ ( 𝜑 → ( abs ‘ Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ≤ ( ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) )
351 137 159 218 225 283 350 le2addd ⊢ ( 𝜑 → ( ( abs ‘ ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) − ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ) + ( abs ‘ Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ) ≤ ( ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) + ( ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) ) )
352 129 2timesd ⊢ ( 𝜑 → ( 2 · ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) = ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) )
353 129 119 129 ppncand ⊢ ( 𝜑 → ( ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) + ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) ) = ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) )
354 129 119 addcomd ⊢ ( 𝜑 → ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) = ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) )
355 354 oveq1d ⊢ ( 𝜑 → ( ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) + ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) ) = ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) + ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) ) )
356 352 353 355 3eqtr2d ⊢ ( 𝜑 → ( 2 · ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) = ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) + ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) ) )
357 356 oveq1d ⊢ ( 𝜑 → ( ( 2 · ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) = ( ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) + ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) ) · 𝑅 ) )
358 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
359 358 129 280 mul32d ⊢ ( 𝜑 → ( ( 2 · ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) = ( ( 2 · 𝑅 ) · ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) )
360 217 recnd ⊢ ( 𝜑 → ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) ∈ ℂ )
361 224 recnd ⊢ ( 𝜑 → ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) ∈ ℂ )
362 360 361 280 adddird ⊢ ( 𝜑 → ( ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) + ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) ) · 𝑅 ) = ( ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) + ( ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) ) )
363 357 359 362 3eqtr3d ⊢ ( 𝜑 → ( ( 2 · 𝑅 ) · ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) = ( ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 + ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) + ( ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 ) · 𝑅 ) ) )
364 351 363 breqtrrd ⊢ ( 𝜑 → ( ( abs ‘ ( ( ⦋ ( 𝐽 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) − ( ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 · Σ 𝑛 ∈ ( 0 ..^ ( 𝐼 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ) + ( abs ‘ Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( ⦋ ( 𝑖 + 1 ) / 𝑛 ⦌ 𝐴 − ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) · Σ 𝑛 ∈ ( 0 ..^ ( 𝑖 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) )
365 95 160 104 216 364 letrd ⊢ ( 𝜑 → ( abs ‘ Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) )
366 2nn0 ⊢ 2 ∈ ℕ0
367 nn0ge0 ⊢ ( 2 ∈ ℕ0 → 0 ≤ 2 )
368 366 367 mp1i ⊢ ( 𝜑 → 0 ≤ 2 )
369 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
370 127 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
371 369 259 15 370 262 letrd ⊢ ( 𝜑 → 0 ≤ 𝑅 )
372 97 15 368 371 mulge0d ⊢ ( 𝜑 → 0 ≤ ( 2 · 𝑅 ) )
373 24 nnrpd ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ℝ+ )
374 nfv ⊢ Ⅎ 𝑛 ( 𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥 )
375 304 305 106 nfbr ⊢ Ⅎ 𝑛 𝐵 ≤ ⦋ 𝑈 / 𝑛 ⦌ 𝐴
376 374 375 nfim ⊢ Ⅎ 𝑛 ( ( 𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝑈 / 𝑛 ⦌ 𝐴 )
377 302 376 nfralw ⊢ Ⅎ 𝑛 ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝑈 / 𝑛 ⦌ 𝐴 )
378 breq2 ⊢ ( 𝑛 = 𝑈 → ( 𝑀 ≤ 𝑛 ↔ 𝑀 ≤ 𝑈 ) )
379 breq1 ⊢ ( 𝑛 = 𝑈 → ( 𝑛 ≤ 𝑥 ↔ 𝑈 ≤ 𝑥 ) )
380 378 379 anbi12d ⊢ ( 𝑛 = 𝑈 → ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ↔ ( 𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥 ) ) )
381 108 breq2d ⊢ ( 𝑛 = 𝑈 → ( 𝐵 ≤ 𝐴 ↔ 𝐵 ≤ ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ) )
382 380 381 imbi12d ⊢ ( 𝑛 = 𝑈 → ( ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) → 𝐵 ≤ 𝐴 ) ↔ ( ( 𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ) ) )
383 382 ralbidv ⊢ ( 𝑛 = 𝑈 → ( ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) → 𝐵 ≤ 𝐴 ) ↔ ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ) ) )
384 377 383 rspc ⊢ ( 𝑈 ∈ ℝ+ → ( ∀ 𝑛 ∈ ℝ+ ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) → 𝐵 ≤ 𝐴 ) → ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ) ) )
385 17 300 384 sylc ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ) )
386 18 19 jca ⊢ ( 𝜑 → ( 𝑀 ≤ 𝑈 ∧ 𝑈 ≤ ( 𝐼 + 1 ) ) )
387 breq2 ⊢ ( 𝑥 = ( 𝐼 + 1 ) → ( 𝑈 ≤ 𝑥 ↔ 𝑈 ≤ ( 𝐼 + 1 ) ) )
388 387 anbi2d ⊢ ( 𝑥 = ( 𝐼 + 1 ) → ( ( 𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥 ) ↔ ( 𝑀 ≤ 𝑈 ∧ 𝑈 ≤ ( 𝐼 + 1 ) ) ) )
389 eqvisset ⊢ ( 𝑥 = ( 𝐼 + 1 ) → ( 𝐼 + 1 ) ∈ V )
390 eqtr3 ⊢ ( ( 𝑥 = ( 𝐼 + 1 ) ∧ 𝑛 = ( 𝐼 + 1 ) ) → 𝑥 = 𝑛 )
391 390 323 syl ⊢ ( ( 𝑥 = ( 𝐼 + 1 ) ∧ 𝑛 = ( 𝐼 + 1 ) ) → 𝐴 = 𝐵 )
392 389 391 csbied ⊢ ( 𝑥 = ( 𝐼 + 1 ) → ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 = 𝐵 )
393 392 eqcomd ⊢ ( 𝑥 = ( 𝐼 + 1 ) → 𝐵 = ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 )
394 393 breq1d ⊢ ( 𝑥 = ( 𝐼 + 1 ) → ( 𝐵 ≤ ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ↔ ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ≤ ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ) )
395 388 394 imbi12d ⊢ ( 𝑥 = ( 𝐼 + 1 ) → ( ( ( 𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ) ↔ ( ( 𝑀 ≤ 𝑈 ∧ 𝑈 ≤ ( 𝐼 + 1 ) ) → ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ≤ ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ) ) )
396 395 rspcv ⊢ ( ( 𝐼 + 1 ) ∈ ℝ+ → ( ∀ 𝑥 ∈ ℝ+ ( ( 𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥 ) → 𝐵 ≤ ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ) → ( ( 𝑀 ≤ 𝑈 ∧ 𝑈 ≤ ( 𝐼 + 1 ) ) → ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ≤ ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ) ) )
397 373 385 386 396 syl3c ⊢ ( 𝜑 → ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ≤ ⦋ 𝑈 / 𝑛 ⦌ 𝐴 )
398 103 111 98 372 397 lemul2ad ⊢ ( 𝜑 → ( ( 2 · 𝑅 ) · ⦋ ( 𝐼 + 1 ) / 𝑛 ⦌ 𝐴 ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ) )
399 95 104 112 365 398 letrd ⊢ ( 𝜑 → ( abs ‘ Σ 𝑖 ∈ ( ( 𝐼 + 1 ) ..^ ( 𝐽 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ) )
400 94 399 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝐽 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝐼 ) ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑈 / 𝑛 ⦌ 𝐴 ) )