Theorem dvfsum2 26360

Description: The reverse of dvfsumrlim 26357, 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 14120	. . . . . . . 8 ⊢ (𝜑 → (𝑀...(⌊‘𝑌)) ∈ Fin)
3		dvfsum2.b2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)
4	3	ralrimiva 3154	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝑍 𝐵 ∈ ℝ)
5		elfzuz 13656	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑀...(⌊‘𝑌)) → 𝑘 ∈ (ℤ≥‘𝑀))
6		dvfsum2.z	. . . . . . . . . 10 ⊢ 𝑍 = (ℤ≥‘𝑀)
7	5, 6	eleqtrrdi 2871	. . . . . . . . 9 ⊢ (𝑘 ∈ (𝑀...(⌊‘𝑌)) → 𝑘 ∈ 𝑍)
8		dvfsum2.c	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)
9	8	eleq1d 2845	. . . . . . . . . 10 ⊢ (𝑥 = 𝑘 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ))
10	9	rspccva 3575	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝑍 𝐵 ∈ ℝ ∧ 𝑘 ∈ 𝑍) → 𝐶 ∈ ℝ)
11	4, 7, 10	syl2an 608	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑌))) → 𝐶 ∈ ℝ)
12	2, 11	fsumrecl 15906	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 ∈ ℝ)
13		dvfsum2.a	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)
14	13	ralrimiva 3154	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ)
15		nfcsb1v 3870	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑌 / 𝑥⦌𝐴
16	15	nfel1 2938	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ
17		csbeq1a 3860	. . . . . . . . . 10 ⊢ (𝑥 = 𝑌 → 𝐴 = ⦋𝑌 / 𝑥⦌𝐴)
18	17	eleq1d 2845	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → (𝐴 ∈ ℝ ↔ ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ))
19	16, 18	rspc 3564	. . . . . . . 8 ⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ))
20	1, 14, 19	sylc 66	. . . . . . 7 ⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ)
21	12, 20	resubcld 11748	. . . . . 6 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ)
22		nfcv 2922	. . . . . . 7 ⊢ Ⅎ𝑥𝑌
23		nfcv 2922	. . . . . . . 8 ⊢ Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶
24		nfcv 2922	. . . . . . . 8 ⊢ Ⅎ𝑥 −
25	23, 24, 15	nfov 7451	. . . . . . 7 ⊢ Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)
26		fveq2 6886	. . . . . . . . . 10 ⊢ (𝑥 = 𝑌 → (⌊‘𝑥) = (⌊‘𝑌))
27	26	oveq2d 7437	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → (𝑀...(⌊‘𝑥)) = (𝑀...(⌊‘𝑌)))
28	27	sumeq1d 15873	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶)
29	28, 17	oveq12d 7439	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))
30		dvfsum2.g	. . . . . . 7 ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))
31	22, 25, 29, 30	fvmptf 7016	. . . . . 6 ⊢ ((𝑌 ∈ 𝑆 ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) → (𝐺‘𝑌) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))
32	1, 21, 31	syl2anc 596	. . . . 5 ⊢ (𝜑 → (𝐺‘𝑌) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))
33		dvfsum2.1	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑆)
34		fzfid 14120	. . . . . . . 8 ⊢ (𝜑 → (𝑀...(⌊‘𝑋)) ∈ Fin)
35		elfzuz 13656	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ (ℤ≥‘𝑀))
36	35, 6	eleqtrrdi 2871	. . . . . . . . 9 ⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ 𝑍)
37	4, 36, 10	syl2an 608	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℝ)
38	34, 37	fsumrecl 15906	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℝ)
39		nfcsb1v 3870	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐴
40	39	nfel1 2938	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ
41		csbeq1a 3860	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → 𝐴 = ⦋𝑋 / 𝑥⦌𝐴)
42	41	eleq1d 2845	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝐴 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ))
43	40, 42	rspc 3564	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ))
44	33, 14, 43	sylc 66	. . . . . . 7 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ)
45	38, 44	resubcld 11748	. . . . . 6 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ)
46		nfcv 2922	. . . . . . 7 ⊢ Ⅎ𝑥𝑋
47		nfcv 2922	. . . . . . . 8 ⊢ Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶
48	47, 24, 39	nfov 7451	. . . . . . 7 ⊢ Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)
49		fveq2 6886	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (⌊‘𝑥) = (⌊‘𝑋))
50	49	oveq2d 7437	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑀...(⌊‘𝑥)) = (𝑀...(⌊‘𝑋)))
51	50	sumeq1d 15873	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)
52	51, 41	oveq12d 7439	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
53	46, 48, 52, 30	fvmptf 7016	. . . . . 6 ⊢ ((𝑋 ∈ 𝑆 ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) → (𝐺‘𝑋) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
54	33, 45, 53	syl2anc 596	. . . . 5 ⊢ (𝜑 → (𝐺‘𝑋) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
55	32, 54	oveq12d 7439	. . . 4 ⊢ (𝜑 → ((𝐺‘𝑌) − (𝐺‘𝑋)) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
56	55	fveq2d 6890	. . 3 ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
57	21	recnd 11341	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℂ)
58	45	recnd 11341	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℂ)
59	57, 58	abssubd 15629	. . 3 ⊢ (𝜑 → (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
60	56, 59	eqtrd 2795	. 2 ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
61		dvfsum2.s	. . . . . . . . . 10 ⊢ 𝑆 = (𝑇(,)+∞)
62		ioossre 13542	. . . . . . . . . 10 ⊢ (𝑇(,)+∞) ⊆ ℝ
63	61, 62	eqsstri 3954	. . . . . . . . 9 ⊢ 𝑆 ⊆ ℝ
64	63	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ⊆ ℝ)
65		dvfsum2.b1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)
66		dvfsum2.b3	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))
67	64, 13, 65, 66	dvmptrecl 26350	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ)
68	67	ralrimiva 3154	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ)
69		dvfsum2.e	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐸)
70	69	eleq1d 2845	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝐵 ∈ ℝ ↔ 𝐸 ∈ ℝ))
71	70	rspcv 3572	. . . . . 6 ⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ → 𝐸 ∈ ℝ))
72	1, 68, 71	sylc 66	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ℝ)
73	21, 72	resubcld 11748	. . . 4 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ∈ ℝ)
74	63, 33	sselid 3906	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ ℝ)
75		reflcl 13940	. . . . . . . . 9 ⊢ (𝑋 ∈ ℝ → (⌊‘𝑋) ∈ ℝ)
76	74, 75	syl 18	. . . . . . . 8 ⊢ (𝜑 → (⌊‘𝑋) ∈ ℝ)
77	74, 76	resubcld 11748	. . . . . . 7 ⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℝ)
78		nfv 1946	. . . . . . . . . 10 ⊢ Ⅎ𝑚 𝐵 ∈ ℝ
79		nfcsb1v 3870	. . . . . . . . . . 11 ⊢ Ⅎ𝑥⦋𝑚 / 𝑥⦌𝐵
80	79	nfel1 2938	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ
81		csbeq1a 3860	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑥⦌𝐵)
82	81	eleq1d 2845	. . . . . . . . . 10 ⊢ (𝑥 = 𝑚 → (𝐵 ∈ ℝ ↔ ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ))
83	78, 80, 82	cbvralw 3304	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ ↔ ∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ)
84	68, 83	sylib 221	. . . . . . . 8 ⊢ (𝜑 → ∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ)
85		csbeq1 3849	. . . . . . . . . 10 ⊢ (𝑚 = 𝑋 → ⦋𝑚 / 𝑥⦌𝐵 = ⦋𝑋 / 𝑥⦌𝐵)
86	85	eleq1d 2845	. . . . . . . . 9 ⊢ (𝑚 = 𝑋 → (⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ))
87	86	rspcv 3572	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑆 → (∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ))
88	33, 84, 87	sylc 66	. . . . . . 7 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ)
89	77, 88	remulcld 11343	. . . . . 6 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ)
90	89, 45	readdcld 11342	. . . . 5 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ)
91	90, 88	resubcld 11748	. . . 4 ⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ)
92	63, 1	sselid 3906	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ ℝ)
93		reflcl 13940	. . . . . . . . . 10 ⊢ (𝑌 ∈ ℝ → (⌊‘𝑌) ∈ ℝ)
94	92, 93	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (⌊‘𝑌) ∈ ℝ)
95	92, 94	resubcld 11748	. . . . . . . 8 ⊢ (𝜑 → (𝑌 − (⌊‘𝑌)) ∈ ℝ)
96	95, 72	remulcld 11343	. . . . . . 7 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ∈ ℝ)
97	96, 21	readdcld 11342	. . . . . 6 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ)
98	97, 72	resubcld 11748	. . . . 5 ⊢ (𝜑 → ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) ∈ ℝ)
99		fracge0 13948	. . . . . . . . 9 ⊢ (𝑌 ∈ ℝ → 0 ≤ (𝑌 − (⌊‘𝑌)))
100	92, 99	syl 18	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ (𝑌 − (⌊‘𝑌)))
101		dvfsum2.0	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵)
102	101	expr 462	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷 ≤ 𝑥 → 0 ≤ 𝐵))
103	102	ralrimiva 3154	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 0 ≤ 𝐵))
104		dvfsum2.d	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℝ)
105		dvfsum2.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ≤ 𝑋)
106		dvfsum2.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ≤ 𝑌)
107	104, 74, 92, 105, 106	letrd 11471	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≤ 𝑌)
108		breq2 5106	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑌 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑌))
109	69	breq2d 5114	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑌 → (0 ≤ 𝐵 ↔ 0 ≤ 𝐸))
110	108, 109	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑥 = 𝑌 → ((𝐷 ≤ 𝑥 → 0 ≤ 𝐵) ↔ (𝐷 ≤ 𝑌 → 0 ≤ 𝐸)))
111	110	rspcv 3572	. . . . . . . . 9 ⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 0 ≤ 𝐵) → (𝐷 ≤ 𝑌 → 0 ≤ 𝐸)))
112	1, 103, 107, 111	syl3c 67	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 𝐸)
113	95, 72, 100, 112	mulge0d 11897	. . . . . . 7 ⊢ (𝜑 → 0 ≤ ((𝑌 − (⌊‘𝑌)) · 𝐸))
114	21, 96	addge02d 11909	. . . . . . 7 ⊢ (𝜑 → (0 ≤ ((𝑌 − (⌊‘𝑌)) · 𝐸) ↔ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
115	113, 114	mpbid 235	. . . . . 6 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
116	21, 97, 72, 115	lesub1dd 11936	. . . . 5 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸))
117		dvfsum2.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℤ)
118		dvfsum2.md	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))
119		dvfsum2.t	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ ℝ)
120	13	renegcld 11747	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → -𝐴 ∈ ℝ)
121	67	renegcld 11747	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → -𝐵 ∈ ℝ)
122	3	renegcld 11747	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → -𝐵 ∈ ℝ)
123		reelprrecn 11296	. . . . . . . . . . . . 13 ⊢ ℝ ∈ {ℝ, ℂ}
124	123	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
125	13	recnd 11341	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℂ)
126	124, 125, 65, 66	dvmptneg 26292	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ -𝐴)) = (𝑥 ∈ 𝑆 ↦ -𝐵))
127	8	negeqd 11555	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑘 → -𝐵 = -𝐶)
128		dvfsum2.u	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ ℝ*)
129		dvfsum2.l	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐵 ≤ 𝐶)
130	67	adantrr 730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) → 𝐵 ∈ ℝ)
131	130	3adant3 1150	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐵 ∈ ℝ)
132		simp2r 1219	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝑘 ∈ 𝑆)
133	68	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ)
134	9	rspcv 3572	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ → 𝐶 ∈ ℝ))
135	132, 133, 134	sylc 66	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ∈ ℝ)
136	131, 135	lenegd 11899	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → (𝐵 ≤ 𝐶 ↔ -𝐶 ≤ -𝐵))
137	129, 136	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → -𝐶 ≤ -𝐵)
138		eqid 2760	. . . . . . . . . . 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 26354	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)))‘𝑌) ≤ ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)))‘𝑋) ∧ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌ -𝐵) ≤ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌ -𝐵)))
141	140	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌ -𝐵) ≤ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌ -𝐵))
142	77	recnd 11341	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℂ)
143	88	recnd 11341	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℂ)
144	142, 143	mulneg2d 11774	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) = -((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵))
145	38	recnd 11341	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℂ)
146	44	recnd 11341	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℂ)
147	145, 146	neg2subd 11690	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( -Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − -⦋𝑋 / 𝑥⦌𝐴) = (⦋𝑋 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
148	37	recnd 11341	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℂ)
149	34, 148	fsumneg 15959	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋)) -𝐶 = -Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)
150	149	oveq1d 7436	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋)) -𝐶 − -⦋𝑋 / 𝑥⦌𝐴) = ( -Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − -⦋𝑋 / 𝑥⦌𝐴))
151	145, 146	negsubdi2d 11689	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) = (⦋𝑋 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
152	147, 150, 151	3eqtr4d 2805	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋)) -𝐶 − -⦋𝑋 / 𝑥⦌𝐴) = -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
153	144, 152	oveq12d 7439	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋)) -𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) = ( -((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
154	89	recnd 11341	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℂ)
155	154, 58	negdid 11686	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) = ( -((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
156	153, 155	eqtr4d 2798	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋)) -𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) = -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
157	90	renegcld 11747	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ)
158	156, 157	eqeltrd 2860	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋)) -𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ)
159		nfcv 2922	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑋 − (⌊‘𝑋))
160		nfcv 2922	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 ·
161		nfcsb1v 3870	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐵
162	161	nfneg 11557	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 -⦋𝑋 / 𝑥⦌𝐵
163	159, 160, 162	nfov 7451	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵)
164		nfcv 2922	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥 +
165		nfcv 2922	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑋)) -𝐶
166	39	nfneg 11557	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 -⦋𝑋 / 𝑥⦌𝐴
167	165, 24, 166	nfov 7451	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑋)) -𝐶 − -⦋𝑋 / 𝑥⦌𝐴)
168	163, 164, 167	nfov 7451	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋)) -𝐶 − -⦋𝑋 / 𝑥⦌𝐴))
169		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
170	169, 49	oveq12d 7439	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → (𝑥 − (⌊‘𝑥)) = (𝑋 − (⌊‘𝑋)))
171		csbeq1a 3860	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → 𝐵 = ⦋𝑋 / 𝑥⦌𝐵)
172	171	negeqd 11555	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → -𝐵 = -⦋𝑋 / 𝑥⦌𝐵)
173	170, 172	oveq12d 7439	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → ((𝑥 − (⌊‘𝑥)) · -𝐵) = ((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵))
174	50	sumeq1d 15873	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑋)) -𝐶)
175	41	negeqd 11555	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → -𝐴 = -⦋𝑋 / 𝑥⦌𝐴)
176	174, 175	oveq12d 7439	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋)) -𝐶 − -⦋𝑋 / 𝑥⦌𝐴))
177	173, 176	oveq12d 7439	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)) = (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋)) -𝐶 − -⦋𝑋 / 𝑥⦌𝐴)))
178	46, 168, 177, 138	fvmptf 7016	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑆 ∧ (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋)) -𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ) → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)))‘𝑋) = (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋)) -𝐶 − -⦋𝑋 / 𝑥⦌𝐴)))
179	33, 158, 178	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)))‘𝑋) = (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋)) -𝐶 − -⦋𝑋 / 𝑥⦌𝐴)))
180	179, 156	eqtrd 2795	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)))‘𝑋) = -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
181		csbnegg 11558	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝑆 → ⦋𝑋 / 𝑥⦌ -𝐵 = -⦋𝑋 / 𝑥⦌𝐵)
182	33, 181	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌ -𝐵 = -⦋𝑋 / 𝑥⦌𝐵)
183	180, 182	oveq12d 7439	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌ -𝐵) = ( -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − -⦋𝑋 / 𝑥⦌𝐵))
184	95	recnd 11341	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 − (⌊‘𝑌)) ∈ ℂ)
185	72	recnd 11341	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 ∈ ℂ)
186	184, 185	mulneg2d 11774	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · -𝐸) = -((𝑌 − (⌊‘𝑌)) · 𝐸))
187	12	recnd 11341	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 ∈ ℂ)
188	20	recnd 11341	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℂ)
189	187, 188	neg2subd 11690	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( -Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − -⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶))
190	11	recnd 11341	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑌))) → 𝐶 ∈ ℂ)
191	2, 190	fsumneg 15959	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌)) -𝐶 = -Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶)
192	191	oveq1d 7436	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌)) -𝐶 − -⦋𝑌 / 𝑥⦌𝐴) = ( -Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − -⦋𝑌 / 𝑥⦌𝐴))
193	187, 188	negsubdi2d 11689	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶))
194	189, 192, 193	3eqtr4d 2805	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌)) -𝐶 − -⦋𝑌 / 𝑥⦌𝐴) = -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))
195	186, 194	oveq12d 7439	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌)) -𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) = ( -((𝑌 − (⌊‘𝑌)) · 𝐸) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
196	96	recnd 11341	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ∈ ℂ)
197	196, 57	negdid 11686	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) = ( -((𝑌 − (⌊‘𝑌)) · 𝐸) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
198	195, 197	eqtr4d 2798	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌)) -𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) = -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
199	97	renegcld 11747	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ)
200	198, 199	eqeltrd 2860	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌)) -𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ)
201		nfcv 2922	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑌 − (⌊‘𝑌)) · -𝐸)
202		nfcv 2922	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑌)) -𝐶
203	15	nfneg 11557	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 -⦋𝑌 / 𝑥⦌𝐴
204	202, 24, 203	nfov 7451	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑌)) -𝐶 − -⦋𝑌 / 𝑥⦌𝐴)
205	201, 164, 204	nfov 7451	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌)) -𝐶 − -⦋𝑌 / 𝑥⦌𝐴))
206		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑌 → 𝑥 = 𝑌)
207	206, 26	oveq12d 7439	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → (𝑥 − (⌊‘𝑥)) = (𝑌 − (⌊‘𝑌)))
208	69	negeqd 11555	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → -𝐵 = -𝐸)
209	207, 208	oveq12d 7439	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑌 → ((𝑥 − (⌊‘𝑥)) · -𝐵) = ((𝑌 − (⌊‘𝑌)) · -𝐸))
210	27	sumeq1d 15873	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑌)) -𝐶)
211	17	negeqd 11555	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → -𝐴 = -⦋𝑌 / 𝑥⦌𝐴)
212	210, 211	oveq12d 7439	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑌 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌)) -𝐶 − -⦋𝑌 / 𝑥⦌𝐴))
213	209, 212	oveq12d 7439	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑌 → (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌)) -𝐶 − -⦋𝑌 / 𝑥⦌𝐴)))
214	22, 205, 213, 138	fvmptf 7016	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ 𝑆 ∧ (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌)) -𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ) → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)))‘𝑌) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌)) -𝐶 − -⦋𝑌 / 𝑥⦌𝐴)))
215	1, 200, 214	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)))‘𝑌) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌)) -𝐶 − -⦋𝑌 / 𝑥⦌𝐴)))
216	215, 198	eqtrd 2795	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)))‘𝑌) = -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
217	208	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = 𝑌) → -𝐵 = -𝐸)
218	1, 217	csbied 3882	. . . . . . . . . 10 ⊢ (𝜑 → ⦋𝑌 / 𝑥⦌ -𝐵 = -𝐸)
219	216, 218	oveq12d 7439	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌ -𝐵) = ( -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − -𝐸))
220	141, 183, 219	3brtr3d 5135	. . . . . . . 8 ⊢ (𝜑 → ( -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − -⦋𝑋 / 𝑥⦌𝐵) ≤ ( -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − -𝐸))
221	90	recnd 11341	. . . . . . . . 9 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℂ)
222	221, 143	neg2subd 11690	. . . . . . . 8 ⊢ (𝜑 → ( -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − -⦋𝑋 / 𝑥⦌𝐵) = (⦋𝑋 / 𝑥⦌𝐵 − (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
223	97	recnd 11341	. . . . . . . . 9 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ ℂ)
224	223, 185	neg2subd 11690	. . . . . . . 8 ⊢ (𝜑 → ( -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − -𝐸) = (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
225	220, 222, 224	3brtr3d 5135	. . . . . . 7 ⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 − (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) ≤ (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
226	221, 143	negsubdi2d 11689	. . . . . . 7 ⊢ (𝜑 → -((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) = (⦋𝑋 / 𝑥⦌𝐵 − (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
227	223, 185	negsubdi2d 11689	. . . . . . 7 ⊢ (𝜑 → -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) = (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
228	225, 226, 227	3brtr4d 5136	. . . . . 6 ⊢ (𝜑 → -((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸))
229	98, 91	lenegd 11899	. . . . . 6 ⊢ (𝜑 → (((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ↔ -((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸)))
230	228, 229	mpbird 260	. . . . 5 ⊢ (𝜑 → ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵))
231	73, 98, 91, 116, 230	letrd 11471	. . . 4 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵))
232		1red 11313	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℝ)
233		nfv 1946	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝐷 ≤ 𝑋
234		nfcv 2922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥0
235		nfcv 2922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 ≤
236	234, 235, 161	nfbr 5151	. . . . . . . . . . 11 ⊢ Ⅎ𝑥0 ≤ ⦋𝑋 / 𝑥⦌𝐵
237	233, 236	nfim 1928	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝐷 ≤ 𝑋 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)
238		breq2 5106	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑋))
239	171	breq2d 5114	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (0 ≤ 𝐵 ↔ 0 ≤ ⦋𝑋 / 𝑥⦌𝐵))
240	238, 239	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝐷 ≤ 𝑥 → 0 ≤ 𝐵) ↔ (𝐷 ≤ 𝑋 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)))
241	237, 240	rspc 3564	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 0 ≤ 𝐵) → (𝐷 ≤ 𝑋 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)))
242	33, 103, 105, 241	syl3c 67	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)
243		fracle1 13947	. . . . . . . . 9 ⊢ (𝑋 ∈ ℝ → (𝑋 − (⌊‘𝑋)) ≤ 1)
244	74, 243	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ≤ 1)
245	77, 232, 88, 242, 244	lemul1ad 12260	. . . . . . 7 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ≤ (1 · ⦋𝑋 / 𝑥⦌𝐵))
246	143	mullidd 11331	. . . . . . 7 ⊢ (𝜑 → (1 · ⦋𝑋 / 𝑥⦌𝐵) = ⦋𝑋 / 𝑥⦌𝐵)
247	245, 246	breqtrd 5130	. . . . . 6 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ≤ ⦋𝑋 / 𝑥⦌𝐵)
248	89, 88, 45, 247	leadd1dd 11934	. . . . 5 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (⦋𝑋 / 𝑥⦌𝐵 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
249	90, 88, 45	lesubadd2d 11919	. . . . 5 ⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ↔ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (⦋𝑋 / 𝑥⦌𝐵 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
250	248, 249	mpbird 260	. . . 4 ⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
251	73, 91, 45, 231, 250	letrd 11471	. . 3 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
252	21, 72	readdcld 11342	. . . 4 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸) ∈ ℝ)
253		fracge0 13948	. . . . . . 7 ⊢ (𝑋 ∈ ℝ → 0 ≤ (𝑋 − (⌊‘𝑋)))
254	74, 253	syl 18	. . . . . 6 ⊢ (𝜑 → 0 ≤ (𝑋 − (⌊‘𝑋)))
255	77, 88, 254, 242	mulge0d 11897	. . . . 5 ⊢ (𝜑 → 0 ≤ ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵))
256	45, 89	addge02d 11909	. . . . 5 ⊢ (𝜑 → (0 ≤ ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ↔ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
257	255, 256	mpbid 235	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
258	140	simpld 500	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)))‘𝑌) ≤ ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥)) -𝐶 − -𝐴)))‘𝑋))
259	258, 216, 180	3brtr3d 5135	. . . . . 6 ⊢ (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
260	90, 97	lenegd 11899	. . . . . 6 ⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ↔ -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
261	259, 260	mpbird 260	. . . . 5 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
262		fracle1 13947	. . . . . . . . . 10 ⊢ (𝑌 ∈ ℝ → (𝑌 − (⌊‘𝑌)) ≤ 1)
263	92, 262	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝑌 − (⌊‘𝑌)) ≤ 1)
264	95, 232, 72, 112, 263	lemul1ad 12260	. . . . . . . 8 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ≤ (1 · 𝐸))
265	185	mullidd 11331	. . . . . . . 8 ⊢ (𝜑 → (1 · 𝐸) = 𝐸)
266	264, 265	breqtrd 5130	. . . . . . 7 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ≤ 𝐸)
267	96, 72, 21, 266	leadd1dd 11934	. . . . . 6 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ (𝐸 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
268	185, 57	addcomd 11516	. . . . . 6 ⊢ (𝜑 → (𝐸 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))
269	267, 268	breqtrd 5130	. . . . 5 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))
270	90, 97, 252, 261, 269	letrd 11471	. . . 4 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))
271	45, 90, 252, 257, 270	letrd 11471	. . 3 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))
272	45, 21, 72	absdifled 15610	. . 3 ⊢ (𝜑 → ((abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) ≤ 𝐸 ↔ (((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))))
273	251, 271, 272	mpbir2and 726	. 2 ⊢ (𝜑 → (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) ≤ 𝐸)
274	60, 273	eqbrtrd 5126	1 ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) ≤ 𝐸)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  ∀wral 3076  ⦋csb 3846   ⊆ wss 3895  {cpr 4586   class class class wbr 5102   ↦ cmpt 5185  ‘cfv 6539  (class class class)co 7421  ℂcc 11202  ℝcr 11203  0cc0 11204  1c1 11205   + caddc 11207   · cmul 11209  +∞cpnf 11344  ℝ^*cxr 11346   ≤ cle 11348   − cmin 11545   -cneg 11546  ℤcz 12697  ℤ_≥cuz 12969  (,)cioo 13480  ...cfz 13643  ⌊cfl 13934  abscabs 15407  Σcsu 15859   D cdv 26189

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-inf2 9646  ax-cnex 11260  ax-resscn 11261  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-mulcom 11268  ax-addass 11269  ax-mulass 11270  ax-distr 11271  ax-i2m1 11272  ax-1ne0 11273  ax-1rid 11274  ax-rnegex 11275  ax-rrecex 11276  ax-cnre 11277  ax-pre-lttri 11278  ax-pre-lttrn 11279  ax-pre-ltadd 11280  ax-pre-mulgt0 11281  ax-pre-sup 11282  ax-addf 11283

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-isom 6548  df-riota 7378  df-ov 7424  df-oprab 7425  df-mpo 7426  df-of 7694  df-om 7879  df-1st 8002  df-2nd 8003  df-supp 8181  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-1o 8480  df-2o 8481  df-er 8721  df-map 8853  df-pm 8854  df-ixp 8930  df-en 8978  df-dom 8979  df-sdom 8980  df-fin 8981  df-fsupp 9358  df-fi 9407  df-sup 9438  df-inf 9439  df-oi 9508  df-card 10024  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353  df-sub 11547  df-neg 11548  df-div 11978  df-nn 12340  df-2 12409  df-3 12410  df-4 12411  df-5 12412  df-6 12413  df-7 12414  df-8 12415  df-9 12416  df-n0 12611  df-z 12698  df-dec 12819  df-uz 12970  df-q 13080  df-rp 13125  df-xneg 13245  df-xadd 13246  df-xmul 13247  df-ioo 13484  df-ico 13486  df-icc 13487  df-fz 13644  df-fzo 13793  df-fl 13936  df-seq 14149  df-exp 14209  df-hash 14479  df-cj 15272  df-re 15273  df-im 15274  df-sqrt 15408  df-abs 15409  df-clim 15661  df-sum 15860  df-struct 17331  df-sets 17348  df-slot 17366  df-ndx 17378  df-base 17394  df-ress 17415  df-plusg 17447  df-mulr 17448  df-starv 17449  df-sca 17450  df-vsca 17451  df-ip 17452  df-tset 17453  df-ple 17454  df-ds 17456  df-unif 17457  df-hom 17458  df-cco 17459  df-rest 17599  df-topn 17600  df-0g 17618  df-gsum 17619  df-topgen 17620  df-pt 17621  df-prds 17624  df-xrs 17680  df-qtop 17685  df-imas 17686  df-xps 17688  df-mre 17762  df-mrc 17763  df-acs 17765  df-mgm 18822  df-sgrp 18914  df-mnd 18930  df-submnd 18985  df-mulg 19284  df-cntz 19537  df-cmn 20002  df-psmet 21676  df-xmet 21677  df-met 21678  df-bl 21679  df-mopn 21680  df-fbas 21681  df-fg 21682  df-cnfld 21685  df-top 23218  df-topon 23235  df-topsp 23257  df-bases 23270  df-cld 23343  df-ntr 23344  df-cls 23345  df-nei 23422  df-lp 23460  df-perf 23461  df-cn 23551  df-cnp 23552  df-haus 23639  df-cmp 23711  df-tx 23887  df-hmeo 24080  df-fil 24171  df-fm 24263  df-flim 24264  df-flf 24265  df-xms 24645  df-ms 24646  df-tms 24647  df-cncf 25205  df-limc 26192  df-dv 26193

This theorem is used by:  logfacbnd3  27556  log2sumbnd  27877