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