dchrisumlem2 - Metamath Proof Explorer

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

Theorem dchrisumlem2 25179

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

**Hypotheses**
Ref	Expression
rpvmasum.z	⊢ 𝑍 = (ℤ/nℤ‘𝑁)
rpvmasum.l	⊢ 𝐿 = (ℤRHom‘𝑍)
rpvmasum.a	⊢ (𝜑 → 𝑁 ∈ ℕ)
rpvmasum.g	⊢ 𝐺 = (DChr‘𝑁)
rpvmasum.d	⊢ 𝐷 = (Base‘𝐺)
rpvmasum.1	⊢ 1 = (0_g‘𝐺)
dchrisum.b	⊢ (𝜑 → 𝑋 ∈ 𝐷)
dchrisum.n1	⊢ (𝜑 → 𝑋 ≠ 1 )
dchrisum.2	⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵)
dchrisum.3	⊢ (𝜑 → 𝑀 ∈ ℕ)
dchrisum.4	⊢ ((𝜑 ∧ 𝑛 ∈ ℝ⁺) → 𝐴 ∈ ℝ)
dchrisum.5	⊢ ((𝜑 ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)
dchrisum.6	⊢ (𝜑 → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝_𝑟 0)
dchrisum.7	⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴))
dchrisum.9	⊢ (𝜑 → 𝑅 ∈ ℝ)
dchrisum.10	⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅)
dchrisumlem2.1	⊢ (𝜑 → 𝑈 ∈ ℝ⁺)
dchrisumlem2.2	⊢ (𝜑 → 𝑀 ≤ 𝑈)
dchrisumlem2.3	⊢ (𝜑 → 𝑈 ≤ (𝐼 + 1))
dchrisumlem2.4	⊢ (𝜑 → 𝐼 ∈ ℕ)
dchrisumlem2.5	⊢ (𝜑 → 𝐽 ∈ (ℤ_≥‘𝐼))

**Assertion**
Ref	Expression
dchrisumlem2	⊢ (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) ≤ ((2 · 𝑅) · ⦋𝑈 / 𝑛⦌𝐴))

Distinct variable groups: 𝑢,𝑛,𝑥 1 ,𝑛,𝑥 𝑛,𝐹,𝑢,𝑥 𝑛,𝐼,𝑢,𝑥 𝑛,𝐽,𝑢,𝑥 𝑥,𝐴 𝑛,𝑁,𝑢,𝑥 𝜑,𝑛,𝑢,𝑥 𝑅,𝑛,𝑢,𝑥 𝑈,𝑛,𝑢,𝑥 𝐵,𝑛 𝑛,𝑍,𝑥 𝐷,𝑛,𝑥 𝑛,𝐿,𝑢,𝑥 𝑛,𝑀,𝑢,𝑥 𝑛,𝑋,𝑢,𝑥 Allowed substitution hints: 𝐴(𝑢,𝑛) 𝐵(𝑥,𝑢) 𝐷(𝑢) 1 (𝑢) 𝐺(𝑥,𝑢,𝑛) 𝑍(𝑢)

Proof of Theorem dchrisumlem2 Dummy variables 𝑘 𝑖 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzodisj 12502	. . . . . . . . 9 ⊢ ((1..^(𝐼 + 1)) ∩ ((𝐼 + 1)..^(𝐽 + 1))) = ∅
2	1	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((1..^(𝐼 + 1)) ∩ ((𝐼 + 1)..^(𝐽 + 1))) = ∅)
3		dchrisumlem2.4	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ ℕ)
4	3	peano2nnd 11037	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐼 + 1) ∈ ℕ)
5		nnuz 11723	. . . . . . . . . . 11 ⊢ ℕ = (ℤ_≥‘1)
6	4, 5	syl6eleq 2711	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼 + 1) ∈ (ℤ_≥‘1))
7		dchrisumlem2.5	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ (ℤ_≥‘𝐼))
8		eluzp1p1 11713	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (ℤ_≥‘𝐼) → (𝐽 + 1) ∈ (ℤ_≥‘(𝐼 + 1)))
9	7, 8	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽 + 1) ∈ (ℤ_≥‘(𝐼 + 1)))
10		elfzuzb 12336	. . . . . . . . . 10 ⊢ ((𝐼 + 1) ∈ (1...(𝐽 + 1)) ↔ ((𝐼 + 1) ∈ (ℤ_≥‘1) ∧ (𝐽 + 1) ∈ (ℤ_≥‘(𝐼 + 1))))
11	6, 9, 10	sylanbrc 698	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 + 1) ∈ (1...(𝐽 + 1)))
12		fzosplit 12501	. . . . . . . . 9 ⊢ ((𝐼 + 1) ∈ (1...(𝐽 + 1)) → (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1))))
13	11, 12	syl 17	. . . . . . . 8 ⊢ (𝜑 → (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1))))
14		fzofi 12773	. . . . . . . . 9 ⊢ (1..^(𝐽 + 1)) ∈ Fin
15	14	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (1..^(𝐽 + 1)) ∈ Fin)
16		elfzouz 12474	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1..^(𝐽 + 1)) → 𝑖 ∈ (ℤ_≥‘1))
17	16, 5	syl6eleqr 2712	. . . . . . . . 9 ⊢ (𝑖 ∈ (1..^(𝐽 + 1)) → 𝑖 ∈ ℕ)
18		rpvmasum.g	. . . . . . . . . . 11 ⊢ 𝐺 = (DChr‘𝑁)
19		rpvmasum.z	. . . . . . . . . . 11 ⊢ 𝑍 = (ℤ/nℤ‘𝑁)
20		rpvmasum.d	. . . . . . . . . . 11 ⊢ 𝐷 = (Base‘𝐺)
21		rpvmasum.l	. . . . . . . . . . 11 ⊢ 𝐿 = (ℤRHom‘𝑍)
22		dchrisum.b	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ 𝐷)
23	22	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑋 ∈ 𝐷)
24		nnz 11399	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ ℕ → 𝑖 ∈ ℤ)
25	24	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℤ)
26	18, 19, 20, 21, 23, 25	dchrzrhcl 24970	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑋‘(𝐿‘𝑖)) ∈ ℂ)
27		nnrp 11842	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ℕ → 𝑖 ∈ ℝ⁺)
28		rpvmasum.a	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℕ)
29		rpvmasum.1	. . . . . . . . . . . . . . 15 ⊢ 1 = (0_g‘𝐺)
30		dchrisum.n1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ≠ 1 )
31		dchrisum.2	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵)
32		dchrisum.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℕ)
33		dchrisum.4	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ⁺) → 𝐴 ∈ ℝ)
34		dchrisum.5	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)
35		dchrisum.6	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑛 ∈ ℝ⁺ ↦ 𝐴) ⇝_𝑟 0)
36		dchrisum.7	. . . . . . . . . . . . . . 15 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴))
37	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36	dchrisumlema 25177	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑖 ∈ ℝ⁺ → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ) ∧ (𝑖 ∈ (𝑀[,)+∞) → 0 ≤ ⦋𝑖 / 𝑛⦌𝐴)))
38	37	simpld 475	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑖 ∈ ℝ⁺ → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ))
39	27, 38	syl5 34	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑖 ∈ ℕ → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ))
40	39	imp 445	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ)
41	40	recnd 10068	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℂ)
42	26, 41	mulcld 10060	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ)
43	17, 42	sylan2 491	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1..^(𝐽 + 1))) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ)
44	2, 13, 15, 43	fsumsplit 14471	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ (1..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)))
45		eluzelz 11697	. . . . . . . . 9 ⊢ (𝐽 ∈ (ℤ_≥‘𝐼) → 𝐽 ∈ ℤ)
46		fzval3 12536	. . . . . . . . 9 ⊢ (𝐽 ∈ ℤ → (1...𝐽) = (1..^(𝐽 + 1)))
47	7, 45, 46	3syl 18	. . . . . . . 8 ⊢ (𝜑 → (1...𝐽) = (1..^(𝐽 + 1)))
48	47	sumeq1d 14431	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = Σ𝑖 ∈ (1..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴))
49	3	nnzd 11481	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ ℤ)
50		fzval3 12536	. . . . . . . . . 10 ⊢ (𝐼 ∈ ℤ → (1...𝐼) = (1..^(𝐼 + 1)))
51	49, 50	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (1...𝐼) = (1..^(𝐼 + 1)))
52	51	sumeq1d 14431	. . . . . . . 8 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴))
53	52	oveq1d 6665	. . . . . . 7 ⊢ (𝜑 → (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)))
54	44, 48, 53	3eqtr4d 2666	. . . . . 6 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)))
55		elfznn 12370	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝐽) → 𝑖 ∈ ℕ)
56		simpr 477	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
57		nfcv 2764	. . . . . . . . . 10 ⊢ Ⅎ𝑛𝑖
58		nfcv 2764	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝑋‘(𝐿‘𝑖))
59		nfcv 2764	. . . . . . . . . . 11 ⊢ Ⅎ𝑛 ·
60		nfcsb1v 3549	. . . . . . . . . . 11 ⊢ Ⅎ𝑛⦋𝑖 / 𝑛⦌𝐴
61	58, 59, 60	nfov 6676	. . . . . . . . . 10 ⊢ Ⅎ𝑛((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)
62		fveq2 6191	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑖 → (𝐿‘𝑛) = (𝐿‘𝑖))
63	62	fveq2d 6195	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑖 → (𝑋‘(𝐿‘𝑛)) = (𝑋‘(𝐿‘𝑖)))
64		csbeq1a 3542	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑖 → 𝐴 = ⦋𝑖 / 𝑛⦌𝐴)
65	63, 64	oveq12d 6668	. . . . . . . . . 10 ⊢ (𝑛 = 𝑖 → ((𝑋‘(𝐿‘𝑛)) · 𝐴) = ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴))
66	57, 61, 65, 36	fvmptf 6301	. . . . . . . . 9 ⊢ ((𝑖 ∈ ℕ ∧ ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ) → (𝐹‘𝑖) = ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴))
67	56, 42, 66	syl2anc 693	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) = ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴))
68	55, 67	sylan2 491	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝐽)) → (𝐹‘𝑖) = ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴))
69	3, 5	syl6eleq 2711	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ (ℤ_≥‘1))
70		uztrn 11704	. . . . . . . 8 ⊢ ((𝐽 ∈ (ℤ_≥‘𝐼) ∧ 𝐼 ∈ (ℤ_≥‘1)) → 𝐽 ∈ (ℤ_≥‘1))
71	7, 69, 70	syl2anc 693	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ (ℤ_≥‘1))
72	55, 42	sylan2 491	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝐽)) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ)
73	68, 71, 72	fsumser 14461	. . . . . 6 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝐽)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = (seq1( + , 𝐹)‘𝐽))
74	54, 73	eqtr3d 2658	. . . . 5 ⊢ (𝜑 → (Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) = (seq1( + , 𝐹)‘𝐽))
75		elfznn 12370	. . . . . . 7 ⊢ (𝑖 ∈ (1...𝐼) → 𝑖 ∈ ℕ)
76	75, 67	sylan2 491	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝐼)) → (𝐹‘𝑖) = ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴))
77	75, 42	sylan2 491	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝐼)) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ)
78	76, 69, 77	fsumser 14461	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = (seq1( + , 𝐹)‘𝐼))
79	74, 78	oveq12d 6668	. . . 4 ⊢ (𝜑 → ((Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) − Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) = ((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼)))
80		fzfid 12772	. . . . . 6 ⊢ (𝜑 → (1...𝐼) ∈ Fin)
81	80, 77	fsumcl 14464	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ)
82		fzofi 12773	. . . . . . 7 ⊢ ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin
83	82	a1i 11	. . . . . 6 ⊢ (𝜑 → ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin)
84		ssun2 3777	. . . . . . . . 9 ⊢ ((𝐼 + 1)..^(𝐽 + 1)) ⊆ ((1..^(𝐼 + 1)) ∪ ((𝐼 + 1)..^(𝐽 + 1)))
85	84, 13	syl5sseqr 3654	. . . . . . . 8 ⊢ (𝜑 → ((𝐼 + 1)..^(𝐽 + 1)) ⊆ (1..^(𝐽 + 1)))
86	85	sselda 3603	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ (1..^(𝐽 + 1)))
87	86, 43	syldan 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ)
88	83, 87	fsumcl 14464	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ)
89	81, 88	pncan2d 10394	. . . 4 ⊢ (𝜑 → ((Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) − Σ𝑖 ∈ (1...𝐼)((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴))
90	79, 89	eqtr3d 2658	. . 3 ⊢ (𝜑 → ((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴))
91	90	fveq2d 6195	. 2 ⊢ (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) = (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)))
92	88	abscld 14175	. . 3 ⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) ∈ ℝ)
93		2re 11090	. . . . . 6 ⊢ 2 ∈ ℝ
94	93	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ∈ ℝ)
95		dchrisum.9	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ ℝ)
96	94, 95	remulcld 10070	. . . 4 ⊢ (𝜑 → (2 · 𝑅) ∈ ℝ)
97	40	ralrimiva 2966	. . . . 5 ⊢ (𝜑 → ∀𝑖 ∈ ℕ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ)
98		csbeq1 3536	. . . . . . 7 ⊢ (𝑖 = (𝐼 + 1) → ⦋𝑖 / 𝑛⦌𝐴 = ⦋(𝐼 + 1) / 𝑛⦌𝐴)
99	98	eleq1d 2686	. . . . . 6 ⊢ (𝑖 = (𝐼 + 1) → (⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ ↔ ⦋(𝐼 + 1) / 𝑛⦌𝐴 ∈ ℝ))
100	99	rspcv 3305	. . . . 5 ⊢ ((𝐼 + 1) ∈ ℕ → (∀𝑖 ∈ ℕ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ → ⦋(𝐼 + 1) / 𝑛⦌𝐴 ∈ ℝ))
101	4, 97, 100	sylc 65	. . . 4 ⊢ (𝜑 → ⦋(𝐼 + 1) / 𝑛⦌𝐴 ∈ ℝ)
102	96, 101	remulcld 10070	. . 3 ⊢ (𝜑 → ((2 · 𝑅) · ⦋(𝐼 + 1) / 𝑛⦌𝐴) ∈ ℝ)
103		dchrisumlem2.1	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ ℝ⁺)
104	33	ralrimiva 2966	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ)
105		nfcsb1v 3549	. . . . . . 7 ⊢ Ⅎ𝑛⦋𝑈 / 𝑛⦌𝐴
106	105	nfel1 2779	. . . . . 6 ⊢ Ⅎ𝑛⦋𝑈 / 𝑛⦌𝐴 ∈ ℝ
107		csbeq1a 3542	. . . . . . 7 ⊢ (𝑛 = 𝑈 → 𝐴 = ⦋𝑈 / 𝑛⦌𝐴)
108	107	eleq1d 2686	. . . . . 6 ⊢ (𝑛 = 𝑈 → (𝐴 ∈ ℝ ↔ ⦋𝑈 / 𝑛⦌𝐴 ∈ ℝ))
109	106, 108	rspc 3303	. . . . 5 ⊢ (𝑈 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ → ⦋𝑈 / 𝑛⦌𝐴 ∈ ℝ))
110	103, 104, 109	sylc 65	. . . 4 ⊢ (𝜑 → ⦋𝑈 / 𝑛⦌𝐴 ∈ ℝ)
111	96, 110	remulcld 10070	. . 3 ⊢ (𝜑 → ((2 · 𝑅) · ⦋𝑈 / 𝑛⦌𝐴) ∈ ℝ)
112	71, 5	syl6eleqr 2712	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ ℕ)
113	112	peano2nnd 11037	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽 + 1) ∈ ℕ)
114	113	nnrpd 11870	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽 + 1) ∈ ℝ⁺)
115	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36	dchrisumlema 25177	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐽 + 1) ∈ ℝ⁺ → ⦋(𝐽 + 1) / 𝑛⦌𝐴 ∈ ℝ) ∧ ((𝐽 + 1) ∈ (𝑀[,)+∞) → 0 ≤ ⦋(𝐽 + 1) / 𝑛⦌𝐴)))
116	115	simpld 475	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐽 + 1) ∈ ℝ⁺ → ⦋(𝐽 + 1) / 𝑛⦌𝐴 ∈ ℝ))
117	114, 116	mpd 15	. . . . . . . . 9 ⊢ (𝜑 → ⦋(𝐽 + 1) / 𝑛⦌𝐴 ∈ ℝ)
118	117	recnd 10068	. . . . . . . 8 ⊢ (𝜑 → ⦋(𝐽 + 1) / 𝑛⦌𝐴 ∈ ℂ)
119		fzofi 12773	. . . . . . . . . 10 ⊢ (0..^(𝐽 + 1)) ∈ Fin
120	119	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (0..^(𝐽 + 1)) ∈ Fin)
121		elfzoelz 12470	. . . . . . . . . 10 ⊢ (𝑛 ∈ (0..^(𝐽 + 1)) → 𝑛 ∈ ℤ)
122	22	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℤ) → 𝑋 ∈ 𝐷)
123		simpr 477	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℤ) → 𝑛 ∈ ℤ)
124	18, 19, 20, 21, 122, 123	dchrzrhcl 24970	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℤ) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ)
125	121, 124	sylan2 491	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^(𝐽 + 1))) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ)
126	120, 125	fsumcl 14464	. . . . . . . 8 ⊢ (𝜑 → Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)) ∈ ℂ)
127	118, 126	mulcld 10060	. . . . . . 7 ⊢ (𝜑 → (⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) ∈ ℂ)
128	101	recnd 10068	. . . . . . . 8 ⊢ (𝜑 → ⦋(𝐼 + 1) / 𝑛⦌𝐴 ∈ ℂ)
129		fzofi 12773	. . . . . . . . . 10 ⊢ (0..^(𝐼 + 1)) ∈ Fin
130	129	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (0..^(𝐼 + 1)) ∈ Fin)
131		elfzoelz 12470	. . . . . . . . . 10 ⊢ (𝑛 ∈ (0..^(𝐼 + 1)) → 𝑛 ∈ ℤ)
132	131, 124	sylan2 491	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^(𝐼 + 1))) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ)
133	130, 132	fsumcl 14464	. . . . . . . 8 ⊢ (𝜑 → Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)) ∈ ℂ)
134	128, 133	mulcld 10060	. . . . . . 7 ⊢ (𝜑 → (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))) ∈ ℂ)
135	127, 134	subcld 10392	. . . . . 6 ⊢ (𝜑 → ((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) ∈ ℂ)
136	135	abscld 14175	. . . . 5 ⊢ (𝜑 → (abs‘((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) ∈ ℝ)
137	86, 17	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ ℕ)
138		peano2nn 11032	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℕ)
139	138	nnrpd 11870	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℝ⁺)
140		nfcsb1v 3549	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛⦋(𝑖 + 1) / 𝑛⦌𝐴
141	140	nfel1 2779	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛⦋(𝑖 + 1) / 𝑛⦌𝐴 ∈ ℝ
142		csbeq1a 3542	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (𝑖 + 1) → 𝐴 = ⦋(𝑖 + 1) / 𝑛⦌𝐴)
143	142	eleq1d 2686	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑖 + 1) → (𝐴 ∈ ℝ ↔ ⦋(𝑖 + 1) / 𝑛⦌𝐴 ∈ ℝ))
144	141, 143	rspc 3303	. . . . . . . . . . . . 13 ⊢ ((𝑖 + 1) ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ → ⦋(𝑖 + 1) / 𝑛⦌𝐴 ∈ ℝ))
145	144	impcom 446	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ ℝ⁺ 𝐴 ∈ ℝ ∧ (𝑖 + 1) ∈ ℝ⁺) → ⦋(𝑖 + 1) / 𝑛⦌𝐴 ∈ ℝ)
146	104, 139, 145	syl2an 494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ⦋(𝑖 + 1) / 𝑛⦌𝐴 ∈ ℝ)
147	146, 40	resubcld 10458	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) ∈ ℝ)
148	147	recnd 10068	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ)
149		fzofi 12773	. . . . . . . . . . . 12 ⊢ (0..^(𝑖 + 1)) ∈ Fin
150	149	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (0..^(𝑖 + 1)) ∈ Fin)
151		elfzoelz 12470	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (0..^(𝑖 + 1)) → 𝑛 ∈ ℤ)
152	151, 124	sylan2 491	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^(𝑖 + 1))) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ)
153	150, 152	fsumcl 14464	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) ∈ ℂ)
154	153	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) ∈ ℂ)
155	148, 154	mulcld 10060	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))) ∈ ℂ)
156	137, 155	syldan 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))) ∈ ℂ)
157	83, 156	fsumcl 14464	. . . . . 6 ⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))) ∈ ℂ)
158	157	abscld 14175	. . . . 5 ⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ∈ ℝ)
159	136, 158	readdcld 10069	. . . 4 ⊢ (𝜑 → ((abs‘((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))) ∈ ℝ)
160	26, 41	mulcomd 10061	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = (⦋𝑖 / 𝑛⦌𝐴 · (𝑋‘(𝐿‘𝑖))))
161		nnnn0 11299	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ ℕ → 𝑖 ∈ ℕ₀)
162	161	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ₀)
163		nn0uz 11722	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (ℤ_≥‘0)
164	162, 163	syl6eleq 2711	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ (ℤ_≥‘0))
165		elfzelz 12342	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (0...𝑖) → 𝑛 ∈ ℤ)
166	124	adantlr 751	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ)
167	165, 166	sylan2 491	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑛 ∈ (0...𝑖)) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ)
168	164, 167, 63	fzosump1 14481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) = (Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)) + (𝑋‘(𝐿‘𝑖))))
169	168	oveq1d 6665	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))) = ((Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)) + (𝑋‘(𝐿‘𝑖))) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))))
170		fzofi 12773	. . . . . . . . . . . . . . 15 ⊢ (0..^𝑖) ∈ Fin
171	170	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (0..^𝑖) ∈ Fin)
172		elfzoelz 12470	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (0..^𝑖) → 𝑛 ∈ ℤ)
173	172, 166	sylan2 491	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑛 ∈ (0..^𝑖)) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ)
174	171, 173	fsumcl 14464	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)) ∈ ℂ)
175	174, 26	pncan2d 10394	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)) + (𝑋‘(𝐿‘𝑖))) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))) = (𝑋‘(𝐿‘𝑖)))
176	169, 175	eqtr2d 2657	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑋‘(𝐿‘𝑖)) = (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))))
177	176	oveq2d 6666	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (⦋𝑖 / 𝑛⦌𝐴 · (𝑋‘(𝐿‘𝑖))) = (⦋𝑖 / 𝑛⦌𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)))))
178	160, 177	eqtrd 2656	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = (⦋𝑖 / 𝑛⦌𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)))))
179	137, 178	syldan 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = (⦋𝑖 / 𝑛⦌𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)))))
180	179	sumeq2dv 14433	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / 𝑛⦌𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)))))
181		csbeq1 3536	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → ⦋𝑘 / 𝑛⦌𝐴 = ⦋𝑖 / 𝑛⦌𝐴)
182		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → (0..^𝑘) = (0..^𝑖))
183	182	sumeq1d 14431	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)))
184	181, 183	jca 554	. . . . . . . 8 ⊢ (𝑘 = 𝑖 → (⦋𝑘 / 𝑛⦌𝐴 = ⦋𝑖 / 𝑛⦌𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛))))
185		csbeq1 3536	. . . . . . . . 9 ⊢ (𝑘 = (𝑖 + 1) → ⦋𝑘 / 𝑛⦌𝐴 = ⦋(𝑖 + 1) / 𝑛⦌𝐴)
186		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑘 = (𝑖 + 1) → (0..^𝑘) = (0..^(𝑖 + 1)))
187	186	sumeq1d 14431	. . . . . . . . 9 ⊢ (𝑘 = (𝑖 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))
188	185, 187	jca 554	. . . . . . . 8 ⊢ (𝑘 = (𝑖 + 1) → (⦋𝑘 / 𝑛⦌𝐴 = ⦋(𝑖 + 1) / 𝑛⦌𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))
189		csbeq1 3536	. . . . . . . . 9 ⊢ (𝑘 = (𝐼 + 1) → ⦋𝑘 / 𝑛⦌𝐴 = ⦋(𝐼 + 1) / 𝑛⦌𝐴)
190		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑘 = (𝐼 + 1) → (0..^𝑘) = (0..^(𝐼 + 1)))
191	190	sumeq1d 14431	. . . . . . . . 9 ⊢ (𝑘 = (𝐼 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))
192	189, 191	jca 554	. . . . . . . 8 ⊢ (𝑘 = (𝐼 + 1) → (⦋𝑘 / 𝑛⦌𝐴 = ⦋(𝐼 + 1) / 𝑛⦌𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))
193		csbeq1 3536	. . . . . . . . 9 ⊢ (𝑘 = (𝐽 + 1) → ⦋𝑘 / 𝑛⦌𝐴 = ⦋(𝐽 + 1) / 𝑛⦌𝐴)
194		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑘 = (𝐽 + 1) → (0..^𝑘) = (0..^(𝐽 + 1)))
195	194	sumeq1d 14431	. . . . . . . . 9 ⊢ (𝑘 = (𝐽 + 1) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))
196	193, 195	jca 554	. . . . . . . 8 ⊢ (𝑘 = (𝐽 + 1) → (⦋𝑘 / 𝑛⦌𝐴 = ⦋(𝐽 + 1) / 𝑛⦌𝐴 ∧ Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))))
197		elfzuz 12338	. . . . . . . . . 10 ⊢ (𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1)) → 𝑘 ∈ (ℤ_≥‘(𝐼 + 1)))
198		eluznn 11758	. . . . . . . . . 10 ⊢ (((𝐼 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘(𝐼 + 1))) → 𝑘 ∈ ℕ)
199	4, 197, 198	syl2an 494	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → 𝑘 ∈ ℕ)
200	41	ralrimiva 2966	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑖 ∈ ℕ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℂ)
201		csbeq1 3536	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → ⦋𝑖 / 𝑛⦌𝐴 = ⦋𝑘 / 𝑛⦌𝐴)
202	201	eleq1d 2686	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑘 → (⦋𝑖 / 𝑛⦌𝐴 ∈ ℂ ↔ ⦋𝑘 / 𝑛⦌𝐴 ∈ ℂ))
203	202	rspccva 3308	. . . . . . . . . 10 ⊢ ((∀𝑖 ∈ ℕ ⦋𝑖 / 𝑛⦌𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) → ⦋𝑘 / 𝑛⦌𝐴 ∈ ℂ)
204	200, 203	sylan 488	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ⦋𝑘 / 𝑛⦌𝐴 ∈ ℂ)
205	199, 204	syldan 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → ⦋𝑘 / 𝑛⦌𝐴 ∈ ℂ)
206		fzofi 12773	. . . . . . . . . . 11 ⊢ (0..^𝑘) ∈ Fin
207	206	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (0..^𝑘) ∈ Fin)
208		elfzoelz 12470	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (0..^𝑘) → 𝑛 ∈ ℤ)
209	208, 124	sylan2 491	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑘)) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ)
210	207, 209	fsumcl 14464	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) ∈ ℂ)
211	210	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 + 1))) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) ∈ ℂ)
212	184, 188, 192, 196, 9, 205, 211	fsumparts 14538	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / 𝑛⦌𝐴 · (Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) − Σ𝑛 ∈ (0..^𝑖)(𝑋‘(𝐿‘𝑛)))) = (((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))))
213	180, 212	eqtrd 2656	. . . . . 6 ⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴) = (((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))))
214	213	fveq2d 6195	. . . . 5 ⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) = (abs‘(((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))))
215	135, 157	abs2dif2d 14197	. . . . 5 ⊢ (𝜑 → (abs‘(((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) − Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))) ≤ ((abs‘((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))))
216	214, 215	eqbrtrd 4675	. . . 4 ⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) ≤ ((abs‘((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))))
217	117, 101	readdcld 10069	. . . . . . 7 ⊢ (𝜑 → (⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) ∈ ℝ)
218	217, 95	remulcld 10070	. . . . . 6 ⊢ (𝜑 → ((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) · 𝑅) ∈ ℝ)
219	181, 185, 189, 193, 9, 205	telfsumo 14534	. . . . . . . 8 ⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) = (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴))
220	137, 40	syldan 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ⦋𝑖 / 𝑛⦌𝐴 ∈ ℝ)
221	137, 146	syldan 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ⦋(𝑖 + 1) / 𝑛⦌𝐴 ∈ ℝ)
222	220, 221	resubcld 10458	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) ∈ ℝ)
223	83, 222	fsumrecl 14465	. . . . . . . 8 ⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) ∈ ℝ)
224	219, 223	eqeltrrd 2702	. . . . . . 7 ⊢ (𝜑 → (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) ∈ ℝ)
225	224, 95	remulcld 10070	. . . . . 6 ⊢ (𝜑 → ((⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) · 𝑅) ∈ ℝ)
226	127	abscld 14175	. . . . . . . 8 ⊢ (𝜑 → (abs‘(⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) ∈ ℝ)
227	134	abscld 14175	. . . . . . . 8 ⊢ (𝜑 → (abs‘(⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) ∈ ℝ)
228	226, 227	readdcld 10069	. . . . . . 7 ⊢ (𝜑 → ((abs‘(⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) + (abs‘(⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) ∈ ℝ)
229	127, 134	abs2dif2d 14197	. . . . . . 7 ⊢ (𝜑 → (abs‘((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) ≤ ((abs‘(⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) + (abs‘(⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))))
230	117, 95	remulcld 10070	. . . . . . . . 9 ⊢ (𝜑 → (⦋(𝐽 + 1) / 𝑛⦌𝐴 · 𝑅) ∈ ℝ)
231	101, 95	remulcld 10070	. . . . . . . . 9 ⊢ (𝜑 → (⦋(𝐼 + 1) / 𝑛⦌𝐴 · 𝑅) ∈ ℝ)
232	118, 126	absmuld 14193	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) = ((abs‘⦋(𝐽 + 1) / 𝑛⦌𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))))
233		eluzelre 11698	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (ℤ_≥‘𝑀) → 𝑖 ∈ ℝ)
234	233	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ ℝ)
235		eluzle 11700	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑖)
236	235	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑀 ≤ 𝑖)
237	32	nnred 11035	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℝ)
238	237	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑀 ∈ ℝ)
239		elicopnf 12269	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℝ → (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀 ≤ 𝑖)))
240	238, 239	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀 ≤ 𝑖)))
241	234, 236, 240	mpbir2and 957	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ (𝑀[,)+∞))
242	241	ex 450	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑖 ∈ (ℤ_≥‘𝑀) → 𝑖 ∈ (𝑀[,)+∞)))
243	242	ssrdv 3609	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℤ_≥‘𝑀) ⊆ (𝑀[,)+∞))
244	32	nnzd 11481	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℤ)
245	49	peano2zd 11485	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐼 + 1) ∈ ℤ)
246	103	rpred 11872	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 ∈ ℝ)
247	4	nnred 11035	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐼 + 1) ∈ ℝ)
248		dchrisumlem2.2	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ≤ 𝑈)
249		dchrisumlem2.3	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 ≤ (𝐼 + 1))
250	237, 246, 247, 248, 249	letrd 10194	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ≤ (𝐼 + 1))
251		eluz2 11693	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 + 1) ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝐼 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝐼 + 1)))
252	244, 245, 250, 251	syl3anbrc 1246	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 + 1) ∈ (ℤ_≥‘𝑀))
253		uztrn 11704	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 + 1) ∈ (ℤ_≥‘(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (ℤ_≥‘𝑀)) → (𝐽 + 1) ∈ (ℤ_≥‘𝑀))
254	9, 252, 253	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐽 + 1) ∈ (ℤ_≥‘𝑀))
255	243, 254	sseldd 3604	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐽 + 1) ∈ (𝑀[,)+∞))
256	115	simprd 479	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐽 + 1) ∈ (𝑀[,)+∞) → 0 ≤ ⦋(𝐽 + 1) / 𝑛⦌𝐴))
257	255, 256	mpd 15	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ ⦋(𝐽 + 1) / 𝑛⦌𝐴)
258	117, 257	absidd 14161	. . . . . . . . . . . 12 ⊢ (𝜑 → (abs‘⦋(𝐽 + 1) / 𝑛⦌𝐴) = ⦋(𝐽 + 1) / 𝑛⦌𝐴)
259	258	oveq1d 6665	. . . . . . . . . . 11 ⊢ (𝜑 → ((abs‘⦋(𝐽 + 1) / 𝑛⦌𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) = (⦋(𝐽 + 1) / 𝑛⦌𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))))
260	232, 259	eqtrd 2656	. . . . . . . . . 10 ⊢ (𝜑 → (abs‘(⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) = (⦋(𝐽 + 1) / 𝑛⦌𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))))
261	126	abscld 14175	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) ∈ ℝ)
262	113	nnnn0d 11351	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐽 + 1) ∈ ℕ₀)
263		dchrisum.10	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅)
264	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263	dchrisumlem1 25178	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐽 + 1) ∈ ℕ₀) → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) ≤ 𝑅)
265	262, 264	mpdan 702	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) ≤ 𝑅)
266	261, 95, 117, 257, 265	lemul2ad 10964	. . . . . . . . . 10 ⊢ (𝜑 → (⦋(𝐽 + 1) / 𝑛⦌𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ (⦋(𝐽 + 1) / 𝑛⦌𝐴 · 𝑅))
267	260, 266	eqbrtrd 4675	. . . . . . . . 9 ⊢ (𝜑 → (abs‘(⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ (⦋(𝐽 + 1) / 𝑛⦌𝐴 · 𝑅))
268	128, 133	absmuld 14193	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) = ((abs‘⦋(𝐼 + 1) / 𝑛⦌𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))))
269	243, 252	sseldd 3604	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐼 + 1) ∈ (𝑀[,)+∞))
270	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36	dchrisumlema 25177	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐼 + 1) ∈ ℝ⁺ → ⦋(𝐼 + 1) / 𝑛⦌𝐴 ∈ ℝ) ∧ ((𝐼 + 1) ∈ (𝑀[,)+∞) → 0 ≤ ⦋(𝐼 + 1) / 𝑛⦌𝐴)))
271	270	simprd 479	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐼 + 1) ∈ (𝑀[,)+∞) → 0 ≤ ⦋(𝐼 + 1) / 𝑛⦌𝐴))
272	269, 271	mpd 15	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ ⦋(𝐼 + 1) / 𝑛⦌𝐴)
273	101, 272	absidd 14161	. . . . . . . . . . . 12 ⊢ (𝜑 → (abs‘⦋(𝐼 + 1) / 𝑛⦌𝐴) = ⦋(𝐼 + 1) / 𝑛⦌𝐴)
274	273	oveq1d 6665	. . . . . . . . . . 11 ⊢ (𝜑 → ((abs‘⦋(𝐼 + 1) / 𝑛⦌𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) = (⦋(𝐼 + 1) / 𝑛⦌𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))))
275	268, 274	eqtrd 2656	. . . . . . . . . 10 ⊢ (𝜑 → (abs‘(⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) = (⦋(𝐼 + 1) / 𝑛⦌𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))))
276	133	abscld 14175	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))) ∈ ℝ)
277	4	nnnn0d 11351	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐼 + 1) ∈ ℕ₀)
278	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263	dchrisumlem1 25178	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐼 + 1) ∈ ℕ₀) → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))) ≤ 𝑅)
279	277, 278	mpdan 702	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))) ≤ 𝑅)
280	276, 95, 101, 272, 279	lemul2ad 10964	. . . . . . . . . 10 ⊢ (𝜑 → (⦋(𝐼 + 1) / 𝑛⦌𝐴 · (abs‘Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ (⦋(𝐼 + 1) / 𝑛⦌𝐴 · 𝑅))
281	275, 280	eqbrtrd 4675	. . . . . . . . 9 ⊢ (𝜑 → (abs‘(⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ (⦋(𝐼 + 1) / 𝑛⦌𝐴 · 𝑅))
282	226, 227, 230, 231, 267, 281	le2addd 10646	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) + (abs‘(⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) ≤ ((⦋(𝐽 + 1) / 𝑛⦌𝐴 · 𝑅) + (⦋(𝐼 + 1) / 𝑛⦌𝐴 · 𝑅)))
283	95	recnd 10068	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ ℂ)
284	118, 128, 283	adddird 10065	. . . . . . . 8 ⊢ (𝜑 → ((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) · 𝑅) = ((⦋(𝐽 + 1) / 𝑛⦌𝐴 · 𝑅) + (⦋(𝐼 + 1) / 𝑛⦌𝐴 · 𝑅)))
285	282, 284	breqtrrd 4681	. . . . . . 7 ⊢ (𝜑 → ((abs‘(⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛)))) + (abs‘(⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) ≤ ((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) · 𝑅))
286	136, 228, 218, 229, 285	letrd 10194	. . . . . 6 ⊢ (𝜑 → (abs‘((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) ≤ ((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) · 𝑅))
287	156	abscld 14175	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ∈ ℝ)
288	83, 287	fsumrecl 14465	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ∈ ℝ)
289	83, 156	fsumabs 14533	. . . . . . 7 ⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))))
290	95	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑅 ∈ ℝ)
291	222, 290	remulcld 10070	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · 𝑅) ∈ ℝ)
292	137, 148	syldan 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) ∈ ℂ)
293	153	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)) ∈ ℂ)
294	292, 293	absmuld 14193	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) = ((abs‘(⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴)) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))))
295		elfzouz 12474	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1)) → 𝑖 ∈ (ℤ_≥‘(𝐼 + 1)))
296		uztrn 11704	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ (ℤ_≥‘(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ (ℤ_≥‘𝑀))
297	295, 252, 296	syl2anr 495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 𝑖 ∈ (ℤ_≥‘𝑀))
298		eluznn 11758	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ ℕ)
299	32, 298	sylan 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ ℕ)
300	299, 139	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑖 + 1) ∈ ℝ⁺)
301	299	nnrpd 11870	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ∈ ℝ⁺)
302	34	3expia 1267	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺)) → ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
303	302	ralrimivva 2971	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
304	303	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴))
305		nfcv 2764	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛ℝ⁺
306		nfv 1843	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛(𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥)
307		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑛𝐵
308		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑛 ≤
309	307, 308, 60	nfbr 4699	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴
310	306, 309	nfim 1825	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) → 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴)
311	305, 310	nfral 2945	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑛∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) → 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴)
312		breq2 4657	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑖 → (𝑀 ≤ 𝑛 ↔ 𝑀 ≤ 𝑖))
313		breq1 4656	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑖 → (𝑛 ≤ 𝑥 ↔ 𝑖 ≤ 𝑥))
314	312, 313	anbi12d 747	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑖 → ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) ↔ (𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥)))
315	64	breq2d 4665	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑖 → (𝐵 ≤ 𝐴 ↔ 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴))
316	314, 315	imbi12d 334	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑖 → (((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) ↔ ((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) → 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴)))
317	316	ralbidv 2986	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑖 → (∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) ↔ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) → 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴)))
318	311, 317	rspc 3303	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) → ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) → 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴)))
319	301, 304, 318	sylc 65	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) → 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴))
320	234	lep1d 10955	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝑖 ≤ (𝑖 + 1))
321	236, 320	jca 554	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑀 ≤ 𝑖 ∧ 𝑖 ≤ (𝑖 + 1)))
322		breq2 4657	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑖 + 1) → (𝑖 ≤ 𝑥 ↔ 𝑖 ≤ (𝑖 + 1)))
323	322	anbi2d 740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑖 + 1) → ((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) ↔ (𝑀 ≤ 𝑖 ∧ 𝑖 ≤ (𝑖 + 1))))
324		eqvisset 3211	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑖 + 1) → (𝑖 + 1) ∈ V)
325		eqtr3 2643	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) → 𝑥 = 𝑛)
326	31	equcoms 1947	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑛 → 𝐴 = 𝐵)
327	325, 326	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) → 𝐴 = 𝐵)
328	324, 327	csbied 3560	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑖 + 1) → ⦋(𝑖 + 1) / 𝑛⦌𝐴 = 𝐵)
329	328	eqcomd 2628	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑖 + 1) → 𝐵 = ⦋(𝑖 + 1) / 𝑛⦌𝐴)
330	329	breq1d 4663	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑖 + 1) → (𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴 ↔ ⦋(𝑖 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑖 / 𝑛⦌𝐴))
331	323, 330	imbi12d 334	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑖 + 1) → (((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) → 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴) ↔ ((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ (𝑖 + 1)) → ⦋(𝑖 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑖 / 𝑛⦌𝐴)))
332	331	rspcv 3305	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 + 1) ∈ ℝ⁺ → (∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑥) → 𝐵 ≤ ⦋𝑖 / 𝑛⦌𝐴) → ((𝑀 ≤ 𝑖 ∧ 𝑖 ≤ (𝑖 + 1)) → ⦋(𝑖 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑖 / 𝑛⦌𝐴)))
333	300, 319, 321, 332	syl3c 66	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → ⦋(𝑖 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑖 / 𝑛⦌𝐴)
334	297, 333	syldan 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ⦋(𝑖 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑖 / 𝑛⦌𝐴)
335	221, 220, 334	abssuble0d 14171	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘(⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴)) = (⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴))
336	335	oveq1d 6665	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((abs‘(⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴)) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) = ((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))))
337	294, 336	eqtrd 2656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) = ((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))))
338	293	abscld 14175	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))) ∈ ℝ)
339	220, 221	subge0d 10617	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (0 ≤ (⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) ↔ ⦋(𝑖 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑖 / 𝑛⦌𝐴))
340	334, 339	mpbird 247	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → 0 ≤ (⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴))
341	137	peano2nnd 11037	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) ∈ ℕ)
342	341	nnnn0d 11351	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (𝑖 + 1) ∈ ℕ₀)
343	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263	dchrisumlem1 25178	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 + 1) ∈ ℕ₀) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))) ≤ 𝑅)
344	342, 343	syldan 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))) ≤ 𝑅)
345	338, 290, 222, 340, 344	lemul2ad 10964	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → ((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · (abs‘Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ ((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · 𝑅))
346	337, 345	eqbrtrd 4675	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (abs‘((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ ((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · 𝑅))
347	83, 287, 291, 346	fsumle 14531	. . . . . . . 8 ⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · 𝑅))
348	222	recnd 10068	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) → (⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) ∈ ℂ)
349	83, 283, 348	fsummulc1 14517	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · 𝑅) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · 𝑅))
350	219	oveq1d 6665	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · 𝑅) = ((⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) · 𝑅))
351	349, 350	eqtr3d 2658	. . . . . . . 8 ⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋𝑖 / 𝑛⦌𝐴 − ⦋(𝑖 + 1) / 𝑛⦌𝐴) · 𝑅) = ((⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) · 𝑅))
352	347, 351	breqtrd 4679	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(abs‘((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ ((⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) · 𝑅))
353	158, 288, 225, 289, 352	letrd 10194	. . . . . 6 ⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛)))) ≤ ((⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) · 𝑅))
354	136, 158, 218, 225, 286, 353	le2addd 10646	. . . . 5 ⊢ (𝜑 → ((abs‘((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))) ≤ (((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) · 𝑅) + ((⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) · 𝑅)))
355	128	2timesd 11275	. . . . . . . 8 ⊢ (𝜑 → (2 · ⦋(𝐼 + 1) / 𝑛⦌𝐴) = (⦋(𝐼 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴))
356	128, 118, 128	ppncand 10432	. . . . . . . 8 ⊢ (𝜑 → ((⦋(𝐼 + 1) / 𝑛⦌𝐴 + ⦋(𝐽 + 1) / 𝑛⦌𝐴) + (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴)) = (⦋(𝐼 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴))
357	128, 118	addcomd 10238	. . . . . . . . 9 ⊢ (𝜑 → (⦋(𝐼 + 1) / 𝑛⦌𝐴 + ⦋(𝐽 + 1) / 𝑛⦌𝐴) = (⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴))
358	357	oveq1d 6665	. . . . . . . 8 ⊢ (𝜑 → ((⦋(𝐼 + 1) / 𝑛⦌𝐴 + ⦋(𝐽 + 1) / 𝑛⦌𝐴) + (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴)) = ((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) + (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴)))
359	355, 356, 358	3eqtr2d 2662	. . . . . . 7 ⊢ (𝜑 → (2 · ⦋(𝐼 + 1) / 𝑛⦌𝐴) = ((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) + (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴)))
360	359	oveq1d 6665	. . . . . 6 ⊢ (𝜑 → ((2 · ⦋(𝐼 + 1) / 𝑛⦌𝐴) · 𝑅) = (((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) + (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴)) · 𝑅))
361		2cnd 11093	. . . . . . 7 ⊢ (𝜑 → 2 ∈ ℂ)
362	361, 128, 283	mul32d 10246	. . . . . 6 ⊢ (𝜑 → ((2 · ⦋(𝐼 + 1) / 𝑛⦌𝐴) · 𝑅) = ((2 · 𝑅) · ⦋(𝐼 + 1) / 𝑛⦌𝐴))
363	217	recnd 10068	. . . . . . 7 ⊢ (𝜑 → (⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) ∈ ℂ)
364	224	recnd 10068	. . . . . . 7 ⊢ (𝜑 → (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) ∈ ℂ)
365	363, 364, 283	adddird 10065	. . . . . 6 ⊢ (𝜑 → (((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) + (⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴)) · 𝑅) = (((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) · 𝑅) + ((⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) · 𝑅)))
366	360, 362, 365	3eqtr3d 2664	. . . . 5 ⊢ (𝜑 → ((2 · 𝑅) · ⦋(𝐼 + 1) / 𝑛⦌𝐴) = (((⦋(𝐽 + 1) / 𝑛⦌𝐴 + ⦋(𝐼 + 1) / 𝑛⦌𝐴) · 𝑅) + ((⦋(𝐼 + 1) / 𝑛⦌𝐴 − ⦋(𝐽 + 1) / 𝑛⦌𝐴) · 𝑅)))
367	354, 366	breqtrrd 4681	. . . 4 ⊢ (𝜑 → ((abs‘((⦋(𝐽 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))) − (⦋(𝐼 + 1) / 𝑛⦌𝐴 · Σ𝑛 ∈ (0..^(𝐼 + 1))(𝑋‘(𝐿‘𝑛))))) + (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / 𝑛⦌𝐴 − ⦋𝑖 / 𝑛⦌𝐴) · Σ𝑛 ∈ (0..^(𝑖 + 1))(𝑋‘(𝐿‘𝑛))))) ≤ ((2 · 𝑅) · ⦋(𝐼 + 1) / 𝑛⦌𝐴))
368	92, 159, 102, 216, 367	letrd 10194	. . 3 ⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) ≤ ((2 · 𝑅) · ⦋(𝐼 + 1) / 𝑛⦌𝐴))
369		2nn0 11309	. . . . . 6 ⊢ 2 ∈ ℕ₀
370		nn0ge0 11318	. . . . . 6 ⊢ (2 ∈ ℕ₀ → 0 ≤ 2)
371	369, 370	mp1i 13	. . . . 5 ⊢ (𝜑 → 0 ≤ 2)
372		0red 10041	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℝ)
373	126	absge0d 14183	. . . . . 6 ⊢ (𝜑 → 0 ≤ (abs‘Σ𝑛 ∈ (0..^(𝐽 + 1))(𝑋‘(𝐿‘𝑛))))
374	372, 261, 95, 373, 265	letrd 10194	. . . . 5 ⊢ (𝜑 → 0 ≤ 𝑅)
375	94, 95, 371, 374	mulge0d 10604	. . . 4 ⊢ (𝜑 → 0 ≤ (2 · 𝑅))
376	4	nnrpd 11870	. . . . 5 ⊢ (𝜑 → (𝐼 + 1) ∈ ℝ⁺)
377		nfv 1843	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥)
378	307, 308, 105	nfbr 4699	. . . . . . . . 9 ⊢ Ⅎ𝑛 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴
379	377, 378	nfim 1825	. . . . . . . 8 ⊢ Ⅎ𝑛((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) → 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴)
380	305, 379	nfral 2945	. . . . . . 7 ⊢ Ⅎ𝑛∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) → 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴)
381		breq2 4657	. . . . . . . . . 10 ⊢ (𝑛 = 𝑈 → (𝑀 ≤ 𝑛 ↔ 𝑀 ≤ 𝑈))
382		breq1 4656	. . . . . . . . . 10 ⊢ (𝑛 = 𝑈 → (𝑛 ≤ 𝑥 ↔ 𝑈 ≤ 𝑥))
383	381, 382	anbi12d 747	. . . . . . . . 9 ⊢ (𝑛 = 𝑈 → ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) ↔ (𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥)))
384	107	breq2d 4665	. . . . . . . . 9 ⊢ (𝑛 = 𝑈 → (𝐵 ≤ 𝐴 ↔ 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴))
385	383, 384	imbi12d 334	. . . . . . . 8 ⊢ (𝑛 = 𝑈 → (((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) ↔ ((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) → 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴)))
386	385	ralbidv 2986	. . . . . . 7 ⊢ (𝑛 = 𝑈 → (∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) ↔ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) → 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴)))
387	380, 386	rspc 3303	. . . . . 6 ⊢ (𝑈 ∈ ℝ⁺ → (∀𝑛 ∈ ℝ⁺ ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥) → 𝐵 ≤ 𝐴) → ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) → 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴)))
388	103, 303, 387	sylc 65	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) → 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴))
389	248, 249	jca 554	. . . . 5 ⊢ (𝜑 → (𝑀 ≤ 𝑈 ∧ 𝑈 ≤ (𝐼 + 1)))
390		breq2 4657	. . . . . . . 8 ⊢ (𝑥 = (𝐼 + 1) → (𝑈 ≤ 𝑥 ↔ 𝑈 ≤ (𝐼 + 1)))
391	390	anbi2d 740	. . . . . . 7 ⊢ (𝑥 = (𝐼 + 1) → ((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) ↔ (𝑀 ≤ 𝑈 ∧ 𝑈 ≤ (𝐼 + 1))))
392		eqvisset 3211	. . . . . . . . . 10 ⊢ (𝑥 = (𝐼 + 1) → (𝐼 + 1) ∈ V)
393		eqtr3 2643	. . . . . . . . . . 11 ⊢ ((𝑥 = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) → 𝑥 = 𝑛)
394	393, 326	syl 17	. . . . . . . . . 10 ⊢ ((𝑥 = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) → 𝐴 = 𝐵)
395	392, 394	csbied 3560	. . . . . . . . 9 ⊢ (𝑥 = (𝐼 + 1) → ⦋(𝐼 + 1) / 𝑛⦌𝐴 = 𝐵)
396	395	eqcomd 2628	. . . . . . . 8 ⊢ (𝑥 = (𝐼 + 1) → 𝐵 = ⦋(𝐼 + 1) / 𝑛⦌𝐴)
397	396	breq1d 4663	. . . . . . 7 ⊢ (𝑥 = (𝐼 + 1) → (𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴 ↔ ⦋(𝐼 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑈 / 𝑛⦌𝐴))
398	391, 397	imbi12d 334	. . . . . 6 ⊢ (𝑥 = (𝐼 + 1) → (((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) → 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴) ↔ ((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ (𝐼 + 1)) → ⦋(𝐼 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑈 / 𝑛⦌𝐴)))
399	398	rspcv 3305	. . . . 5 ⊢ ((𝐼 + 1) ∈ ℝ⁺ → (∀𝑥 ∈ ℝ⁺ ((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ 𝑥) → 𝐵 ≤ ⦋𝑈 / 𝑛⦌𝐴) → ((𝑀 ≤ 𝑈 ∧ 𝑈 ≤ (𝐼 + 1)) → ⦋(𝐼 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑈 / 𝑛⦌𝐴)))
400	376, 388, 389, 399	syl3c 66	. . . 4 ⊢ (𝜑 → ⦋(𝐼 + 1) / 𝑛⦌𝐴 ≤ ⦋𝑈 / 𝑛⦌𝐴)
401	101, 110, 96, 375, 400	lemul2ad 10964	. . 3 ⊢ (𝜑 → ((2 · 𝑅) · ⦋(𝐼 + 1) / 𝑛⦌𝐴) ≤ ((2 · 𝑅) · ⦋𝑈 / 𝑛⦌𝐴))
402	92, 102, 111, 368, 401	letrd 10194	. 2 ⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((𝑋‘(𝐿‘𝑖)) · ⦋𝑖 / 𝑛⦌𝐴)) ≤ ((2 · 𝑅) · ⦋𝑈 / 𝑛⦌𝐴))
403	91, 402	eqbrtrd 4675	1 ⊢ (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) ≤ ((2 · 𝑅) · ⦋𝑈 / 𝑛⦌𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 Vcvv 3200 ⦋csb 3533 ∪ cun 3572 ∩ cin 3573 ∅c0 3915 class class class wbr 4653 ↦ cmpt 4729 ‘cfv 5888 (class class class)co 6650 Fincfn 7955 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 +∞cpnf 10071 ≤ cle 10075 − cmin 10266 ℕcn 11020 2c2 11070 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ℝ⁺crp 11832 [,)cico 12177 ...cfz 12326 ..^cfzo 12465 seqcseq 12801 abscabs 13974 ⇝_𝑟 crli 14216 Σcsu 14416 Basecbs 15857 0_gc0g 16100 ℤRHomczrh 19848 ℤ/nℤczn 19851 DChrcdchr 24957

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-tpos 7352 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-ec 7744 df-qs 7748 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-xnn0 11364 df-z 11378 df-dec 11494 df-uz 11688 df-rp 11833 df-ico 12181 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-rlim 14220 df-sum 14417 df-dvds 14984 df-gcd 15217 df-phi 15471 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-0g 16102 df-imas 16168 df-qus 16169 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-mhm 17335 df-grp 17425 df-minusg 17426 df-sbg 17427 df-mulg 17541 df-subg 17591 df-nsg 17592 df-eqg 17593 df-ghm 17658 df-cmn 18195 df-abl 18196 df-mgp 18490 df-ur 18502 df-ring 18549 df-cring 18550 df-oppr 18623 df-dvdsr 18641 df-unit 18642 df-invr 18672 df-rnghom 18715 df-subrg 18778 df-lmod 18865 df-lss 18933 df-lsp 18972 df-sra 19172 df-rgmod 19173 df-lidl 19174 df-rsp 19175 df-2idl 19232 df-cnfld 19747 df-zring 19819 df-zrh 19852 df-zn 19855 df-dchr 24958

This theorem is referenced by: dchrisumlem3 25180

W3C validator