dvfsum2 - Metamath Proof Explorer

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

Theorem dvfsum2 26011

Description: The reverse of dvfsumrlim 26008, when comparing a finite sum of increasing terms to an integral. In this case there is no point in stating the limit properties, because the terms of the sum aren't approaching zero, but there is nevertheless still a natural asymptotic statement that can be made. (Contributed by Mario Carneiro, 20-May-2016.)

**Hypotheses**
Ref	Expression
dvfsum2.s	⊢ 𝑆 = (𝑇(,)+∞)
dvfsum2.z	⊢ 𝑍 = (ℤ_≥‘𝑀)
dvfsum2.m	⊢ (𝜑 → 𝑀 ∈ ℤ)
dvfsum2.d	⊢ (𝜑 → 𝐷 ∈ ℝ)
dvfsum2.u	⊢ (𝜑 → 𝑈 ∈ ℝ^*)
dvfsum2.md	⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))
dvfsum2.t	⊢ (𝜑 → 𝑇 ∈ ℝ)
dvfsum2.a	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)
dvfsum2.b1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)
dvfsum2.b2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)
dvfsum2.b3	⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))
dvfsum2.c	⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)
dvfsum2.l	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐵 ≤ 𝐶)
dvfsum2.g	⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))
dvfsum2.0	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵)
dvfsum2.1	⊢ (𝜑 → 𝑋 ∈ 𝑆)
dvfsum2.2	⊢ (𝜑 → 𝑌 ∈ 𝑆)
dvfsum2.3	⊢ (𝜑 → 𝐷 ≤ 𝑋)
dvfsum2.4	⊢ (𝜑 → 𝑋 ≤ 𝑌)
dvfsum2.5	⊢ (𝜑 → 𝑌 ≤ 𝑈)
dvfsum2.e	⊢ (𝑥 = 𝑌 → 𝐵 = 𝐸)

**Assertion**
Ref	Expression
dvfsum2	⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) ≤ 𝐸)

Distinct variable groups: 𝐵,𝑘 𝑥,𝐶 𝑥,𝑘,𝐷 𝜑,𝑘,𝑥 𝑥,𝐸 𝑘,𝑀,𝑥 𝑆,𝑘,𝑥 𝑘,𝑋,𝑥 𝑘,𝑌,𝑥 𝑥,𝑇 𝑈,𝑘,𝑥 𝑥,𝑉 𝑥,𝑍 Allowed substitution hints: 𝐴(𝑥,𝑘) 𝐵(𝑥) 𝐶(𝑘) 𝑇(𝑘) 𝐸(𝑘) 𝐺(𝑥,𝑘) 𝑉(𝑘) 𝑍(𝑘)

Proof of Theorem dvfsum2 Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvfsum2.2	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑆)
2		fzfid 13926	. . . . . . . 8 ⊢ (𝜑 → (𝑀...(⌊‘𝑌)) ∈ Fin)
3		dvfsum2.b2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)
4	3	ralrimiva 3130	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝑍 𝐵 ∈ ℝ)
5		elfzuz 13465	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑀...(⌊‘𝑌)) → 𝑘 ∈ (ℤ_≥‘𝑀))
6		dvfsum2.z	. . . . . . . . . 10 ⊢ 𝑍 = (ℤ_≥‘𝑀)
7	5, 6	eleqtrrdi 2848	. . . . . . . . 9 ⊢ (𝑘 ∈ (𝑀...(⌊‘𝑌)) → 𝑘 ∈ 𝑍)
8		dvfsum2.c	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)
9	8	eleq1d 2822	. . . . . . . . . 10 ⊢ (𝑥 = 𝑘 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ))
10	9	rspccva 3564	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝑍 𝐵 ∈ ℝ ∧ 𝑘 ∈ 𝑍) → 𝐶 ∈ ℝ)
11	4, 7, 10	syl2an 597	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑌))) → 𝐶 ∈ ℝ)
12	2, 11	fsumrecl 15687	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 ∈ ℝ)
13		dvfsum2.a	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)
14	13	ralrimiva 3130	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ)
15		nfcsb1v 3862	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑌 / 𝑥⦌𝐴
16	15	nfel1 2916	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ
17		csbeq1a 3852	. . . . . . . . . 10 ⊢ (𝑥 = 𝑌 → 𝐴 = ⦋𝑌 / 𝑥⦌𝐴)
18	17	eleq1d 2822	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → (𝐴 ∈ ℝ ↔ ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ))
19	16, 18	rspc 3553	. . . . . . . 8 ⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ))
20	1, 14, 19	sylc 65	. . . . . . 7 ⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ)
21	12, 20	resubcld 11569	. . . . . 6 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ)
22		nfcv 2899	. . . . . . 7 ⊢ Ⅎ𝑥𝑌
23		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶
24		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑥 −
25	23, 24, 15	nfov 7390	. . . . . . 7 ⊢ Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)
26		fveq2 6834	. . . . . . . . . 10 ⊢ (𝑥 = 𝑌 → (⌊‘𝑥) = (⌊‘𝑌))
27	26	oveq2d 7376	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → (𝑀...(⌊‘𝑥)) = (𝑀...(⌊‘𝑌)))
28	27	sumeq1d 15653	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶)
29	28, 17	oveq12d 7378	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))
30		dvfsum2.g	. . . . . . 7 ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))
31	22, 25, 29, 30	fvmptf 6963	. . . . . 6 ⊢ ((𝑌 ∈ 𝑆 ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) → (𝐺‘𝑌) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))
32	1, 21, 31	syl2anc 585	. . . . 5 ⊢ (𝜑 → (𝐺‘𝑌) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))
33		dvfsum2.1	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑆)
34		fzfid 13926	. . . . . . . 8 ⊢ (𝜑 → (𝑀...(⌊‘𝑋)) ∈ Fin)
35		elfzuz 13465	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ (ℤ_≥‘𝑀))
36	35, 6	eleqtrrdi 2848	. . . . . . . . 9 ⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ 𝑍)
37	4, 36, 10	syl2an 597	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℝ)
38	34, 37	fsumrecl 15687	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℝ)
39		nfcsb1v 3862	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐴
40	39	nfel1 2916	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ
41		csbeq1a 3852	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → 𝐴 = ⦋𝑋 / 𝑥⦌𝐴)
42	41	eleq1d 2822	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝐴 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ))
43	40, 42	rspc 3553	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ))
44	33, 14, 43	sylc 65	. . . . . . 7 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ)
45	38, 44	resubcld 11569	. . . . . 6 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ)
46		nfcv 2899	. . . . . . 7 ⊢ Ⅎ𝑥𝑋
47		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶
48	47, 24, 39	nfov 7390	. . . . . . 7 ⊢ Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)
49		fveq2 6834	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (⌊‘𝑥) = (⌊‘𝑋))
50	49	oveq2d 7376	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑀...(⌊‘𝑥)) = (𝑀...(⌊‘𝑋)))
51	50	sumeq1d 15653	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)
52	51, 41	oveq12d 7378	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
53	46, 48, 52, 30	fvmptf 6963	. . . . . 6 ⊢ ((𝑋 ∈ 𝑆 ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) → (𝐺‘𝑋) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
54	33, 45, 53	syl2anc 585	. . . . 5 ⊢ (𝜑 → (𝐺‘𝑋) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
55	32, 54	oveq12d 7378	. . . 4 ⊢ (𝜑 → ((𝐺‘𝑌) − (𝐺‘𝑋)) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
56	55	fveq2d 6838	. . 3 ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
57	21	recnd 11164	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℂ)
58	45	recnd 11164	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℂ)
59	57, 58	abssubd 15409	. . 3 ⊢ (𝜑 → (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
60	56, 59	eqtrd 2772	. 2 ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
61		dvfsum2.s	. . . . . . . . . 10 ⊢ 𝑆 = (𝑇(,)+∞)
62		ioossre 13351	. . . . . . . . . 10 ⊢ (𝑇(,)+∞) ⊆ ℝ
63	61, 62	eqsstri 3969	. . . . . . . . 9 ⊢ 𝑆 ⊆ ℝ
64	63	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ⊆ ℝ)
65		dvfsum2.b1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)
66		dvfsum2.b3	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))
67	64, 13, 65, 66	dvmptrecl 26001	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ)
68	67	ralrimiva 3130	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ)
69		dvfsum2.e	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐸)
70	69	eleq1d 2822	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝐵 ∈ ℝ ↔ 𝐸 ∈ ℝ))
71	70	rspcv 3561	. . . . . 6 ⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ → 𝐸 ∈ ℝ))
72	1, 68, 71	sylc 65	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ℝ)
73	21, 72	resubcld 11569	. . . 4 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ∈ ℝ)
74	63, 33	sselid 3920	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ ℝ)
75		reflcl 13746	. . . . . . . . 9 ⊢ (𝑋 ∈ ℝ → (⌊‘𝑋) ∈ ℝ)
76	74, 75	syl 17	. . . . . . . 8 ⊢ (𝜑 → (⌊‘𝑋) ∈ ℝ)
77	74, 76	resubcld 11569	. . . . . . 7 ⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℝ)
78		nfv 1916	. . . . . . . . . 10 ⊢ Ⅎ𝑚 𝐵 ∈ ℝ
79		nfcsb1v 3862	. . . . . . . . . . 11 ⊢ Ⅎ𝑥⦋𝑚 / 𝑥⦌𝐵
80	79	nfel1 2916	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ
81		csbeq1a 3852	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑥⦌𝐵)
82	81	eleq1d 2822	. . . . . . . . . 10 ⊢ (𝑥 = 𝑚 → (𝐵 ∈ ℝ ↔ ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ))
83	78, 80, 82	cbvralw 3280	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ ↔ ∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ)
84	68, 83	sylib 218	. . . . . . . 8 ⊢ (𝜑 → ∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ)
85		csbeq1 3841	. . . . . . . . . 10 ⊢ (𝑚 = 𝑋 → ⦋𝑚 / 𝑥⦌𝐵 = ⦋𝑋 / 𝑥⦌𝐵)
86	85	eleq1d 2822	. . . . . . . . 9 ⊢ (𝑚 = 𝑋 → (⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ))
87	86	rspcv 3561	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑆 → (∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ))
88	33, 84, 87	sylc 65	. . . . . . 7 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ)
89	77, 88	remulcld 11166	. . . . . 6 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ)
90	89, 45	readdcld 11165	. . . . 5 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ)
91	90, 88	resubcld 11569	. . . 4 ⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ)
92	63, 1	sselid 3920	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ ℝ)
93		reflcl 13746	. . . . . . . . . 10 ⊢ (𝑌 ∈ ℝ → (⌊‘𝑌) ∈ ℝ)
94	92, 93	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (⌊‘𝑌) ∈ ℝ)
95	92, 94	resubcld 11569	. . . . . . . 8 ⊢ (𝜑 → (𝑌 − (⌊‘𝑌)) ∈ ℝ)
96	95, 72	remulcld 11166	. . . . . . 7 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ∈ ℝ)
97	96, 21	readdcld 11165	. . . . . 6 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ)
98	97, 72	resubcld 11569	. . . . 5 ⊢ (𝜑 → ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) ∈ ℝ)
99		fracge0 13754	. . . . . . . . 9 ⊢ (𝑌 ∈ ℝ → 0 ≤ (𝑌 − (⌊‘𝑌)))
100	92, 99	syl 17	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ (𝑌 − (⌊‘𝑌)))
101		dvfsum2.0	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵)
102	101	expr 456	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷 ≤ 𝑥 → 0 ≤ 𝐵))
103	102	ralrimiva 3130	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 0 ≤ 𝐵))
104		dvfsum2.d	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℝ)
105		dvfsum2.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ≤ 𝑋)
106		dvfsum2.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ≤ 𝑌)
107	104, 74, 92, 105, 106	letrd 11294	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≤ 𝑌)
108		breq2 5090	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑌 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑌))
109	69	breq2d 5098	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑌 → (0 ≤ 𝐵 ↔ 0 ≤ 𝐸))
110	108, 109	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑥 = 𝑌 → ((𝐷 ≤ 𝑥 → 0 ≤ 𝐵) ↔ (𝐷 ≤ 𝑌 → 0 ≤ 𝐸)))
111	110	rspcv 3561	. . . . . . . . 9 ⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 0 ≤ 𝐵) → (𝐷 ≤ 𝑌 → 0 ≤ 𝐸)))
112	1, 103, 107, 111	syl3c 66	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 𝐸)
113	95, 72, 100, 112	mulge0d 11718	. . . . . . 7 ⊢ (𝜑 → 0 ≤ ((𝑌 − (⌊‘𝑌)) · 𝐸))
114	21, 96	addge02d 11730	. . . . . . 7 ⊢ (𝜑 → (0 ≤ ((𝑌 − (⌊‘𝑌)) · 𝐸) ↔ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
115	113, 114	mpbid 232	. . . . . 6 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
116	21, 97, 72, 115	lesub1dd 11757	. . . . 5 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸))
117		dvfsum2.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℤ)
118		dvfsum2.md	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))
119		dvfsum2.t	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ ℝ)
120	13	renegcld 11568	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → -𝐴 ∈ ℝ)
121	67	renegcld 11568	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → -𝐵 ∈ ℝ)
122	3	renegcld 11568	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → -𝐵 ∈ ℝ)
123		reelprrecn 11121	. . . . . . . . . . . . 13 ⊢ ℝ ∈ {ℝ, ℂ}
124	123	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
125	13	recnd 11164	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℂ)
126	124, 125, 65, 66	dvmptneg 25943	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ -𝐴)) = (𝑥 ∈ 𝑆 ↦ -𝐵))
127	8	negeqd 11378	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑘 → -𝐵 = -𝐶)
128		dvfsum2.u	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ ℝ^*)
129		dvfsum2.l	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐵 ≤ 𝐶)
130	67	adantrr 718	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) → 𝐵 ∈ ℝ)
131	130	3adant3 1133	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐵 ∈ ℝ)
132		simp2r 1202	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝑘 ∈ 𝑆)
133	68	3ad2ant1 1134	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ)
134	9	rspcv 3561	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ → 𝐶 ∈ ℝ))
135	132, 133, 134	sylc 65	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ∈ ℝ)
136	131, 135	lenegd 11720	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → (𝐵 ≤ 𝐶 ↔ -𝐶 ≤ -𝐵))
137	129, 136	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → -𝐶 ≤ -𝐵)
138		eqid 2737	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴))) = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))
139		dvfsum2.5	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ≤ 𝑈)
140	61, 6, 117, 104, 118, 119, 120, 121, 122, 126, 127, 128, 137, 138, 33, 1, 105, 106, 139	dvfsumlem3 26005	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) ≤ ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) ∧ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌-𝐵) ≤ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌-𝐵)))
141	140	simprd 495	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌-𝐵) ≤ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌-𝐵))
142	77	recnd 11164	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℂ)
143	88	recnd 11164	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℂ)
144	142, 143	mulneg2d 11595	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) = -((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵))
145	38	recnd 11164	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℂ)
146	44	recnd 11164	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℂ)
147	145, 146	neg2subd 11513	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (-Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − -⦋𝑋 / 𝑥⦌𝐴) = (⦋𝑋 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
148	37	recnd 11164	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℂ)
149	34, 148	fsumneg 15740	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 = -Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)
150	149	oveq1d 7375	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴) = (-Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − -⦋𝑋 / 𝑥⦌𝐴))
151	145, 146	negsubdi2d 11512	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) = (⦋𝑋 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
152	147, 150, 151	3eqtr4d 2782	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴) = -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
153	144, 152	oveq12d 7378	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) = (-((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
154	89	recnd 11164	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℂ)
155	154, 58	negdid 11509	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) = (-((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
156	153, 155	eqtr4d 2775	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) = -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
157	90	renegcld 11568	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ)
158	156, 157	eqeltrd 2837	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ)
159		nfcv 2899	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑋 − (⌊‘𝑋))
160		nfcv 2899	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 ·
161		nfcsb1v 3862	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐵
162	161	nfneg 11380	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥-⦋𝑋 / 𝑥⦌𝐵
163	159, 160, 162	nfov 7390	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵)
164		nfcv 2899	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥 +
165		nfcv 2899	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶
166	39	nfneg 11380	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥-⦋𝑋 / 𝑥⦌𝐴
167	165, 24, 166	nfov 7390	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)
168	163, 164, 167	nfov 7390	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴))
169		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
170	169, 49	oveq12d 7378	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → (𝑥 − (⌊‘𝑥)) = (𝑋 − (⌊‘𝑋)))
171		csbeq1a 3852	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → 𝐵 = ⦋𝑋 / 𝑥⦌𝐵)
172	171	negeqd 11378	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → -𝐵 = -⦋𝑋 / 𝑥⦌𝐵)
173	170, 172	oveq12d 7378	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → ((𝑥 − (⌊‘𝑥)) · -𝐵) = ((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵))
174	50	sumeq1d 15653	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶)
175	41	negeqd 11378	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → -𝐴 = -⦋𝑋 / 𝑥⦌𝐴)
176	174, 175	oveq12d 7378	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴))
177	173, 176	oveq12d 7378	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)) = (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)))
178	46, 168, 177, 138	fvmptf 6963	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑆 ∧ (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ) → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) = (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)))
179	33, 158, 178	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) = (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)))
180	179, 156	eqtrd 2772	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) = -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
181		csbnegg 11381	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝑆 → ⦋𝑋 / 𝑥⦌-𝐵 = -⦋𝑋 / 𝑥⦌𝐵)
182	33, 181	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌-𝐵 = -⦋𝑋 / 𝑥⦌𝐵)
183	180, 182	oveq12d 7378	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌-𝐵) = (-(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − -⦋𝑋 / 𝑥⦌𝐵))
184	95	recnd 11164	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 − (⌊‘𝑌)) ∈ ℂ)
185	72	recnd 11164	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 ∈ ℂ)
186	184, 185	mulneg2d 11595	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · -𝐸) = -((𝑌 − (⌊‘𝑌)) · 𝐸))
187	12	recnd 11164	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 ∈ ℂ)
188	20	recnd 11164	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℂ)
189	187, 188	neg2subd 11513	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (-Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − -⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶))
190	11	recnd 11164	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑌))) → 𝐶 ∈ ℂ)
191	2, 190	fsumneg 15740	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 = -Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶)
192	191	oveq1d 7375	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴) = (-Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − -⦋𝑌 / 𝑥⦌𝐴))
193	187, 188	negsubdi2d 11512	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶))
194	189, 192, 193	3eqtr4d 2782	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴) = -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))
195	186, 194	oveq12d 7378	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) = (-((𝑌 − (⌊‘𝑌)) · 𝐸) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
196	96	recnd 11164	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ∈ ℂ)
197	196, 57	negdid 11509	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) = (-((𝑌 − (⌊‘𝑌)) · 𝐸) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
198	195, 197	eqtr4d 2775	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) = -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
199	97	renegcld 11568	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ)
200	198, 199	eqeltrd 2837	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ)
201		nfcv 2899	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑌 − (⌊‘𝑌)) · -𝐸)
202		nfcv 2899	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶
203	15	nfneg 11380	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥-⦋𝑌 / 𝑥⦌𝐴
204	202, 24, 203	nfov 7390	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)
205	201, 164, 204	nfov 7390	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴))
206		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑌 → 𝑥 = 𝑌)
207	206, 26	oveq12d 7378	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → (𝑥 − (⌊‘𝑥)) = (𝑌 − (⌊‘𝑌)))
208	69	negeqd 11378	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → -𝐵 = -𝐸)
209	207, 208	oveq12d 7378	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑌 → ((𝑥 − (⌊‘𝑥)) · -𝐵) = ((𝑌 − (⌊‘𝑌)) · -𝐸))
210	27	sumeq1d 15653	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶)
211	17	negeqd 11378	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → -𝐴 = -⦋𝑌 / 𝑥⦌𝐴)
212	210, 211	oveq12d 7378	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑌 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴))
213	209, 212	oveq12d 7378	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑌 → (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)))
214	22, 205, 213, 138	fvmptf 6963	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ 𝑆 ∧ (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ) → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)))
215	1, 200, 214	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)))
216	215, 198	eqtrd 2772	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) = -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
217	208	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = 𝑌) → -𝐵 = -𝐸)
218	1, 217	csbied 3874	. . . . . . . . . 10 ⊢ (𝜑 → ⦋𝑌 / 𝑥⦌-𝐵 = -𝐸)
219	216, 218	oveq12d 7378	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌-𝐵) = (-(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − -𝐸))
220	141, 183, 219	3brtr3d 5117	. . . . . . . 8 ⊢ (𝜑 → (-(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − -⦋𝑋 / 𝑥⦌𝐵) ≤ (-(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − -𝐸))
221	90	recnd 11164	. . . . . . . . 9 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℂ)
222	221, 143	neg2subd 11513	. . . . . . . 8 ⊢ (𝜑 → (-(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − -⦋𝑋 / 𝑥⦌𝐵) = (⦋𝑋 / 𝑥⦌𝐵 − (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
223	97	recnd 11164	. . . . . . . . 9 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ ℂ)
224	223, 185	neg2subd 11513	. . . . . . . 8 ⊢ (𝜑 → (-(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − -𝐸) = (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
225	220, 222, 224	3brtr3d 5117	. . . . . . 7 ⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 − (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) ≤ (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
226	221, 143	negsubdi2d 11512	. . . . . . 7 ⊢ (𝜑 → -((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) = (⦋𝑋 / 𝑥⦌𝐵 − (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
227	223, 185	negsubdi2d 11512	. . . . . . 7 ⊢ (𝜑 → -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) = (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
228	225, 226, 227	3brtr4d 5118	. . . . . 6 ⊢ (𝜑 → -((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸))
229	98, 91	lenegd 11720	. . . . . 6 ⊢ (𝜑 → (((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ↔ -((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸)))
230	228, 229	mpbird 257	. . . . 5 ⊢ (𝜑 → ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵))
231	73, 98, 91, 116, 230	letrd 11294	. . . 4 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵))
232		1red 11136	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℝ)
233		nfv 1916	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝐷 ≤ 𝑋
234		nfcv 2899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥0
235		nfcv 2899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 ≤
236	234, 235, 161	nfbr 5133	. . . . . . . . . . 11 ⊢ Ⅎ𝑥0 ≤ ⦋𝑋 / 𝑥⦌𝐵
237	233, 236	nfim 1898	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝐷 ≤ 𝑋 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)
238		breq2 5090	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑋))
239	171	breq2d 5098	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (0 ≤ 𝐵 ↔ 0 ≤ ⦋𝑋 / 𝑥⦌𝐵))
240	238, 239	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝐷 ≤ 𝑥 → 0 ≤ 𝐵) ↔ (𝐷 ≤ 𝑋 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)))
241	237, 240	rspc 3553	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 0 ≤ 𝐵) → (𝐷 ≤ 𝑋 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)))
242	33, 103, 105, 241	syl3c 66	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)
243		fracle1 13753	. . . . . . . . 9 ⊢ (𝑋 ∈ ℝ → (𝑋 − (⌊‘𝑋)) ≤ 1)
244	74, 243	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ≤ 1)
245	77, 232, 88, 242, 244	lemul1ad 12086	. . . . . . 7 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ≤ (1 · ⦋𝑋 / 𝑥⦌𝐵))
246	143	mullidd 11154	. . . . . . 7 ⊢ (𝜑 → (1 · ⦋𝑋 / 𝑥⦌𝐵) = ⦋𝑋 / 𝑥⦌𝐵)
247	245, 246	breqtrd 5112	. . . . . 6 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ≤ ⦋𝑋 / 𝑥⦌𝐵)
248	89, 88, 45, 247	leadd1dd 11755	. . . . 5 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (⦋𝑋 / 𝑥⦌𝐵 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
249	90, 88, 45	lesubadd2d 11740	. . . . 5 ⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ↔ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (⦋𝑋 / 𝑥⦌𝐵 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
250	248, 249	mpbird 257	. . . 4 ⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
251	73, 91, 45, 231, 250	letrd 11294	. . 3 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
252	21, 72	readdcld 11165	. . . 4 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸) ∈ ℝ)
253		fracge0 13754	. . . . . . 7 ⊢ (𝑋 ∈ ℝ → 0 ≤ (𝑋 − (⌊‘𝑋)))
254	74, 253	syl 17	. . . . . 6 ⊢ (𝜑 → 0 ≤ (𝑋 − (⌊‘𝑋)))
255	77, 88, 254, 242	mulge0d 11718	. . . . 5 ⊢ (𝜑 → 0 ≤ ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵))
256	45, 89	addge02d 11730	. . . . 5 ⊢ (𝜑 → (0 ≤ ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ↔ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
257	255, 256	mpbid 232	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
258	140	simpld 494	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) ≤ ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋))
259	258, 216, 180	3brtr3d 5117	. . . . . 6 ⊢ (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
260	90, 97	lenegd 11720	. . . . . 6 ⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ↔ -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
261	259, 260	mpbird 257	. . . . 5 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
262		fracle1 13753	. . . . . . . . . 10 ⊢ (𝑌 ∈ ℝ → (𝑌 − (⌊‘𝑌)) ≤ 1)
263	92, 262	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑌 − (⌊‘𝑌)) ≤ 1)
264	95, 232, 72, 112, 263	lemul1ad 12086	. . . . . . . 8 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ≤ (1 · 𝐸))
265	185	mullidd 11154	. . . . . . . 8 ⊢ (𝜑 → (1 · 𝐸) = 𝐸)
266	264, 265	breqtrd 5112	. . . . . . 7 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ≤ 𝐸)
267	96, 72, 21, 266	leadd1dd 11755	. . . . . 6 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ (𝐸 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
268	185, 57	addcomd 11339	. . . . . 6 ⊢ (𝜑 → (𝐸 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))
269	267, 268	breqtrd 5112	. . . . 5 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))
270	90, 97, 252, 261, 269	letrd 11294	. . . 4 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))
271	45, 90, 252, 257, 270	letrd 11294	. . 3 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))
272	45, 21, 72	absdifled 15390	. . 3 ⊢ (𝜑 → ((abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) ≤ 𝐸 ↔ (((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))))
273	251, 271, 272	mpbir2and 714	. 2 ⊢ (𝜑 → (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) ≤ 𝐸)
274	60, 273	eqbrtrd 5108	1 ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) ≤ 𝐸)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ⦋csb 3838 ⊆ wss 3890 {cpr 4570 class class class wbr 5086 ↦ cmpt 5167 ‘cfv 6492 (class class class)co 7360 ℂcc 11027 ℝcr 11028 0cc0 11029 1c1 11030 + caddc 11032 · cmul 11034 +∞cpnf 11167 ℝ^*cxr 11169 ≤ cle 11171 − cmin 11368 -cneg 11369 ℤcz 12515 ℤ_≥cuz 12779 (,)cioo 13289 ...cfz 13452 ⌊cfl 13740 abscabs 15187 Σcsu 15639 D cdv 25840

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-inf2 9553 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107 ax-addf 11108

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-of 7624 df-om 7811 df-1st 7935 df-2nd 7936 df-supp 8104 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-1o 8398 df-2o 8399 df-er 8636 df-map 8768 df-pm 8769 df-ixp 8839 df-en 8887 df-dom 8888 df-sdom 8889 df-fin 8890 df-fsupp 9268 df-fi 9317 df-sup 9348 df-inf 9349 df-oi 9418 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-4 12237 df-5 12238 df-6 12239 df-7 12240 df-8 12241 df-9 12242 df-n0 12429 df-z 12516 df-dec 12636 df-uz 12780 df-q 12890 df-rp 12934 df-xneg 13054 df-xadd 13055 df-xmul 13056 df-ioo 13293 df-ico 13295 df-icc 13296 df-fz 13453 df-fzo 13600 df-fl 13742 df-seq 13955 df-exp 14015 df-hash 14284 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-clim 15441 df-sum 15640 df-struct 17108 df-sets 17125 df-slot 17143 df-ndx 17155 df-base 17171 df-ress 17192 df-plusg 17224 df-mulr 17225 df-starv 17226 df-sca 17227 df-vsca 17228 df-ip 17229 df-tset 17230 df-ple 17231 df-ds 17233 df-unif 17234 df-hom 17235 df-cco 17236 df-rest 17376 df-topn 17377 df-0g 17395 df-gsum 17396 df-topgen 17397 df-pt 17398 df-prds 17401 df-xrs 17457 df-qtop 17462 df-imas 17463 df-xps 17465 df-mre 17539 df-mrc 17540 df-acs 17542 df-mgm 18599 df-sgrp 18678 df-mnd 18694 df-submnd 18743 df-mulg 19035 df-cntz 19283 df-cmn 19748 df-psmet 21336 df-xmet 21337 df-met 21338 df-bl 21339 df-mopn 21340 df-fbas 21341 df-fg 21342 df-cnfld 21345 df-top 22869 df-topon 22886 df-topsp 22908 df-bases 22921 df-cld 22994 df-ntr 22995 df-cls 22996 df-nei 23073 df-lp 23111 df-perf 23112 df-cn 23202 df-cnp 23203 df-haus 23290 df-cmp 23362 df-tx 23537 df-hmeo 23730 df-fil 23821 df-fm 23913 df-flim 23914 df-flf 23915 df-xms 24295 df-ms 24296 df-tms 24297 df-cncf 24855 df-limc 25843 df-dv 25844

This theorem is referenced by: logfacbnd3 27200 log2sumbnd 27521

W3C validator