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 · 𝑅 ) · 𝑈 / 𝑛 𝐴 ) )