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 24778

Description: The reverse of dvfsumrlim 24775, 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 13425	. . . . . . . 8 ⊢ (𝜑 → (𝑀...(⌊‘𝑌)) ∈ Fin)
3		dvfsum2.b2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)
4	3	ralrimiva 3096	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝑍 𝐵 ∈ ℝ)
5		elfzuz 12987	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑀...(⌊‘𝑌)) → 𝑘 ∈ (ℤ_≥‘𝑀))
6		dvfsum2.z	. . . . . . . . . 10 ⊢ 𝑍 = (ℤ_≥‘𝑀)
7	5, 6	eleqtrrdi 2844	. . . . . . . . 9 ⊢ (𝑘 ∈ (𝑀...(⌊‘𝑌)) → 𝑘 ∈ 𝑍)
8		dvfsum2.c	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)
9	8	eleq1d 2817	. . . . . . . . . 10 ⊢ (𝑥 = 𝑘 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ))
10	9	rspccva 3523	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝑍 𝐵 ∈ ℝ ∧ 𝑘 ∈ 𝑍) → 𝐶 ∈ ℝ)
11	4, 7, 10	syl2an 599	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑌))) → 𝐶 ∈ ℝ)
12	2, 11	fsumrecl 15177	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 ∈ ℝ)
13		dvfsum2.a	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)
14	13	ralrimiva 3096	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ)
15		nfcsb1v 3812	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑌 / 𝑥⦌𝐴
16	15	nfel1 2915	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ
17		csbeq1a 3802	. . . . . . . . . 10 ⊢ (𝑥 = 𝑌 → 𝐴 = ⦋𝑌 / 𝑥⦌𝐴)
18	17	eleq1d 2817	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → (𝐴 ∈ ℝ ↔ ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ))
19	16, 18	rspc 3512	. . . . . . . 8 ⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ))
20	1, 14, 19	sylc 65	. . . . . . 7 ⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ)
21	12, 20	resubcld 11139	. . . . . 6 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ)
22		nfcv 2899	. . . . . . 7 ⊢ Ⅎ𝑥𝑌
23		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶
24		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑥 −
25	23, 24, 15	nfov 7194	. . . . . . 7 ⊢ Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)
26		fveq2 6668	. . . . . . . . . 10 ⊢ (𝑥 = 𝑌 → (⌊‘𝑥) = (⌊‘𝑌))
27	26	oveq2d 7180	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → (𝑀...(⌊‘𝑥)) = (𝑀...(⌊‘𝑌)))
28	27	sumeq1d 15144	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶)
29	28, 17	oveq12d 7182	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))
30		dvfsum2.g	. . . . . . 7 ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))
31	22, 25, 29, 30	fvmptf 6790	. . . . . 6 ⊢ ((𝑌 ∈ 𝑆 ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) → (𝐺‘𝑌) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))
32	1, 21, 31	syl2anc 587	. . . . 5 ⊢ (𝜑 → (𝐺‘𝑌) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))
33		dvfsum2.1	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑆)
34		fzfid 13425	. . . . . . . 8 ⊢ (𝜑 → (𝑀...(⌊‘𝑋)) ∈ Fin)
35		elfzuz 12987	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ (ℤ_≥‘𝑀))
36	35, 6	eleqtrrdi 2844	. . . . . . . . 9 ⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ 𝑍)
37	4, 36, 10	syl2an 599	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℝ)
38	34, 37	fsumrecl 15177	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℝ)
39		nfcsb1v 3812	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐴
40	39	nfel1 2915	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ
41		csbeq1a 3802	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → 𝐴 = ⦋𝑋 / 𝑥⦌𝐴)
42	41	eleq1d 2817	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝐴 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ))
43	40, 42	rspc 3512	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ))
44	33, 14, 43	sylc 65	. . . . . . 7 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ)
45	38, 44	resubcld 11139	. . . . . 6 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ)
46		nfcv 2899	. . . . . . 7 ⊢ Ⅎ𝑥𝑋
47		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶
48	47, 24, 39	nfov 7194	. . . . . . 7 ⊢ Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)
49		fveq2 6668	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (⌊‘𝑥) = (⌊‘𝑋))
50	49	oveq2d 7180	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑀...(⌊‘𝑥)) = (𝑀...(⌊‘𝑋)))
51	50	sumeq1d 15144	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)
52	51, 41	oveq12d 7182	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
53	46, 48, 52, 30	fvmptf 6790	. . . . . 6 ⊢ ((𝑋 ∈ 𝑆 ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) → (𝐺‘𝑋) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
54	33, 45, 53	syl2anc 587	. . . . 5 ⊢ (𝜑 → (𝐺‘𝑋) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
55	32, 54	oveq12d 7182	. . . 4 ⊢ (𝜑 → ((𝐺‘𝑌) − (𝐺‘𝑋)) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
56	55	fveq2d 6672	. . 3 ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
57	21	recnd 10740	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℂ)
58	45	recnd 10740	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℂ)
59	57, 58	abssubd 14896	. . 3 ⊢ (𝜑 → (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
60	56, 59	eqtrd 2773	. 2 ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
61		dvfsum2.s	. . . . . . . . . 10 ⊢ 𝑆 = (𝑇(,)+∞)
62		ioossre 12875	. . . . . . . . . 10 ⊢ (𝑇(,)+∞) ⊆ ℝ
63	61, 62	eqsstri 3909	. . . . . . . . 9 ⊢ 𝑆 ⊆ ℝ
64	63	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ⊆ ℝ)
65		dvfsum2.b1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)
66		dvfsum2.b3	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))
67	64, 13, 65, 66	dvmptrecl 24768	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ)
68	67	ralrimiva 3096	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ)
69		dvfsum2.e	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐸)
70	69	eleq1d 2817	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝐵 ∈ ℝ ↔ 𝐸 ∈ ℝ))
71	70	rspcv 3519	. . . . . 6 ⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ → 𝐸 ∈ ℝ))
72	1, 68, 71	sylc 65	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ℝ)
73	21, 72	resubcld 11139	. . . 4 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ∈ ℝ)
74	63, 33	sseldi 3873	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ ℝ)
75		reflcl 13250	. . . . . . . . 9 ⊢ (𝑋 ∈ ℝ → (⌊‘𝑋) ∈ ℝ)
76	74, 75	syl 17	. . . . . . . 8 ⊢ (𝜑 → (⌊‘𝑋) ∈ ℝ)
77	74, 76	resubcld 11139	. . . . . . 7 ⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℝ)
78		nfv 1920	. . . . . . . . . 10 ⊢ Ⅎ𝑚 𝐵 ∈ ℝ
79		nfcsb1v 3812	. . . . . . . . . . 11 ⊢ Ⅎ𝑥⦋𝑚 / 𝑥⦌𝐵
80	79	nfel1 2915	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ
81		csbeq1a 3802	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑥⦌𝐵)
82	81	eleq1d 2817	. . . . . . . . . 10 ⊢ (𝑥 = 𝑚 → (𝐵 ∈ ℝ ↔ ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ))
83	78, 80, 82	cbvralw 3339	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ ↔ ∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ)
84	68, 83	sylib 221	. . . . . . . 8 ⊢ (𝜑 → ∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ)
85		csbeq1 3791	. . . . . . . . . 10 ⊢ (𝑚 = 𝑋 → ⦋𝑚 / 𝑥⦌𝐵 = ⦋𝑋 / 𝑥⦌𝐵)
86	85	eleq1d 2817	. . . . . . . . 9 ⊢ (𝑚 = 𝑋 → (⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ))
87	86	rspcv 3519	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑆 → (∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ))
88	33, 84, 87	sylc 65	. . . . . . 7 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ)
89	77, 88	remulcld 10742	. . . . . 6 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ)
90	89, 45	readdcld 10741	. . . . 5 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ)
91	90, 88	resubcld 11139	. . . 4 ⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ)
92	63, 1	sseldi 3873	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ ℝ)
93		reflcl 13250	. . . . . . . . . 10 ⊢ (𝑌 ∈ ℝ → (⌊‘𝑌) ∈ ℝ)
94	92, 93	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (⌊‘𝑌) ∈ ℝ)
95	92, 94	resubcld 11139	. . . . . . . 8 ⊢ (𝜑 → (𝑌 − (⌊‘𝑌)) ∈ ℝ)
96	95, 72	remulcld 10742	. . . . . . 7 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ∈ ℝ)
97	96, 21	readdcld 10741	. . . . . 6 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ)
98	97, 72	resubcld 11139	. . . . 5 ⊢ (𝜑 → ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) ∈ ℝ)
99		fracge0 13258	. . . . . . . . 9 ⊢ (𝑌 ∈ ℝ → 0 ≤ (𝑌 − (⌊‘𝑌)))
100	92, 99	syl 17	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ (𝑌 − (⌊‘𝑌)))
101		dvfsum2.0	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵)
102	101	expr 460	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷 ≤ 𝑥 → 0 ≤ 𝐵))
103	102	ralrimiva 3096	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 0 ≤ 𝐵))
104		dvfsum2.d	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℝ)
105		dvfsum2.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ≤ 𝑋)
106		dvfsum2.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ≤ 𝑌)
107	104, 74, 92, 105, 106	letrd 10868	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≤ 𝑌)
108		breq2 5031	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑌 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑌))
109	69	breq2d 5039	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑌 → (0 ≤ 𝐵 ↔ 0 ≤ 𝐸))
110	108, 109	imbi12d 348	. . . . . . . . . 10 ⊢ (𝑥 = 𝑌 → ((𝐷 ≤ 𝑥 → 0 ≤ 𝐵) ↔ (𝐷 ≤ 𝑌 → 0 ≤ 𝐸)))
111	110	rspcv 3519	. . . . . . . . 9 ⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 0 ≤ 𝐵) → (𝐷 ≤ 𝑌 → 0 ≤ 𝐸)))
112	1, 103, 107, 111	syl3c 66	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 𝐸)
113	95, 72, 100, 112	mulge0d 11288	. . . . . . 7 ⊢ (𝜑 → 0 ≤ ((𝑌 − (⌊‘𝑌)) · 𝐸))
114	21, 96	addge02d 11300	. . . . . . 7 ⊢ (𝜑 → (0 ≤ ((𝑌 − (⌊‘𝑌)) · 𝐸) ↔ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
115	113, 114	mpbid 235	. . . . . 6 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
116	21, 97, 72, 115	lesub1dd 11327	. . . . 5 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸))
117		dvfsum2.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℤ)
118		dvfsum2.md	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))
119		dvfsum2.t	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ ℝ)
120	13	renegcld 11138	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → -𝐴 ∈ ℝ)
121	67	renegcld 11138	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → -𝐵 ∈ ℝ)
122	3	renegcld 11138	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → -𝐵 ∈ ℝ)
123		reelprrecn 10700	. . . . . . . . . . . . 13 ⊢ ℝ ∈ {ℝ, ℂ}
124	123	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
125	13	recnd 10740	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℂ)
126	124, 125, 65, 66	dvmptneg 24710	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ -𝐴)) = (𝑥 ∈ 𝑆 ↦ -𝐵))
127	8	negeqd 10951	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑘 → -𝐵 = -𝐶)
128		dvfsum2.u	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ ℝ^*)
129		dvfsum2.l	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐵 ≤ 𝐶)
130	67	adantrr 717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) → 𝐵 ∈ ℝ)
131	130	3adant3 1133	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐵 ∈ ℝ)
132		simp2r 1201	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝑘 ∈ 𝑆)
133	68	3ad2ant1 1134	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ)
134	9	rspcv 3519	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ → 𝐶 ∈ ℝ))
135	132, 133, 134	sylc 65	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ∈ ℝ)
136	131, 135	lenegd 11290	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → (𝐵 ≤ 𝐶 ↔ -𝐶 ≤ -𝐵))
137	129, 136	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → -𝐶 ≤ -𝐵)
138		eqid 2738	. . . . . . . . . . 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 24772	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) ≤ ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) ∧ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌-𝐵) ≤ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌-𝐵)))
141	140	simprd 499	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌-𝐵) ≤ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌-𝐵))
142	77	recnd 10740	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℂ)
143	88	recnd 10740	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℂ)
144	142, 143	mulneg2d 11165	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) = -((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵))
145	38	recnd 10740	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℂ)
146	44	recnd 10740	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℂ)
147	145, 146	neg2subd 11085	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (-Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − -⦋𝑋 / 𝑥⦌𝐴) = (⦋𝑋 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
148	37	recnd 10740	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℂ)
149	34, 148	fsumneg 15228	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 = -Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)
150	149	oveq1d 7179	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴) = (-Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − -⦋𝑋 / 𝑥⦌𝐴))
151	145, 146	negsubdi2d 11084	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) = (⦋𝑋 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
152	147, 150, 151	3eqtr4d 2783	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴) = -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
153	144, 152	oveq12d 7182	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) = (-((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
154	89	recnd 10740	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℂ)
155	154, 58	negdid 11081	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) = (-((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
156	153, 155	eqtr4d 2776	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) = -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
157	90	renegcld 11138	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ)
158	156, 157	eqeltrd 2833	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ)
159		nfcv 2899	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑋 − (⌊‘𝑋))
160		nfcv 2899	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 ·
161		nfcsb1v 3812	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐵
162	161	nfneg 10953	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥-⦋𝑋 / 𝑥⦌𝐵
163	159, 160, 162	nfov 7194	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵)
164		nfcv 2899	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥 +
165		nfcv 2899	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶
166	39	nfneg 10953	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥-⦋𝑋 / 𝑥⦌𝐴
167	165, 24, 166	nfov 7194	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)
168	163, 164, 167	nfov 7194	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴))
169		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
170	169, 49	oveq12d 7182	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → (𝑥 − (⌊‘𝑥)) = (𝑋 − (⌊‘𝑋)))
171		csbeq1a 3802	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → 𝐵 = ⦋𝑋 / 𝑥⦌𝐵)
172	171	negeqd 10951	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → -𝐵 = -⦋𝑋 / 𝑥⦌𝐵)
173	170, 172	oveq12d 7182	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → ((𝑥 − (⌊‘𝑥)) · -𝐵) = ((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵))
174	50	sumeq1d 15144	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶)
175	41	negeqd 10951	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → -𝐴 = -⦋𝑋 / 𝑥⦌𝐴)
176	174, 175	oveq12d 7182	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴))
177	173, 176	oveq12d 7182	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)) = (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)))
178	46, 168, 177, 138	fvmptf 6790	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ 𝑆 ∧ (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ) → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) = (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)))
179	33, 158, 178	syl2anc 587	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) = (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)))
180	179, 156	eqtrd 2773	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) = -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
181		csbnegg 10954	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝑆 → ⦋𝑋 / 𝑥⦌-𝐵 = -⦋𝑋 / 𝑥⦌𝐵)
182	33, 181	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌-𝐵 = -⦋𝑋 / 𝑥⦌𝐵)
183	180, 182	oveq12d 7182	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌-𝐵) = (-(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − -⦋𝑋 / 𝑥⦌𝐵))
184	95	recnd 10740	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 − (⌊‘𝑌)) ∈ ℂ)
185	72	recnd 10740	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 ∈ ℂ)
186	184, 185	mulneg2d 11165	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · -𝐸) = -((𝑌 − (⌊‘𝑌)) · 𝐸))
187	12	recnd 10740	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 ∈ ℂ)
188	20	recnd 10740	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℂ)
189	187, 188	neg2subd 11085	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (-Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − -⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶))
190	11	recnd 10740	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑌))) → 𝐶 ∈ ℂ)
191	2, 190	fsumneg 15228	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 = -Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶)
192	191	oveq1d 7179	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴) = (-Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − -⦋𝑌 / 𝑥⦌𝐴))
193	187, 188	negsubdi2d 11084	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶))
194	189, 192, 193	3eqtr4d 2783	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴) = -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))
195	186, 194	oveq12d 7182	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) = (-((𝑌 − (⌊‘𝑌)) · 𝐸) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
196	96	recnd 10740	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ∈ ℂ)
197	196, 57	negdid 11081	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) = (-((𝑌 − (⌊‘𝑌)) · 𝐸) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
198	195, 197	eqtr4d 2776	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) = -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
199	97	renegcld 11138	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ)
200	198, 199	eqeltrd 2833	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ)
201		nfcv 2899	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑌 − (⌊‘𝑌)) · -𝐸)
202		nfcv 2899	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶
203	15	nfneg 10953	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥-⦋𝑌 / 𝑥⦌𝐴
204	202, 24, 203	nfov 7194	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)
205	201, 164, 204	nfov 7194	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴))
206		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑌 → 𝑥 = 𝑌)
207	206, 26	oveq12d 7182	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → (𝑥 − (⌊‘𝑥)) = (𝑌 − (⌊‘𝑌)))
208	69	negeqd 10951	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → -𝐵 = -𝐸)
209	207, 208	oveq12d 7182	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑌 → ((𝑥 − (⌊‘𝑥)) · -𝐵) = ((𝑌 − (⌊‘𝑌)) · -𝐸))
210	27	sumeq1d 15144	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶)
211	17	negeqd 10951	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → -𝐴 = -⦋𝑌 / 𝑥⦌𝐴)
212	210, 211	oveq12d 7182	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑌 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴))
213	209, 212	oveq12d 7182	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑌 → (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)))
214	22, 205, 213, 138	fvmptf 6790	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ 𝑆 ∧ (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ) → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)))
215	1, 200, 214	syl2anc 587	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)))
216	215, 198	eqtrd 2773	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) = -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
217	208	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = 𝑌) → -𝐵 = -𝐸)
218	1, 217	csbied 3824	. . . . . . . . . 10 ⊢ (𝜑 → ⦋𝑌 / 𝑥⦌-𝐵 = -𝐸)
219	216, 218	oveq12d 7182	. . . . . . . . 9 ⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌-𝐵) = (-(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − -𝐸))
220	141, 183, 219	3brtr3d 5058	. . . . . . . 8 ⊢ (𝜑 → (-(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − -⦋𝑋 / 𝑥⦌𝐵) ≤ (-(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − -𝐸))
221	90	recnd 10740	. . . . . . . . 9 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℂ)
222	221, 143	neg2subd 11085	. . . . . . . 8 ⊢ (𝜑 → (-(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − -⦋𝑋 / 𝑥⦌𝐵) = (⦋𝑋 / 𝑥⦌𝐵 − (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
223	97	recnd 10740	. . . . . . . . 9 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ ℂ)
224	223, 185	neg2subd 11085	. . . . . . . 8 ⊢ (𝜑 → (-(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − -𝐸) = (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
225	220, 222, 224	3brtr3d 5058	. . . . . . 7 ⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 − (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) ≤ (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
226	221, 143	negsubdi2d 11084	. . . . . . 7 ⊢ (𝜑 → -((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) = (⦋𝑋 / 𝑥⦌𝐵 − (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
227	223, 185	negsubdi2d 11084	. . . . . . 7 ⊢ (𝜑 → -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) = (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))))
228	225, 226, 227	3brtr4d 5059	. . . . . 6 ⊢ (𝜑 → -((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸))
229	98, 91	lenegd 11290	. . . . . 6 ⊢ (𝜑 → (((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ↔ -((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸)))
230	228, 229	mpbird 260	. . . . 5 ⊢ (𝜑 → ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵))
231	73, 98, 91, 116, 230	letrd 10868	. . . 4 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵))
232		1red 10713	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℝ)
233		nfv 1920	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝐷 ≤ 𝑋
234		nfcv 2899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥0
235		nfcv 2899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 ≤
236	234, 235, 161	nfbr 5074	. . . . . . . . . . 11 ⊢ Ⅎ𝑥0 ≤ ⦋𝑋 / 𝑥⦌𝐵
237	233, 236	nfim 1902	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝐷 ≤ 𝑋 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)
238		breq2 5031	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑋))
239	171	breq2d 5039	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (0 ≤ 𝐵 ↔ 0 ≤ ⦋𝑋 / 𝑥⦌𝐵))
240	238, 239	imbi12d 348	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝐷 ≤ 𝑥 → 0 ≤ 𝐵) ↔ (𝐷 ≤ 𝑋 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)))
241	237, 240	rspc 3512	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 0 ≤ 𝐵) → (𝐷 ≤ 𝑋 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)))
242	33, 103, 105, 241	syl3c 66	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)
243		fracle1 13257	. . . . . . . . 9 ⊢ (𝑋 ∈ ℝ → (𝑋 − (⌊‘𝑋)) ≤ 1)
244	74, 243	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ≤ 1)
245	77, 232, 88, 242, 244	lemul1ad 11650	. . . . . . 7 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ≤ (1 · ⦋𝑋 / 𝑥⦌𝐵))
246	143	mulid2d 10730	. . . . . . 7 ⊢ (𝜑 → (1 · ⦋𝑋 / 𝑥⦌𝐵) = ⦋𝑋 / 𝑥⦌𝐵)
247	245, 246	breqtrd 5053	. . . . . 6 ⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ≤ ⦋𝑋 / 𝑥⦌𝐵)
248	89, 88, 45, 247	leadd1dd 11325	. . . . 5 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (⦋𝑋 / 𝑥⦌𝐵 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
249	90, 88, 45	lesubadd2d 11310	. . . . 5 ⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ↔ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (⦋𝑋 / 𝑥⦌𝐵 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
250	248, 249	mpbird 260	. . . 4 ⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
251	73, 91, 45, 231, 250	letrd 10868	. . 3 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))
252	21, 72	readdcld 10741	. . . 4 ⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸) ∈ ℝ)
253		fracge0 13258	. . . . . . 7 ⊢ (𝑋 ∈ ℝ → 0 ≤ (𝑋 − (⌊‘𝑋)))
254	74, 253	syl 17	. . . . . 6 ⊢ (𝜑 → 0 ≤ (𝑋 − (⌊‘𝑋)))
255	77, 88, 254, 242	mulge0d 11288	. . . . 5 ⊢ (𝜑 → 0 ≤ ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵))
256	45, 89	addge02d 11300	. . . . 5 ⊢ (𝜑 → (0 ≤ ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ↔ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
257	255, 256	mpbid 235	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
258	140	simpld 498	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) ≤ ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋))
259	258, 216, 180	3brtr3d 5058	. . . . . 6 ⊢ (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))
260	90, 97	lenegd 11290	. . . . . 6 ⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ↔ -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))))
261	259, 260	mpbird 260	. . . . 5 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
262		fracle1 13257	. . . . . . . . . 10 ⊢ (𝑌 ∈ ℝ → (𝑌 − (⌊‘𝑌)) ≤ 1)
263	92, 262	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑌 − (⌊‘𝑌)) ≤ 1)
264	95, 232, 72, 112, 263	lemul1ad 11650	. . . . . . . 8 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ≤ (1 · 𝐸))
265	185	mulid2d 10730	. . . . . . . 8 ⊢ (𝜑 → (1 · 𝐸) = 𝐸)
266	264, 265	breqtrd 5053	. . . . . . 7 ⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ≤ 𝐸)
267	96, 72, 21, 266	leadd1dd 11325	. . . . . 6 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ (𝐸 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))
268	185, 57	addcomd 10913	. . . . . 6 ⊢ (𝜑 → (𝐸 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))
269	267, 268	breqtrd 5053	. . . . 5 ⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))
270	90, 97, 252, 261, 269	letrd 10868	. . . 4 ⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))
271	45, 90, 252, 257, 270	letrd 10868	. . 3 ⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))
272	45, 21, 72	absdifled 14877	. . 3 ⊢ (𝜑 → ((abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) ≤ 𝐸 ↔ (((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸))))
273	251, 271, 272	mpbir2and 713	. 2 ⊢ (𝜑 → (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) ≤ 𝐸)
274	60, 273	eqbrtrd 5049	1 ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) ≤ 𝐸)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1088 = wceq 1542 ∈ wcel 2113 ∀wral 3053 ⦋csb 3788 ⊆ wss 3841 {cpr 4515 class class class wbr 5027 ↦ cmpt 5107 ‘cfv 6333 (class class class)co 7164 ℂcc 10606 ℝcr 10607 0cc0 10608 1c1 10609 + caddc 10611 · cmul 10613 +∞cpnf 10743 ℝ^*cxr 10745 ≤ cle 10747 − cmin 10941 -cneg 10942 ℤcz 12055 ℤ_≥cuz 12317 (,)cioo 12814 ...cfz 12974 ⌊cfl 13244 abscabs 14676 Σcsu 15128 D cdv 24607

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-rep 5151 ax-sep 5164 ax-nul 5171 ax-pow 5229 ax-pr 5293 ax-un 7473 ax-inf2 9170 ax-cnex 10664 ax-resscn 10665 ax-1cn 10666 ax-icn 10667 ax-addcl 10668 ax-addrcl 10669 ax-mulcl 10670 ax-mulrcl 10671 ax-mulcom 10672 ax-addass 10673 ax-mulass 10674 ax-distr 10675 ax-i2m1 10676 ax-1ne0 10677 ax-1rid 10678 ax-rnegex 10679 ax-rrecex 10680 ax-cnre 10681 ax-pre-lttri 10682 ax-pre-lttrn 10683 ax-pre-ltadd 10684 ax-pre-mulgt0 10685 ax-pre-sup 10686 ax-addf 10687 ax-mulf 10688

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3399 df-sbc 3680 df-csb 3789 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-pss 3860 df-nul 4210 df-if 4412 df-pw 4487 df-sn 4514 df-pr 4516 df-tp 4518 df-op 4520 df-uni 4794 df-int 4834 df-iun 4880 df-iin 4881 df-br 5028 df-opab 5090 df-mpt 5108 df-tr 5134 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-se 5479 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6123 df-ord 6169 df-on 6170 df-lim 6171 df-suc 6172 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-f1 6338 df-fo 6339 df-f1o 6340 df-fv 6341 df-isom 6342 df-riota 7121 df-ov 7167 df-oprab 7168 df-mpo 7169 df-of 7419 df-om 7594 df-1st 7707 df-2nd 7708 df-supp 7850 df-wrecs 7969 df-recs 8030 df-rdg 8068 df-1o 8124 df-2o 8125 df-er 8313 df-map 8432 df-pm 8433 df-ixp 8501 df-en 8549 df-dom 8550 df-sdom 8551 df-fin 8552 df-fsupp 8900 df-fi 8941 df-sup 8972 df-inf 8973 df-oi 9040 df-card 9434 df-pnf 10748 df-mnf 10749 df-xr 10750 df-ltxr 10751 df-le 10752 df-sub 10943 df-neg 10944 df-div 11369 df-nn 11710 df-2 11772 df-3 11773 df-4 11774 df-5 11775 df-6 11776 df-7 11777 df-8 11778 df-9 11779 df-n0 11970 df-z 12056 df-dec 12173 df-uz 12318 df-q 12424 df-rp 12466 df-xneg 12583 df-xadd 12584 df-xmul 12585 df-ioo 12818 df-ico 12820 df-icc 12821 df-fz 12975 df-fzo 13118 df-fl 13246 df-seq 13454 df-exp 13515 df-hash 13776 df-cj 14541 df-re 14542 df-im 14543 df-sqrt 14677 df-abs 14678 df-clim 14928 df-sum 15129 df-struct 16581 df-ndx 16582 df-slot 16583 df-base 16585 df-sets 16586 df-ress 16587 df-plusg 16674 df-mulr 16675 df-starv 16676 df-sca 16677 df-vsca 16678 df-ip 16679 df-tset 16680 df-ple 16681 df-ds 16683 df-unif 16684 df-hom 16685 df-cco 16686 df-rest 16792 df-topn 16793 df-0g 16811 df-gsum 16812 df-topgen 16813 df-pt 16814 df-prds 16817 df-xrs 16871 df-qtop 16876 df-imas 16877 df-xps 16879 df-mre 16953 df-mrc 16954 df-acs 16956 df-mgm 17961 df-sgrp 18010 df-mnd 18021 df-submnd 18066 df-mulg 18336 df-cntz 18558 df-cmn 19019 df-psmet 20202 df-xmet 20203 df-met 20204 df-bl 20205 df-mopn 20206 df-fbas 20207 df-fg 20208 df-cnfld 20211 df-top 21638 df-topon 21655 df-topsp 21677 df-bases 21690 df-cld 21763 df-ntr 21764 df-cls 21765 df-nei 21842 df-lp 21880 df-perf 21881 df-cn 21971 df-cnp 21972 df-haus 22059 df-cmp 22131 df-tx 22306 df-hmeo 22499 df-fil 22590 df-fm 22682 df-flim 22683 df-flf 22684 df-xms 23066 df-ms 23067 df-tms 23068 df-cncf 23623 df-limc 24610 df-dv 24611

This theorem is referenced by: logfacbnd3 25951 log2sumbnd 26272

W3C validator