Theorem dvfsum2 24718

Description: The reverse of dvfsumrlim 24715, 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 13375	. . . . . . . 8 ⊢ (𝜑 → (𝑀...(⌊‘𝑌)) ∈ Fin)
3		dvfsum2.b2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)
4	3	ralrimiva 3111	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝑍 𝐵 ∈ ℝ)
5		elfzuz 12937	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑀...(⌊‘𝑌)) → 𝑘 ∈ (ℤ≥‘𝑀))
6		dvfsum2.z	. . . . . . . . . 10 ⊢ 𝑍 = (ℤ≥‘𝑀)
7	5, 6	eleqtrrdi 2862	. . . . . . . . 9 ⊢ (𝑘 ∈ (𝑀...(⌊‘𝑌)) → 𝑘 ∈ 𝑍)
8		dvfsum2.c	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)
9	8	eleq1d 2835	. . . . . . . . . 10 ⊢ (𝑥 = 𝑘 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ))
10	9	rspccva 3538	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝑍 𝐵 ∈ ℝ ∧ 𝑘 ∈ 𝑍) → 𝐶 ∈ ℝ)
11	4, 7, 10	syl2an 599	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑌))) → 𝐶 ∈ ℝ)
12	2, 11	fsumrecl 15124	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 ∈ ℝ)
13		dvfsum2.a	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)
14	13	ralrimiva 3111	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ)
15		nfcsb1v 3825	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑌 / 𝑥⦌𝐴
16	15	nfel1 2933	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ
17		csbeq1a 3815	. . . . . . . . . 10 ⊢ (𝑥 = 𝑌 → 𝐴 = ⦋𝑌 / 𝑥⦌𝐴)
18	17	eleq1d 2835	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → (𝐴 ∈ ℝ ↔ ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ))
19	16, 18	rspc 3527	. . . . . . . 8 ⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ))
20	1, 14, 19	sylc 65	. . . . . . 7 ⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ)
21	12, 20	resubcld 11091	. . . . . 6 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ)
22		nfcv 2917	. . . . . . 7 ⊢ Ⅎ𝑥𝑌
23		nfcv 2917	. . . . . . . 8 ⊢ Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶
24		nfcv 2917	. . . . . . . 8 ⊢ Ⅎ𝑥 −
25	23, 24, 15	nfov 7173	. . . . . . 7 ⊢ Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)
26		fveq2 6651	. . . . . . . . . 10 ⊢ (𝑥 = 𝑌 → (⌊‘𝑥) = (⌊‘𝑌))
27	26	oveq2d 7159	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → (𝑀...(⌊‘𝑥)) = (𝑀...(⌊‘𝑌)))
28	27	sumeq1d 15091	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶)
29	28, 17	oveq12d 7161	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))
30		dvfsum2.g	. . . . . . 7 ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))
31	22, 25, 29, 30	fvmptf 6773	. . . . . 6 ⊢ ((𝑌 ∈ 𝑆 ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) → (𝐺‘𝑌) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))
32	1, 21, 31	syl2anc 588	. . . . 5 ⊢ (𝜑 → (𝐺‘𝑌) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))
33		dvfsum2.1	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑆)
34		fzfid 13375	. . . . . . . 8 ⊢ (𝜑 → (𝑀...(⌊‘𝑋)) ∈ Fin)
35		elfzuz 12937	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ (ℤ≥‘𝑀))
36	35, 6	eleqtrrdi 2862	. . . . . . . . 9 ⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ 𝑍)
37	4, 36, 10	syl2an 599	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℝ)
38	34, 37	fsumrecl 15124	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℝ)
39		nfcsb1v 3825	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐴
40	39	nfel1 2933	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ
41		csbeq1a 3815	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → 𝐴 = ⦋𝑋 / 𝑥⦌𝐴)
42	41	eleq1d 2835	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝐴 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ))
43	40, 42	rspc 3527	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ))
44	33, 14, 43	sylc 65	. . . . . . 7 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ)
45	38, 44	resubcld 11091	. . . . . 6 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ)
46		nfcv 2917	. . . . . . 7 ⊢ Ⅎ𝑥𝑋
47		nfcv 2917	. . . . . . . 8 ⊢ Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶
48	47, 24, 39	nfov 7173	. . . . . . 7 ⊢ Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)
49		fveq2 6651	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (⌊‘𝑥) = (⌊‘𝑋))
50	49	oveq2d 7159	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑀...(⌊‘𝑥)) = (𝑀...(⌊‘𝑋)))
51	50	sumeq1d 15091	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)
52	51, 41	oveq12d 7161	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
53	46, 48, 52, 30	fvmptf 6773	. . . . . 6 ⊢ ((𝑋 ∈ 𝑆 ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) → (𝐺‘𝑋) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
54	33, 45, 53	syl2anc 588	. . . . 5 ⊢ (𝜑 → (𝐺‘𝑋) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
55	32, 54	oveq12d 7161	. . . 4 ⊢ (𝜑 → ((𝐺‘𝑌) − (𝐺‘𝑋)) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
56	55	fveq2d 6655	. . 3 ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
57	21	recnd 10692	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℂ)
58	45	recnd 10692	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℂ)
59	57, 58	abssubd 14846	. . 3 ⊢ (𝜑 → (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
60	56, 59	eqtrd 2794	. 2 ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
61		dvfsum2.s	. . . . . . . . . 10 ⊢ 𝑆 = (𝑇(,)+∞)
62		ioossre 12825	. . . . . . . . . 10 ⊢ (𝑇(,)+∞) ⊆ ℝ
63	61, 62	eqsstri 3922	. . . . . . . . 9 ⊢ 𝑆 ⊆ ℝ
64	63	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ⊆ ℝ)
65		dvfsum2.b1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)
66		dvfsum2.b3	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))
67	64, 13, 65, 66	dvmptrecl 24708	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ)
68	67	ralrimiva 3111	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ)
69		dvfsum2.e	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐸)
70	69	eleq1d 2835	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝐵 ∈ ℝ ↔ 𝐸 ∈ ℝ))
71	70	rspcv 3534	. . . . . 6 ⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ → 𝐸 ∈ ℝ))
72	1, 68, 71	sylc 65	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ℝ)
73	21, 72	resubcld 11091	. . . 4 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ∈ ℝ)
74	63, 33	sseldi 3886	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ ℝ)
75		reflcl 13200	. . . . . . . . 9 ⊢ (𝑋 ∈ ℝ → (⌊‘𝑋) ∈ ℝ)
76	74, 75	syl 17	. . . . . . . 8 ⊢ (𝜑 → (⌊‘𝑋) ∈ ℝ)
77	74, 76	resubcld 11091	. . . . . . 7 ⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℝ)
78		nfv 1916	. . . . . . . . . 10 ⊢ Ⅎ𝑚 𝐵 ∈ ℝ
79		nfcsb1v 3825	. . . . . . . . . . 11 ⊢ Ⅎ𝑥⦋𝑚 / 𝑥⦌𝐵
80	79	nfel1 2933	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ
81		csbeq1a 3815	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑥⦌𝐵)
82	81	eleq1d 2835	. . . . . . . . . 10 ⊢ (𝑥 = 𝑚 → (𝐵 ∈ ℝ ↔ ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ))
83	78, 80, 82	cbvralw 3350	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ ↔ ∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ)
84	68, 83	sylib 221	. . . . . . . 8 ⊢ (𝜑 → ∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ)
85		csbeq1 3804	. . . . . . . . . 10 ⊢ (𝑚 = 𝑋 → ⦋𝑚 / 𝑥⦌𝐵 = ⦋𝑋 / 𝑥⦌𝐵)
86	85	eleq1d 2835	. . . . . . . . 9 ⊢ (𝑚 = 𝑋 → (⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ))
87	86	rspcv 3534	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑆 → (∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ))
88	33, 84, 87	sylc 65	. . . . . . 7 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ)
89	77, 88	remulcld 10694	. . . . . 6 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ)
90	89, 45	readdcld 10693	. . . . 5 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ)
91	90, 88	resubcld 11091	. . . 4 ⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ)
92	63, 1	sseldi 3886	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ ℝ)
93		reflcl 13200	. . . . . . . . . 10 ⊢ (𝑌 ∈ ℝ → (⌊‘𝑌) ∈ ℝ)
94	92, 93	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (⌊‘𝑌) ∈ ℝ)
95	92, 94	resubcld 11091	. . . . . . . 8 ⊢ (𝜑 → (𝑌 − (⌊‘𝑌)) ∈ ℝ)
96	95, 72	remulcld 10694	. . . . . . 7 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ∈ ℝ)
97	96, 21	readdcld 10693	. . . . . 6 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ)
98	97, 72	resubcld 11091	. . . . 5 ⊢ (𝜑 → ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) ∈ ℝ)
99		fracge0 13208	. . . . . . . . 9 ⊢ (𝑌 ∈ ℝ → 0 ≤ (𝑌 − (⌊‘𝑌)))
100	92, 99	syl 17	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ (𝑌 − (⌊‘𝑌)))
101		dvfsum2.0	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵)
102	101	expr 461	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷 ≤ 𝑥 → 0 ≤ 𝐵))
103	102	ralrimiva 3111	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 0 ≤ 𝐵))
104		dvfsum2.d	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℝ)
105		dvfsum2.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ≤ 𝑋)
106		dvfsum2.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ≤ 𝑌)
107	104, 74, 92, 105, 106	letrd 10820	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≤ 𝑌)
108		breq2 5029	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑌 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑌))
109	69	breq2d 5037	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑌 → (0 ≤ 𝐵 ↔ 0 ≤ 𝐸))
110	108, 109	imbi12d 349	. . . . . . . . . 10 ⊢ (𝑥 = 𝑌 → ((𝐷 ≤ 𝑥 → 0 ≤ 𝐵) ↔ (𝐷 ≤ 𝑌 → 0 ≤ 𝐸)))
111	110	rspcv 3534	. . . . . . . . 9 ⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 0 ≤ 𝐵) → (𝐷 ≤ 𝑌 → 0 ≤ 𝐸)))
112	1, 103, 107, 111	syl3c 66	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 𝐸)
113	95, 72, 100, 112	mulge0d 11240	. . . . . . 7 ⊢ (𝜑 → 0 ≤ ((𝑌 − (⌊‘𝑌)) · 𝐸))
114	21, 96	addge02d 11252	. . . . . . 7 ⊢ (𝜑 → (0 ≤ ((𝑌 − (⌊‘𝑌)) · 𝐸) ↔ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
115	113, 114	mpbid 235	. . . . . 6 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
116	21, 97, 72, 115	lesub1dd 11279	. . . . 5 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸))
117		dvfsum2.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℤ)
118		dvfsum2.md	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))
119		dvfsum2.t	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ ℝ)
120	13	renegcld 11090	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → -𝐴 ∈ ℝ)
121	67	renegcld 11090	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → -𝐵 ∈ ℝ)
122	3	renegcld 11090	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → -𝐵 ∈ ℝ)
123		reelprrecn 10652	. . . . . . . . . . . . 13 ⊢ ℝ ∈ {ℝ, ℂ}
124	123	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
125	13	recnd 10692	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℂ)
126	124, 125, 65, 66	dvmptneg 24650	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ -𝐴)) = (𝑥 ∈ 𝑆 ↦ -𝐵))
127	8	negeqd 10903	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑘 → -𝐵 = -𝐶)
128		dvfsum2.u	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ ℝ*)
129		dvfsum2.l	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐵 ≤ 𝐶)
130	67	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) → 𝐵 ∈ ℝ)
131	130	3adant3 1130	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐵 ∈ ℝ)
132		simp2r 1198	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝑘 ∈ 𝑆)
133	68	3ad2ant1 1131	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ)
134	9	rspcv 3534	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ → 𝐶 ∈ ℝ))
135	132, 133, 134	sylc 65	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ∈ ℝ)
136	131, 135	lenegd 11242	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → (𝐵 ≤ 𝐶 ↔ -𝐶 ≤ -𝐵))
137	129, 136	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → -𝐶 ≤ -𝐵)
138		eqid 2759	. . . . . . . . . . 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 24712	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) ≤ ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) ∧ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌-𝐵) ≤ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌-𝐵)))
141	140	simprd 500	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌-𝐵) ≤ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌-𝐵))
142	77	recnd 10692	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℂ)
143	88	recnd 10692	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℂ)
144	142, 143	mulneg2d 11117	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) = -((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵))
145	38	recnd 10692	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℂ)
146	44	recnd 10692	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℂ)
147	145, 146	neg2subd 11037	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (-Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − -⦋𝑋 / 𝑥⦌𝐴) = (⦋𝑋 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
148	37	recnd 10692	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℂ)
149	34, 148	fsumneg 15175	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 = -Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)
150	149	oveq1d 7158	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴) = (-Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − -⦋𝑋 / 𝑥⦌𝐴))
151	145, 146	negsubdi2d 11036	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) = (⦋𝑋 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
152	147, 150, 151	3eqtr4d 2804	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴) = -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
153	144, 152	oveq12d 7161	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) = (-((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
154	89	recnd 10692	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℂ)
155	154, 58	negdid 11033	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) = (-((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
156	153, 155	eqtr4d 2797	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) = -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
157	90	renegcld 11090	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ)
158	156, 157	eqeltrd 2851	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ)
159		nfcv 2917	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑋 − (⌊‘𝑋))
160		nfcv 2917	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 ·
161		nfcsb1v 3825	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐵
162	161	nfneg 10905	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥-⦋𝑋 / 𝑥⦌𝐵
163	159, 160, 162	nfov 7173	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵)
164		nfcv 2917	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥 +
165		nfcv 2917	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶
166	39	nfneg 10905	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥-⦋𝑋 / 𝑥⦌𝐴
167	165, 24, 166	nfov 7173	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)
168	163, 164, 167	nfov 7173	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴))
169		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
170	169, 49	oveq12d 7161	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → (𝑥 − (⌊‘𝑥)) = (𝑋 − (⌊‘𝑋)))
171		csbeq1a 3815	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → 𝐵 = ⦋𝑋 / 𝑥⦌𝐵)
172	171	negeqd 10903	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → -𝐵 = -⦋𝑋 / 𝑥⦌𝐵)
173	170, 172	oveq12d 7161	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → ((𝑥 − (⌊‘𝑥)) · -𝐵) = ((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵))
174	50	sumeq1d 15091	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶)
175	41	negeqd 10903	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → -𝐴 = -⦋𝑋 / 𝑥⦌𝐴)
176	174, 175	oveq12d 7161	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴))
177	173, 176	oveq12d 7161	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)) = (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)))
178	46, 168, 177, 138	fvmptf 6773	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑆 ∧ (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ) → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) = (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)))
179	33, 158, 178	syl2anc 588	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) = (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)))
180	179, 156	eqtrd 2794	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) = -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
181		csbnegg 10906	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝑆 → ⦋𝑋 / 𝑥⦌-𝐵 = -⦋𝑋 / 𝑥⦌𝐵)
182	33, 181	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌-𝐵 = -⦋𝑋 / 𝑥⦌𝐵)
183	180, 182	oveq12d 7161	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌-𝐵) = (-(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − -⦋𝑋 / 𝑥⦌𝐵))
184	95	recnd 10692	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 − (⌊‘𝑌)) ∈ ℂ)
185	72	recnd 10692	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 ∈ ℂ)
186	184, 185	mulneg2d 11117	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · -𝐸) = -((𝑌 − (⌊‘𝑌)) · 𝐸))
187	12	recnd 10692	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 ∈ ℂ)
188	20	recnd 10692	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℂ)
189	187, 188	neg2subd 11037	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (-Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − -⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶))
190	11	recnd 10692	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑌))) → 𝐶 ∈ ℂ)
191	2, 190	fsumneg 15175	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 = -Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶)
192	191	oveq1d 7158	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴) = (-Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − -⦋𝑌 / 𝑥⦌𝐴))
193	187, 188	negsubdi2d 11036	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶))
194	189, 192, 193	3eqtr4d 2804	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴) = -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))
195	186, 194	oveq12d 7161	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) = (-((𝑌 − (⌊‘𝑌)) · 𝐸) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
196	96	recnd 10692	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ∈ ℂ)
197	196, 57	negdid 11033	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) = (-((𝑌 − (⌊‘𝑌)) · 𝐸) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
198	195, 197	eqtr4d 2797	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) = -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
199	97	renegcld 11090	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ)
200	198, 199	eqeltrd 2851	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ)
201		nfcv 2917	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑌 − (⌊‘𝑌)) · -𝐸)
202		nfcv 2917	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶
203	15	nfneg 10905	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥-⦋𝑌 / 𝑥⦌𝐴
204	202, 24, 203	nfov 7173	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)
205	201, 164, 204	nfov 7173	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴))
206		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑌 → 𝑥 = 𝑌)
207	206, 26	oveq12d 7161	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → (𝑥 − (⌊‘𝑥)) = (𝑌 − (⌊‘𝑌)))
208	69	negeqd 10903	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → -𝐵 = -𝐸)
209	207, 208	oveq12d 7161	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑌 → ((𝑥 − (⌊‘𝑥)) · -𝐵) = ((𝑌 − (⌊‘𝑌)) · -𝐸))
210	27	sumeq1d 15091	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶)
211	17	negeqd 10903	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → -𝐴 = -⦋𝑌 / 𝑥⦌𝐴)
212	210, 211	oveq12d 7161	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑌 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴))
213	209, 212	oveq12d 7161	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑌 → (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)))
214	22, 205, 213, 138	fvmptf 6773	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ 𝑆 ∧ (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ) → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)))
215	1, 200, 214	syl2anc 588	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)))
216	215, 198	eqtrd 2794	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) = -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
217	208	adantl 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = 𝑌) → -𝐵 = -𝐸)
218	1, 217	csbied 3837	. . . . . . . . . 10 ⊢ (𝜑 → ⦋𝑌 / 𝑥⦌-𝐵 = -𝐸)
219	216, 218	oveq12d 7161	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌-𝐵) = (-(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − -𝐸))
220	141, 183, 219	3brtr3d 5056	. . . . . . . 8 ⊢ (𝜑 → (-(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − -⦋𝑋 / 𝑥⦌𝐵) ≤ (-(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − -𝐸))
221	90	recnd 10692	. . . . . . . . 9 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℂ)
222	221, 143	neg2subd 11037	. . . . . . . 8 ⊢ (𝜑 → (-(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − -⦋𝑋 / 𝑥⦌𝐵) = (⦋𝑋 / 𝑥⦌𝐵 − (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
223	97	recnd 10692	. . . . . . . . 9 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ ℂ)
224	223, 185	neg2subd 11037	. . . . . . . 8 ⊢ (𝜑 → (-(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − -𝐸) = (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
225	220, 222, 224	3brtr3d 5056	. . . . . . 7 ⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 − (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) ≤ (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
226	221, 143	negsubdi2d 11036	. . . . . . 7 ⊢ (𝜑 → -((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) = (⦋𝑋 / 𝑥⦌𝐵 − (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
227	223, 185	negsubdi2d 11036	. . . . . . 7 ⊢ (𝜑 → -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) = (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
228	225, 226, 227	3brtr4d 5057	. . . . . 6 ⊢ (𝜑 → -((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸))
229	98, 91	lenegd 11242	. . . . . 6 ⊢ (𝜑 → (((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ↔ -((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸)))
230	228, 229	mpbird 260	. . . . 5 ⊢ (𝜑 → ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵))
231	73, 98, 91, 116, 230	letrd 10820	. . . 4 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵))
232		1red 10665	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℝ)
233		nfv 1916	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝐷 ≤ 𝑋
234		nfcv 2917	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥0
235		nfcv 2917	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 ≤
236	234, 235, 161	nfbr 5072	. . . . . . . . . . 11 ⊢ Ⅎ𝑥0 ≤ ⦋𝑋 / 𝑥⦌𝐵
237	233, 236	nfim 1898	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝐷 ≤ 𝑋 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)
238		breq2 5029	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑋))
239	171	breq2d 5037	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (0 ≤ 𝐵 ↔ 0 ≤ ⦋𝑋 / 𝑥⦌𝐵))
240	238, 239	imbi12d 349	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝐷 ≤ 𝑥 → 0 ≤ 𝐵) ↔ (𝐷 ≤ 𝑋 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)))
241	237, 240	rspc 3527	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 0 ≤ 𝐵) → (𝐷 ≤ 𝑋 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)))
242	33, 103, 105, 241	syl3c 66	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)
243		fracle1 13207	. . . . . . . . 9 ⊢ (𝑋 ∈ ℝ → (𝑋 − (⌊‘𝑋)) ≤ 1)
244	74, 243	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ≤ 1)
245	77, 232, 88, 242, 244	lemul1ad 11602	. . . . . . 7 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ≤ (1 · ⦋𝑋 / 𝑥⦌𝐵))
246	143	mulid2d 10682	. . . . . . 7 ⊢ (𝜑 → (1 · ⦋𝑋 / 𝑥⦌𝐵) = ⦋𝑋 / 𝑥⦌𝐵)
247	245, 246	breqtrd 5051	. . . . . 6 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ≤ ⦋𝑋 / 𝑥⦌𝐵)
248	89, 88, 45, 247	leadd1dd 11277	. . . . 5 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (⦋𝑋 / 𝑥⦌𝐵 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
249	90, 88, 45	lesubadd2d 11262	. . . . 5 ⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ↔ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (⦋𝑋 / 𝑥⦌𝐵 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
250	248, 249	mpbird 260	. . . 4 ⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
251	73, 91, 45, 231, 250	letrd 10820	. . 3 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
252	21, 72	readdcld 10693	. . . 4 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸) ∈ ℝ)
253		fracge0 13208	. . . . . . 7 ⊢ (𝑋 ∈ ℝ → 0 ≤ (𝑋 − (⌊‘𝑋)))
254	74, 253	syl 17	. . . . . 6 ⊢ (𝜑 → 0 ≤ (𝑋 − (⌊‘𝑋)))
255	77, 88, 254, 242	mulge0d 11240	. . . . 5 ⊢ (𝜑 → 0 ≤ ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵))
256	45, 89	addge02d 11252	. . . . 5 ⊢ (𝜑 → (0 ≤ ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ↔ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
257	255, 256	mpbid 235	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
258	140	simpld 499	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) ≤ ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋))
259	258, 216, 180	3brtr3d 5056	. . . . . 6 ⊢ (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
260	90, 97	lenegd 11242	. . . . . 6 ⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ↔ -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
261	259, 260	mpbird 260	. . . . 5 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
262		fracle1 13207	. . . . . . . . . 10 ⊢ (𝑌 ∈ ℝ → (𝑌 − (⌊‘𝑌)) ≤ 1)
263	92, 262	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑌 − (⌊‘𝑌)) ≤ 1)
264	95, 232, 72, 112, 263	lemul1ad 11602	. . . . . . . 8 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ≤ (1 · 𝐸))
265	185	mulid2d 10682	. . . . . . . 8 ⊢ (𝜑 → (1 · 𝐸) = 𝐸)
266	264, 265	breqtrd 5051	. . . . . . 7 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ≤ 𝐸)
267	96, 72, 21, 266	leadd1dd 11277	. . . . . 6 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ (𝐸 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
268	185, 57	addcomd 10865	. . . . . 6 ⊢ (𝜑 → (𝐸 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))
269	267, 268	breqtrd 5051	. . . . 5 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))
270	90, 97, 252, 261, 269	letrd 10820	. . . 4 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))
271	45, 90, 252, 257, 270	letrd 10820	. . 3 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))
272	45, 21, 72	absdifled 14827	. . 3 ⊢ (𝜑 → ((abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) ≤ 𝐸 ↔ (((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))))
273	251, 271, 272	mpbir2and 713	. 2 ⊢ (𝜑 → (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) ≤ 𝐸)
274	60, 273	eqbrtrd 5047	1 ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) ≤ 𝐸)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112  ∀wral 3068  ⦋csb 3801   ⊆ wss 3854  {cpr 4517   class class class wbr 5025   ↦ cmpt 5105  ‘cfv 6328  (class class class)co 7143  ℂcc 10558  ℝcr 10559  0cc0 10560  1c1 10561   + caddc 10563   · cmul 10565  +∞cpnf 10695  ℝ^*cxr 10697   ≤ cle 10699   − cmin 10893  -cneg 10894  ℤcz 12005  ℤ_≥cuz 12267  (,)cioo 12764  ...cfz 12924  ⌊cfl 13194  abscabs 14626  Σcsu 15075   D cdv 24547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5149  ax-sep 5162  ax-nul 5169  ax-pow 5227  ax-pr 5291  ax-un 7452  ax-inf2 9122  ax-cnex 10616  ax-resscn 10617  ax-1cn 10618  ax-icn 10619  ax-addcl 10620  ax-addrcl 10621  ax-mulcl 10622  ax-mulrcl 10623  ax-mulcom 10624  ax-addass 10625  ax-mulass 10626  ax-distr 10627  ax-i2m1 10628  ax-1ne0 10629  ax-1rid 10630  ax-rnegex 10631  ax-rrecex 10632  ax-cnre 10633  ax-pre-lttri 10634  ax-pre-lttrn 10635  ax-pre-ltadd 10636  ax-pre-mulgt0 10637  ax-pre-sup 10638  ax-addf 10639  ax-mulf 10640

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-nel 3054  df-ral 3073  df-rex 3074  df-reu 3075  df-rmo 3076  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-pss 3873  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-tp 4520  df-op 4522  df-uni 4792  df-int 4832  df-iun 4878  df-iin 4879  df-br 5026  df-opab 5088  df-mpt 5106  df-tr 5132  df-id 5423  df-eprel 5428  df-po 5436  df-so 5437  df-fr 5476  df-se 5477  df-we 5478  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7101  df-ov 7146  df-oprab 7147  df-mpo 7148  df-of 7398  df-om 7573  df-1st 7686  df-2nd 7687  df-supp 7829  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-1o 8105  df-2o 8106  df-oadd 8109  df-er 8292  df-map 8411  df-pm 8412  df-ixp 8473  df-en 8521  df-dom 8522  df-sdom 8523  df-fin 8524  df-fsupp 8852  df-fi 8893  df-sup 8924  df-inf 8925  df-oi 8992  df-card 9386  df-pnf 10700  df-mnf 10701  df-xr 10702  df-ltxr 10703  df-le 10704  df-sub 10895  df-neg 10896  df-div 11321  df-nn 11660  df-2 11722  df-3 11723  df-4 11724  df-5 11725  df-6 11726  df-7 11727  df-8 11728  df-9 11729  df-n0 11920  df-z 12006  df-dec 12123  df-uz 12268  df-q 12374  df-rp 12416  df-xneg 12533  df-xadd 12534  df-xmul 12535  df-ioo 12768  df-ico 12770  df-icc 12771  df-fz 12925  df-fzo 13068  df-fl 13196  df-seq 13404  df-exp 13465  df-hash 13726  df-cj 14491  df-re 14492  df-im 14493  df-sqrt 14627  df-abs 14628  df-clim 14878  df-sum 15076  df-struct 16528  df-ndx 16529  df-slot 16530  df-base 16532  df-sets 16533  df-ress 16534  df-plusg 16621  df-mulr 16622  df-starv 16623  df-sca 16624  df-vsca 16625  df-ip 16626  df-tset 16627  df-ple 16628  df-ds 16630  df-unif 16631  df-hom 16632  df-cco 16633  df-rest 16739  df-topn 16740  df-0g 16758  df-gsum 16759  df-topgen 16760  df-pt 16761  df-prds 16764  df-xrs 16818  df-qtop 16823  df-imas 16824  df-xps 16826  df-mre 16900  df-mrc 16901  df-acs 16903  df-mgm 17903  df-sgrp 17952  df-mnd 17963  df-submnd 18008  df-mulg 18277  df-cntz 18499  df-cmn 18960  df-psmet 20143  df-xmet 20144  df-met 20145  df-bl 20146  df-mopn 20147  df-fbas 20148  df-fg 20149  df-cnfld 20152  df-top 21579  df-topon 21596  df-topsp 21618  df-bases 21631  df-cld 21704  df-ntr 21705  df-cls 21706  df-nei 21783  df-lp 21821  df-perf 21822  df-cn 21912  df-cnp 21913  df-haus 22000  df-cmp 22072  df-tx 22247  df-hmeo 22440  df-fil 22531  df-fm 22623  df-flim 22624  df-flf 22625  df-xms 23007  df-ms 23008  df-tms 23009  df-cncf 23564  df-limc 24550  df-dv 24551

This theorem is referenced by:  logfacbnd3  25891  log2sumbnd  26212