gg-dvfsumlem2

Description: Lemma for dvfsumrlim . (Contributed by Mario Carneiro, 17-May-2016) Use mpomulcn instead of mulcn as direct dependency. (Revised by GG, 16-Mar-2025)

	Ref	Expression
Hypotheses	gg-dvfsum.s	$⊢ S = (T, +∞)$
	gg-dvfsum.z	$⊢ Z = ℤ_{\geq M}$
	gg-dvfsum.m	$⊢ φ \to M \in ℤ$
	gg-dvfsum.d	$⊢ φ \to D \in ℝ$
	gg-dvfsum.md	$⊢ φ \to M \leq D + 1$
	gg-dvfsum.t	$⊢ φ \to T \in ℝ$
	gg-dvfsum.a	$⊢ (φ \land x \in S) \to A \in ℝ$
	gg-dvfsum.b1	$⊢ (φ \land x \in S) \to B \in V$
	gg-dvfsum.b2	$⊢ (φ \land x \in Z) \to B \in ℝ$
	gg-dvfsum.b3	$⊢ φ \to \frac{d (x \in S⟼ A)}{d_{ℝ} x} = (x \in S ⟼ B)$
	gg-dvfsum.c	$⊢ x = k \to B = C$
	gg-dvfsum.u	$⊢ φ \to U \in ℝ^{*}$
	gg-dvfsum.l	$⊢ (φ \land (x \in S \land k \in S) \land (D \leq x \land x \leq k \land k \leq U)) \to C \leq B$
	gg-dvfsum.h	$⊢ H = (x \in S ⟼ (x - ⌊x⌋) B + \sum_{k = M}^{⌊x⌋} C - A)$
	gg-dvfsumlem1.1	$⊢ φ \to X \in S$
	gg-dvfsumlem1.2	$⊢ φ \to Y \in S$
	gg-dvfsumlem1.3	$⊢ φ \to D \leq X$
	gg-dvfsumlem1.4	$⊢ φ \to X \leq Y$
	gg-dvfsumlem1.5	$⊢ φ \to Y \leq U$
	gg-dvfsumlem1.6	$⊢ φ \to Y \leq ⌊X⌋ + 1$
Assertion	gg-dvfsumlem2	$⊢ φ \to (H (Y) \leq H (X) \land H (X) - ⦋ X / x ⦌ B \leq H (Y) - ⦋ Y / x ⦌ B)$

Proof

Step	Hyp	Ref	Expression
1		gg-dvfsum.s	$⊢ S = (T, +∞)$
2		gg-dvfsum.z	$⊢ Z = ℤ_{\geq M}$
3		gg-dvfsum.m	$⊢ φ \to M \in ℤ$
4		gg-dvfsum.d	$⊢ φ \to D \in ℝ$
5		gg-dvfsum.md	$⊢ φ \to M \leq D + 1$
6		gg-dvfsum.t	$⊢ φ \to T \in ℝ$
7		gg-dvfsum.a	$⊢ (φ \land x \in S) \to A \in ℝ$
8		gg-dvfsum.b1	$⊢ (φ \land x \in S) \to B \in V$
9		gg-dvfsum.b2	$⊢ (φ \land x \in Z) \to B \in ℝ$
10		gg-dvfsum.b3	$⊢ φ \to \frac{d (x \in S⟼ A)}{d_{ℝ} x} = (x \in S ⟼ B)$
11		gg-dvfsum.c	$⊢ x = k \to B = C$
12		gg-dvfsum.u	$⊢ φ \to U \in ℝ^{*}$
13		gg-dvfsum.l	$⊢ (φ \land (x \in S \land k \in S) \land (D \leq x \land x \leq k \land k \leq U)) \to C \leq B$
14		gg-dvfsum.h	$⊢ H = (x \in S ⟼ (x - ⌊x⌋) B + \sum_{k = M}^{⌊x⌋} C - A)$
15		gg-dvfsumlem1.1	$⊢ φ \to X \in S$
16		gg-dvfsumlem1.2	$⊢ φ \to Y \in S$
17		gg-dvfsumlem1.3	$⊢ φ \to D \leq X$
18		gg-dvfsumlem1.4	$⊢ φ \to X \leq Y$
19		gg-dvfsumlem1.5	$⊢ φ \to Y \leq U$
20		gg-dvfsumlem1.6	$⊢ φ \to Y \leq ⌊X⌋ + 1$
21		ioossre	$⊢ (T, +∞) \subseteq ℝ$
22	1 21	eqsstri	$⊢ S \subseteq ℝ$
23	22 16	sselid	$⊢ φ \to Y \in ℝ$
24	15 1	eleqtrdi	$⊢ φ \to X \in (T, +∞)$
25	6	rexrd	$⊢ φ \to T \in ℝ^{*}$
26		elioopnf	$⊢ T \in ℝ^{*} \to (X \in (T, +∞) \leftrightarrow (X \in ℝ \land T < X))$
27	25 26	syl	$⊢ φ \to (X \in (T, +∞) \leftrightarrow (X \in ℝ \land T < X))$
28	24 27	mpbid	$⊢ φ \to (X \in ℝ \land T < X)$
29	28	simpld	$⊢ φ \to X \in ℝ$
30		reflcl	$⊢ X \in ℝ \to ⌊X⌋ \in ℝ$
31	29 30	syl	$⊢ φ \to ⌊X⌋ \in ℝ$
32	23 31	resubcld	$⊢ φ \to Y - ⌊X⌋ \in ℝ$
33		csbeq1	$⊢ y = Y \to ⦋ y / x ⦌ B = ⦋ Y / x ⦌ B$
34	33	eleq1d	$⊢ y = Y \to (⦋ y / x ⦌ B \in ℝ \leftrightarrow ⦋ Y / x ⦌ B \in ℝ)$
35	22	a1i	$⊢ φ \to S \subseteq ℝ$
36	35 7 8 10	dvmptrecl	$⊢ (φ \land x \in S) \to B \in ℝ$
37	36	fmpttd	$⊢ φ \to (x \in S ⟼ B) : S ⟶ ℝ$
38		nfcv	$⊢ \underline{Ⅎ} y B$
39		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ B$
40		csbeq1a	$⊢ x = y \to B = ⦋ y / x ⦌ B$
41	38 39 40	cbvmpt	$⊢ (x \in S ⟼ B) = (y \in S ⟼ ⦋ y / x ⦌ B)$
42	41	fmpt	$⊢ \forall y \in S ⦋ y / x ⦌ B \in ℝ \leftrightarrow (x \in S ⟼ B) : S ⟶ ℝ$
43	37 42	sylibr	$⊢ φ \to \forall y \in S ⦋ y / x ⦌ B \in ℝ$
44	34 43 16	rspcdva	$⊢ φ \to ⦋ Y / x ⦌ B \in ℝ$
45	32 44	remulcld	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B \in ℝ$
46		csbeq1	$⊢ y = Y \to ⦋ y / x ⦌ A = ⦋ Y / x ⦌ A$
47	46	eleq1d	$⊢ y = Y \to (⦋ y / x ⦌ A \in ℝ \leftrightarrow ⦋ Y / x ⦌ A \in ℝ)$
48	7	fmpttd	$⊢ φ \to (x \in S ⟼ A) : S ⟶ ℝ$
49		nfcv	$⊢ \underline{Ⅎ} y A$
50		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ A$
51		csbeq1a	$⊢ x = y \to A = ⦋ y / x ⦌ A$
52	49 50 51	cbvmpt	$⊢ (x \in S ⟼ A) = (y \in S ⟼ ⦋ y / x ⦌ A)$
53	52	fmpt	$⊢ \forall y \in S ⦋ y / x ⦌ A \in ℝ \leftrightarrow (x \in S ⟼ A) : S ⟶ ℝ$
54	48 53	sylibr	$⊢ φ \to \forall y \in S ⦋ y / x ⦌ A \in ℝ$
55	47 54 16	rspcdva	$⊢ φ \to ⦋ Y / x ⦌ A \in ℝ$
56	45 55	resubcld	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A \in ℝ$
57	29 31	resubcld	$⊢ φ \to X - ⌊X⌋ \in ℝ$
58		csbeq1	$⊢ y = X \to ⦋ y / x ⦌ B = ⦋ X / x ⦌ B$
59	58	eleq1d	$⊢ y = X \to (⦋ y / x ⦌ B \in ℝ \leftrightarrow ⦋ X / x ⦌ B \in ℝ)$
60	59 43 15	rspcdva	$⊢ φ \to ⦋ X / x ⦌ B \in ℝ$
61	57 60	remulcld	$⊢ φ \to (X - ⌊X⌋) ⦋ X / x ⦌ B \in ℝ$
62		csbeq1	$⊢ y = X \to ⦋ y / x ⦌ A = ⦋ X / x ⦌ A$
63	62	eleq1d	$⊢ y = X \to (⦋ y / x ⦌ A \in ℝ \leftrightarrow ⦋ X / x ⦌ A \in ℝ)$
64	63 54 15	rspcdva	$⊢ φ \to ⦋ X / x ⦌ A \in ℝ$
65	61 64	resubcld	$⊢ φ \to (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A \in ℝ$
66		fzfid	$⊢ φ \to (M \dots ⌊X⌋) \in Fin$
67	9	ralrimiva	$⊢ φ \to \forall x \in Z B \in ℝ$
68		elfzuz	$⊢ k \in (M \dots ⌊X⌋) \to k \in ℤ_{\geq M}$
69	68 2	eleqtrrdi	$⊢ k \in (M \dots ⌊X⌋) \to k \in Z$
70	11	eleq1d	$⊢ x = k \to (B \in ℝ \leftrightarrow C \in ℝ)$
71	70	rspccva	$⊢ (\forall x \in Z B \in ℝ \land k \in Z) \to C \in ℝ$
72	67 69 71	syl2an	$⊢ (φ \land k \in (M \dots ⌊X⌋)) \to C \in ℝ$
73	66 72	fsumrecl	$⊢ φ \to \sum_{k = M}^{⌊X⌋} C \in ℝ$
74	57 44	remulcld	$⊢ φ \to (X - ⌊X⌋) ⦋ Y / x ⦌ B \in ℝ$
75	74 64	resubcld	$⊢ φ \to (X - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ X / x ⦌ A \in ℝ$
76	23 29	resubcld	$⊢ φ \to Y - X \in ℝ$
77	44 76	remulcld	$⊢ φ \to ⦋ Y / x ⦌ B (Y - X) \in ℝ$
78	44	recnd	$⊢ φ \to ⦋ Y / x ⦌ B \in ℂ$
79	23	recnd	$⊢ φ \to Y \in ℂ$
80	29	recnd	$⊢ φ \to X \in ℂ$
81	78 79 80	subdid	$⊢ φ \to ⦋ Y / x ⦌ B (Y - X) = ⦋ Y / x ⦌ B Y - ⦋ Y / x ⦌ B X$
82		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
83	82	mpomulcn	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
84		csbeq1	$⊢ z = Y \to ⦋ z / x ⦌ B = ⦋ Y / x ⦌ B$
85	84	eleq1d	$⊢ z = Y \to (⦋ z / x ⦌ B \in ℝ \leftrightarrow ⦋ Y / x ⦌ B \in ℝ)$
86		nfcv	$⊢ \underline{Ⅎ} z B$
87		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ z / x ⦌ B$
88		csbeq1a	$⊢ x = z \to B = ⦋ z / x ⦌ B$
89	86 87 88	cbvmpt	$⊢ (x \in S ⟼ B) = (z \in S ⟼ ⦋ z / x ⦌ B)$
90	89	fmpt	$⊢ \forall z \in S ⦋ z / x ⦌ B \in ℝ \leftrightarrow (x \in S ⟼ B) : S ⟶ ℝ$
91	37 90	sylibr	$⊢ φ \to \forall z \in S ⦋ z / x ⦌ B \in ℝ$
92	85 91 16	rspcdva	$⊢ φ \to ⦋ Y / x ⦌ B \in ℝ$
93		pnfxr	$⊢ +∞ \in ℝ^{*}$
94	93	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
95	28	simprd	$⊢ φ \to T < X$
96	23	ltpnfd	$⊢ φ \to Y < +∞$
97		iccssioo	$⊢ ((T \in ℝ^{} \land +∞ \in ℝ^{}) \land (T < X \land Y < +∞)) \to [X, Y] \subseteq (T, +∞)$
98	25 94 95 96 97	syl22anc	$⊢ φ \to [X, Y] \subseteq (T, +∞)$
99	98 21	sstrdi	$⊢ φ \to [X, Y] \subseteq ℝ$
100		ax-resscn	$⊢ ℝ \subseteq ℂ$
101	99 100	sstrdi	$⊢ φ \to [X, Y] \subseteq ℂ$
102	100	a1i	$⊢ φ \to ℝ \subseteq ℂ$
103		cncfmptc	$⊢ (⦋ Y / x ⦌ B \in ℝ \land [X, Y] \subseteq ℂ \land ℝ \subseteq ℂ) \to (y \in [X, Y] ⟼ ⦋ Y / x ⦌ B) : [X, Y] \underset{cn}{⟶} ℝ$
104	92 101 102 103	syl3anc	$⊢ φ \to (y \in [X, Y] ⟼ ⦋ Y / x ⦌ B) : [X, Y] \underset{cn}{⟶} ℝ$
105		cncfmptid	$⊢ ([X, Y] \subseteq ℝ \land ℝ \subseteq ℂ) \to (y \in [X, Y] ⟼ y) : [X, Y] \underset{cn}{⟶} ℝ$
106	99 100 105	sylancl	$⊢ φ \to (y \in [X, Y] ⟼ y) : [X, Y] \underset{cn}{⟶} ℝ$
107		remulcl	$⊢ (⦋ Y / x ⦌ B \in ℝ \land y \in ℝ) \to ⦋ Y / x ⦌ B y \in ℝ$
108		simpl	$⊢ (⦋ Y / x ⦌ B \in ℝ \land y \in ℝ) \to ⦋ Y / x ⦌ B \in ℝ$
109	108	recnd	$⊢ (⦋ Y / x ⦌ B \in ℝ \land y \in ℝ) \to ⦋ Y / x ⦌ B \in ℂ$
110		simpr	$⊢ (⦋ Y / x ⦌ B \in ℝ \land y \in ℝ) \to y \in ℝ$
111	110	recnd	$⊢ (⦋ Y / x ⦌ B \in ℝ \land y \in ℝ) \to y \in ℂ$
112	109 111	jca	$⊢ (⦋ Y / x ⦌ B \in ℝ \land y \in ℝ) \to (⦋ Y / x ⦌ B \in ℂ \land y \in ℂ)$
113		ovmul	$⊢ (⦋ Y / x ⦌ B \in ℂ \land y \in ℂ) \to ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y = ⦋ Y / x ⦌ B y$
114	113	eqcomd	$⊢ (⦋ Y / x ⦌ B \in ℂ \land y \in ℂ) \to ⦋ Y / x ⦌ B y = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y$
115	112 114	syl	$⊢ (⦋ Y / x ⦌ B \in ℝ \land y \in ℝ) \to ⦋ Y / x ⦌ B y = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y$
116	115	eleq1d	$⊢ (⦋ Y / x ⦌ B \in ℝ \land y \in ℝ) \to (⦋ Y / x ⦌ B y \in ℝ \leftrightarrow ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y \in ℝ)$
117	116	biimpd	$⊢ (⦋ Y / x ⦌ B \in ℝ \land y \in ℝ) \to (⦋ Y / x ⦌ B y \in ℝ \to ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y \in ℝ)$
118	107 117	mpd	$⊢ (⦋ Y / x ⦌ B \in ℝ \land y \in ℝ) \to ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y \in ℝ$
119	82 83 104 106 100 118	cncfmpt2ss	$⊢ φ \to (y \in [X, Y] ⟼ ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y) : [X, Y] \underset{cn}{⟶} ℝ$
120		df-mpt	$⊢ (y \in [X, Y] ⟼ ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y) = \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\}$
121	120	eleq1i	$⊢ (y \in [X, Y] ⟼ ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y) : [X, Y] \underset{cn}{⟶} ℝ \leftrightarrow \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} : [X, Y] \underset{cn}{⟶} ℝ$
122	121	biimpi	$⊢ (y \in [X, Y] ⟼ ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y) : [X, Y] \underset{cn}{⟶} ℝ \to \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} : [X, Y] \underset{cn}{⟶} ℝ$
123	119 122	syl	$⊢ φ \to \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} : [X, Y] \underset{cn}{⟶} ℝ$
124		idd	$⊢ φ \to (y \in [X, Y] \to y \in [X, Y])$
125	124	a1dd	$⊢ φ \to (y \in [X, Y] \to (w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y \to y \in [X, Y]))$
126	125	impd	$⊢ φ \to ((y \in [X, Y] \land w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y) \to y \in [X, Y])$
127		csbeq1	$⊢ m = Y \to ⦋ m / x ⦌ B = ⦋ Y / x ⦌ B$
128	127	eleq1d	$⊢ m = Y \to (⦋ m / x ⦌ B \in ℝ \leftrightarrow ⦋ Y / x ⦌ B \in ℝ)$
129		nfcv	$⊢ \underline{Ⅎ} m B$
130		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ m / x ⦌ B$
131		csbeq1a	$⊢ x = m \to B = ⦋ m / x ⦌ B$
132	129 130 131	cbvmpt	$⊢ (x \in S ⟼ B) = (m \in S ⟼ ⦋ m / x ⦌ B)$
133	132	fmpt	$⊢ \forall m \in S ⦋ m / x ⦌ B \in ℝ \leftrightarrow (x \in S ⟼ B) : S ⟶ ℝ$
134	37 133	sylibr	$⊢ φ \to \forall m \in S ⦋ m / x ⦌ B \in ℝ$
135	128 134 16	rspcdva	$⊢ φ \to ⦋ Y / x ⦌ B \in ℝ$
136	135	recnd	$⊢ φ \to ⦋ Y / x ⦌ B \in ℂ$
137	136	adantr	$⊢ (φ \land y \in [X, Y]) \to ⦋ Y / x ⦌ B \in ℂ$
138		elicc2	$⊢ (X \in ℝ \land Y \in ℝ) \to (y \in [X, Y] \leftrightarrow (y \in ℝ \land X \leq y \land y \leq Y))$
139	29 23 138	syl2anc	$⊢ φ \to (y \in [X, Y] \leftrightarrow (y \in ℝ \land X \leq y \land y \leq Y))$
140	139	biimpa	$⊢ (φ \land y \in [X, Y]) \to (y \in ℝ \land X \leq y \land y \leq Y)$
141	140	simp1d	$⊢ (φ \land y \in [X, Y]) \to y \in ℝ$
142	141	recnd	$⊢ (φ \land y \in [X, Y]) \to y \in ℂ$
143	137 142	jca	$⊢ (φ \land y \in [X, Y]) \to (⦋ Y / x ⦌ B \in ℂ \land y \in ℂ)$
144	143 113	syl	$⊢ (φ \land y \in [X, Y]) \to ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y = ⦋ Y / x ⦌ B y$
145	144	eqeq2d	$⊢ (φ \land y \in [X, Y]) \to (w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y \leftrightarrow w = ⦋ Y / x ⦌ B y)$
146	145	biimpd	$⊢ (φ \land y \in [X, Y]) \to (w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y \to w = ⦋ Y / x ⦌ B y)$
147	146	ex	$⊢ φ \to (y \in [X, Y] \to (w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y \to w = ⦋ Y / x ⦌ B y))$
148	147	impd	$⊢ φ \to ((y \in [X, Y] \land w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y) \to w = ⦋ Y / x ⦌ B y)$
149	126 148	jcad	$⊢ φ \to ((y \in [X, Y] \land w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y) \to (y \in [X, Y] \land w = ⦋ Y / x ⦌ B y))$
150	124	a1dd	$⊢ φ \to (y \in [X, Y] \to (w = ⦋ Y / x ⦌ B y \to y \in [X, Y]))$
151	150	impd	$⊢ φ \to ((y \in [X, Y] \land w = ⦋ Y / x ⦌ B y) \to y \in [X, Y])$
152		csbeq1	$⊢ k = Y \to ⦋ k / x ⦌ B = ⦋ Y / x ⦌ B$
153	152	eleq1d	$⊢ k = Y \to (⦋ k / x ⦌ B \in ℝ \leftrightarrow ⦋ Y / x ⦌ B \in ℝ)$
154		nfcv	$⊢ \underline{Ⅎ} k B$
155		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ k / x ⦌ B$
156		csbeq1a	$⊢ x = k \to B = ⦋ k / x ⦌ B$
157	154 155 156	cbvmpt	$⊢ (x \in S ⟼ B) = (k \in S ⟼ ⦋ k / x ⦌ B)$
158	157	fmpt	$⊢ \forall k \in S ⦋ k / x ⦌ B \in ℝ \leftrightarrow (x \in S ⟼ B) : S ⟶ ℝ$
159	37 158	sylibr	$⊢ φ \to \forall k \in S ⦋ k / x ⦌ B \in ℝ$
160	153 159 16	rspcdva	$⊢ φ \to ⦋ Y / x ⦌ B \in ℝ$
161	160	recnd	$⊢ φ \to ⦋ Y / x ⦌ B \in ℂ$
162	161	adantr	$⊢ (φ \land y \in [X, Y]) \to ⦋ Y / x ⦌ B \in ℂ$
163	162 142	jca	$⊢ (φ \land y \in [X, Y]) \to (⦋ Y / x ⦌ B \in ℂ \land y \in ℂ)$
164	163 114	syl	$⊢ (φ \land y \in [X, Y]) \to ⦋ Y / x ⦌ B y = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y$
165	164	eqeq2d	$⊢ (φ \land y \in [X, Y]) \to (w = ⦋ Y / x ⦌ B y \leftrightarrow w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)$
166	165	biimpd	$⊢ (φ \land y \in [X, Y]) \to (w = ⦋ Y / x ⦌ B y \to w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)$
167	166	ex	$⊢ φ \to (y \in [X, Y] \to (w = ⦋ Y / x ⦌ B y \to w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y))$
168	167	impd	$⊢ φ \to ((y \in [X, Y] \land w = ⦋ Y / x ⦌ B y) \to w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)$
169	151 168	jcad	$⊢ φ \to ((y \in [X, Y] \land w = ⦋ Y / x ⦌ B y) \to (y \in [X, Y] \land w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y))$
170	149 169	impbid	$⊢ φ \to ((y \in [X, Y] \land w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y) \leftrightarrow (y \in [X, Y] \land w = ⦋ Y / x ⦌ B y))$
171	170	opabbidv	$⊢ φ \to \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} = \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ Y / x ⦌ B y)\}$
172		df-mpt	$⊢ (y \in [X, Y] ⟼ ⦋ Y / x ⦌ B y) = \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ Y / x ⦌ B y)\}$
173	172	eqcomi	$⊢ \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ Y / x ⦌ B y)\} = (y \in [X, Y] ⟼ ⦋ Y / x ⦌ B y)$
174	173	eqeq2i	$⊢ \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} = \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ Y / x ⦌ B y)\} \leftrightarrow \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} = (y \in [X, Y] ⟼ ⦋ Y / x ⦌ B y)$
175	174	biimpi	$⊢ \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} = \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ Y / x ⦌ B y)\} \to \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} = (y \in [X, Y] ⟼ ⦋ Y / x ⦌ B y)$
176	171 175	syl	$⊢ φ \to \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} = (y \in [X, Y] ⟼ ⦋ Y / x ⦌ B y)$
177	176	eleq1d	$⊢ φ \to (\{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} : [X, Y] \underset{cn}{⟶} ℝ \leftrightarrow (y \in [X, Y] ⟼ ⦋ Y / x ⦌ B y) : [X, Y] \underset{cn}{⟶} ℝ)$
178	177	biimpd	$⊢ φ \to (\{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ Y / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} : [X, Y] \underset{cn}{⟶} ℝ \to (y \in [X, Y] ⟼ ⦋ Y / x ⦌ B y) : [X, Y] \underset{cn}{⟶} ℝ)$
179	123 178	mpd	$⊢ φ \to (y \in [X, Y] ⟼ ⦋ Y / x ⦌ B y) : [X, Y] \underset{cn}{⟶} ℝ$
180		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
181	180	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
182		ioossicc	$⊢ (X, Y) \subseteq [X, Y]$
183	182 99	sstrid	$⊢ φ \to (X, Y) \subseteq ℝ$
184	183	sselda	$⊢ (φ \land y \in (X, Y)) \to y \in ℝ$
185	184	recnd	$⊢ (φ \land y \in (X, Y)) \to y \in ℂ$
186		1cnd	$⊢ (φ \land y \in (X, Y)) \to 1 \in ℂ$
187		simpr	$⊢ (φ \land y \in ℝ) \to y \in ℝ$
188	187	recnd	$⊢ (φ \land y \in ℝ) \to y \in ℂ$
189		1cnd	$⊢ (φ \land y \in ℝ) \to 1 \in ℂ$
190	181	dvmptid	$⊢ φ \to \frac{d (y \in ℝ⟼ y)}{d_{ℝ} y} = (y \in ℝ ⟼ 1)$
191	82	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
192		iooretop	$⊢ (X, Y) \in topGen (ran (.))$
193	192	a1i	$⊢ φ \to (X, Y) \in topGen (ran (.))$
194	181 188 189 190 183 191 82 193	dvmptres	$⊢ φ \to \frac{d (y \in (X, Y)⟼ y)}{d_{ℝ} y} = (y \in (X, Y) ⟼ 1)$
195	181 185 186 194 78	dvmptcmul	$⊢ φ \to \frac{d (y \in (X, Y)⟼ ⦋ Y / x ⦌ B y)}{d_{ℝ} y} = (y \in (X, Y) ⟼ ⦋ Y / x ⦌ B \cdot 1)$
196	78	mulridd	$⊢ φ \to ⦋ Y / x ⦌ B \cdot 1 = ⦋ Y / x ⦌ B$
197	196	mpteq2dv	$⊢ φ \to (y \in (X, Y) ⟼ ⦋ Y / x ⦌ B \cdot 1) = (y \in (X, Y) ⟼ ⦋ Y / x ⦌ B)$
198	195 197	eqtrd	$⊢ φ \to \frac{d (y \in (X, Y)⟼ ⦋ Y / x ⦌ B y)}{d_{ℝ} y} = (y \in (X, Y) ⟼ ⦋ Y / x ⦌ B)$
199	98 1	sseqtrrdi	$⊢ φ \to [X, Y] \subseteq S$
200	199	resmptd	$⊢ φ \to {(y \in S ⟼ ⦋ y / x ⦌ A) ↾}_{[X, Y]} = (y \in [X, Y] ⟼ ⦋ y / x ⦌ A)$
201	7	recnd	$⊢ (φ \land x \in S) \to A \in ℂ$
202	201	fmpttd	$⊢ φ \to (x \in S ⟼ A) : S ⟶ ℂ$
203	10	dmeqd	$⊢ φ \to dom \frac{d (x \in S⟼ A)}{d_{ℝ} x} = dom (x \in S ⟼ B)$
204	8	ralrimiva	$⊢ φ \to \forall x \in S B \in V$
205		dmmptg	$⊢ \forall x \in S B \in V \to dom (x \in S ⟼ B) = S$
206	204 205	syl	$⊢ φ \to dom (x \in S ⟼ B) = S$
207	203 206	eqtrd	$⊢ φ \to dom \frac{d (x \in S⟼ A)}{d_{ℝ} x} = S$
208		dvcn	$⊢ ((ℝ \subseteq ℂ \land (x \in S ⟼ A) : S ⟶ ℂ \land S \subseteq ℝ) \land dom \frac{d (x \in S⟼ A)}{d_{ℝ} x} = S) \to (x \in S ⟼ A) : S \underset{cn}{⟶} ℂ$
209	102 202 35 207 208	syl31anc	$⊢ φ \to (x \in S ⟼ A) : S \underset{cn}{⟶} ℂ$
210		cncfcdm	$⊢ (ℝ \subseteq ℂ \land (x \in S ⟼ A) : S \underset{cn}{⟶} ℂ) \to ((x \in S ⟼ A) : S \underset{cn}{⟶} ℝ \leftrightarrow (x \in S ⟼ A) : S ⟶ ℝ)$
211	100 209 210	sylancr	$⊢ φ \to ((x \in S ⟼ A) : S \underset{cn}{⟶} ℝ \leftrightarrow (x \in S ⟼ A) : S ⟶ ℝ)$
212	48 211	mpbird	$⊢ φ \to (x \in S ⟼ A) : S \underset{cn}{⟶} ℝ$
213	52 212	eqeltrrid	$⊢ φ \to (y \in S ⟼ ⦋ y / x ⦌ A) : S \underset{cn}{⟶} ℝ$
214		rescncf	$⊢ [X, Y] \subseteq S \to ((y \in S ⟼ ⦋ y / x ⦌ A) : S \underset{cn}{⟶} ℝ \to ({(y \in S ⟼ ⦋ y / x ⦌ A) ↾}_{[X, Y]}) : [X, Y] \underset{cn}{⟶} ℝ)$
215	199 213 214	sylc	$⊢ φ \to ({(y \in S ⟼ ⦋ y / x ⦌ A) ↾}_{[X, Y]}) : [X, Y] \underset{cn}{⟶} ℝ$
216	200 215	eqeltrrd	$⊢ φ \to (y \in [X, Y] ⟼ ⦋ y / x ⦌ A) : [X, Y] \underset{cn}{⟶} ℝ$
217	54	r19.21bi	$⊢ (φ \land y \in S) \to ⦋ y / x ⦌ A \in ℝ$
218	217	recnd	$⊢ (φ \land y \in S) \to ⦋ y / x ⦌ A \in ℂ$
219	43	r19.21bi	$⊢ (φ \land y \in S) \to ⦋ y / x ⦌ B \in ℝ$
220	52	oveq2i	$⊢ \frac{d (x \in S⟼ A)}{d_{ℝ} x} = \frac{d (y \in S⟼ ⦋ y / x ⦌ A)}{d_{ℝ} y}$
221	10 220 41	3eqtr3g	$⊢ φ \to \frac{d (y \in S⟼ ⦋ y / x ⦌ A)}{d_{ℝ} y} = (y \in S ⟼ ⦋ y / x ⦌ B)$
222	182 199	sstrid	$⊢ φ \to (X, Y) \subseteq S$
223	181 218 219 221 222 191 82 193	dvmptres	$⊢ φ \to \frac{d (y \in (X, Y)⟼ ⦋ y / x ⦌ A)}{d_{ℝ} y} = (y \in (X, Y) ⟼ ⦋ y / x ⦌ B)$
224	182	sseli	$⊢ y \in (X, Y) \to y \in [X, Y]$
225		simpl	$⊢ (φ \land y \in [X, Y]) \to φ$
226	199	sselda	$⊢ (φ \land y \in [X, Y]) \to y \in S$
227	16	adantr	$⊢ (φ \land y \in [X, Y]) \to Y \in S$
228	4	adantr	$⊢ (φ \land y \in [X, Y]) \to D \in ℝ$
229	29	adantr	$⊢ (φ \land y \in [X, Y]) \to X \in ℝ$
230	17	adantr	$⊢ (φ \land y \in [X, Y]) \to D \leq X$
231	140	simp2d	$⊢ (φ \land y \in [X, Y]) \to X \leq y$
232	228 229 141 230 231	letrd	$⊢ (φ \land y \in [X, Y]) \to D \leq y$
233	140	simp3d	$⊢ (φ \land y \in [X, Y]) \to y \leq Y$
234	19	adantr	$⊢ (φ \land y \in [X, Y]) \to Y \leq U$
235		simp2r	$⊢ (φ \land (y \in S \land Y \in S) \land (D \leq y \land y \leq Y \land Y \leq U)) \to Y \in S$
236		eleq1	$⊢ k = Y \to (k \in S \leftrightarrow Y \in S)$
237	236	anbi2d	$⊢ k = Y \to ((y \in S \land k \in S) \leftrightarrow (y \in S \land Y \in S))$
238		breq2	$⊢ k = Y \to (y \leq k \leftrightarrow y \leq Y)$
239		breq1	$⊢ k = Y \to (k \leq U \leftrightarrow Y \leq U)$
240	238 239	3anbi23d	$⊢ k = Y \to ((D \leq y \land y \leq k \land k \leq U) \leftrightarrow (D \leq y \land y \leq Y \land Y \leq U))$
241	237 240	3anbi23d	$⊢ k = Y \to ((φ \land (y \in S \land k \in S) \land (D \leq y \land y \leq k \land k \leq U)) \leftrightarrow (φ \land (y \in S \land Y \in S) \land (D \leq y \land y \leq Y \land Y \leq U)))$
242		vex	$⊢ k \in V$
243	242 11	csbie	$⊢ ⦋ k / x ⦌ B = C$
244	243 152	eqtr3id	$⊢ k = Y \to C = ⦋ Y / x ⦌ B$
245	244	breq1d	$⊢ k = Y \to (C \leq ⦋ y / x ⦌ B \leftrightarrow ⦋ Y / x ⦌ B \leq ⦋ y / x ⦌ B)$
246	241 245	imbi12d	$⊢ k = Y \to (((φ \land (y \in S \land k \in S) \land (D \leq y \land y \leq k \land k \leq U)) \to C \leq ⦋ y / x ⦌ B) \leftrightarrow ((φ \land (y \in S \land Y \in S) \land (D \leq y \land y \leq Y \land Y \leq U)) \to ⦋ Y / x ⦌ B \leq ⦋ y / x ⦌ B))$
247		nfv	$⊢ Ⅎ x (φ \land (y \in S \land k \in S) \land (D \leq y \land y \leq k \land k \leq U))$
248		nfcv	$⊢ \underline{Ⅎ} x C$
249		nfcv	$⊢ \underline{Ⅎ} x \leq$
250	248 249 39	nfbr	$⊢ Ⅎ x C \leq ⦋ y / x ⦌ B$
251	247 250	nfim	$⊢ Ⅎ x ((φ \land (y \in S \land k \in S) \land (D \leq y \land y \leq k \land k \leq U)) \to C \leq ⦋ y / x ⦌ B)$
252		eleq1	$⊢ x = y \to (x \in S \leftrightarrow y \in S)$
253	252	anbi1d	$⊢ x = y \to ((x \in S \land k \in S) \leftrightarrow (y \in S \land k \in S))$
254		breq2	$⊢ x = y \to (D \leq x \leftrightarrow D \leq y)$
255		breq1	$⊢ x = y \to (x \leq k \leftrightarrow y \leq k)$
256	254 255	3anbi12d	$⊢ x = y \to ((D \leq x \land x \leq k \land k \leq U) \leftrightarrow (D \leq y \land y \leq k \land k \leq U))$
257	253 256	3anbi23d	$⊢ x = y \to ((φ \land (x \in S \land k \in S) \land (D \leq x \land x \leq k \land k \leq U)) \leftrightarrow (φ \land (y \in S \land k \in S) \land (D \leq y \land y \leq k \land k \leq U)))$
258	40	breq2d	$⊢ x = y \to (C \leq B \leftrightarrow C \leq ⦋ y / x ⦌ B)$
259	257 258	imbi12d	$⊢ x = y \to (((φ \land (x \in S \land k \in S) \land (D \leq x \land x \leq k \land k \leq U)) \to C \leq B) \leftrightarrow ((φ \land (y \in S \land k \in S) \land (D \leq y \land y \leq k \land k \leq U)) \to C \leq ⦋ y / x ⦌ B))$
260	251 259 13	chvarfv	$⊢ (φ \land (y \in S \land k \in S) \land (D \leq y \land y \leq k \land k \leq U)) \to C \leq ⦋ y / x ⦌ B$
261	246 260	vtoclg	$⊢ Y \in S \to ((φ \land (y \in S \land Y \in S) \land (D \leq y \land y \leq Y \land Y \leq U)) \to ⦋ Y / x ⦌ B \leq ⦋ y / x ⦌ B)$
262	235 261	mpcom	$⊢ (φ \land (y \in S \land Y \in S) \land (D \leq y \land y \leq Y \land Y \leq U)) \to ⦋ Y / x ⦌ B \leq ⦋ y / x ⦌ B$
263	225 226 227 232 233 234 262	syl123anc	$⊢ (φ \land y \in [X, Y]) \to ⦋ Y / x ⦌ B \leq ⦋ y / x ⦌ B$
264	224 263	sylan2	$⊢ (φ \land y \in (X, Y)) \to ⦋ Y / x ⦌ B \leq ⦋ y / x ⦌ B$
265	29	rexrd	$⊢ φ \to X \in ℝ^{*}$
266	23	rexrd	$⊢ φ \to Y \in ℝ^{*}$
267		lbicc2	$⊢ (X \in ℝ^{} \land Y \in ℝ^{} \land X \leq Y) \to X \in [X, Y]$
268	265 266 18 267	syl3anc	$⊢ φ \to X \in [X, Y]$
269		ubicc2	$⊢ (X \in ℝ^{} \land Y \in ℝ^{} \land X \leq Y) \to Y \in [X, Y]$
270	265 266 18 269	syl3anc	$⊢ φ \to Y \in [X, Y]$
271		oveq2	$⊢ y = X \to ⦋ Y / x ⦌ B y = ⦋ Y / x ⦌ B X$
272		oveq2	$⊢ y = Y \to ⦋ Y / x ⦌ B y = ⦋ Y / x ⦌ B Y$
273	29 23 179 198 216 223 264 268 270 18 271 62 272 46	dvle	$⊢ φ \to ⦋ Y / x ⦌ B Y - ⦋ Y / x ⦌ B X \leq ⦋ Y / x ⦌ A - ⦋ X / x ⦌ A$
274	81 273	eqbrtrd	$⊢ φ \to ⦋ Y / x ⦌ B (Y - X) \leq ⦋ Y / x ⦌ A - ⦋ X / x ⦌ A$
275	77 55 64 274	lesubd	$⊢ φ \to ⦋ X / x ⦌ A \leq ⦋ Y / x ⦌ A - ⦋ Y / x ⦌ B (Y - X)$
276	74	recnd	$⊢ φ \to (X - ⌊X⌋) ⦋ Y / x ⦌ B \in ℂ$
277	45	recnd	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B \in ℂ$
278	55	recnd	$⊢ φ \to ⦋ Y / x ⦌ A \in ℂ$
279	276 277 278	subsubd	$⊢ φ \to (X - ⌊X⌋) ⦋ Y / x ⦌ B - ((Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A) = (X - ⌊X⌋) ⦋ Y / x ⦌ B - (Y - ⌊X⌋) ⦋ Y / x ⦌ B + ⦋ Y / x ⦌ A$
280	277 276	negsubdi2d	$⊢ φ \to - ((Y - ⌊X⌋) ⦋ Y / x ⦌ B - (X - ⌊X⌋) ⦋ Y / x ⦌ B) = (X - ⌊X⌋) ⦋ Y / x ⦌ B - (Y - ⌊X⌋) ⦋ Y / x ⦌ B$
281	31	recnd	$⊢ φ \to ⌊X⌋ \in ℂ$
282	79 80 281	nnncan2d	$⊢ φ \to Y - ⌊X⌋ - (X - ⌊X⌋) = Y - X$
283	282	oveq1d	$⊢ φ \to (Y - ⌊X⌋ - (X - ⌊X⌋)) ⦋ Y / x ⦌ B = (Y - X) ⦋ Y / x ⦌ B$
284	32	recnd	$⊢ φ \to Y - ⌊X⌋ \in ℂ$
285	57	recnd	$⊢ φ \to X - ⌊X⌋ \in ℂ$
286	284 285 78	subdird	$⊢ φ \to (Y - ⌊X⌋ - (X - ⌊X⌋)) ⦋ Y / x ⦌ B = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - (X - ⌊X⌋) ⦋ Y / x ⦌ B$
287	76	recnd	$⊢ φ \to Y - X \in ℂ$
288	287 78	mulcomd	$⊢ φ \to (Y - X) ⦋ Y / x ⦌ B = ⦋ Y / x ⦌ B (Y - X)$
289	283 286 288	3eqtr3d	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B - (X - ⌊X⌋) ⦋ Y / x ⦌ B = ⦋ Y / x ⦌ B (Y - X)$
290	289	negeqd	$⊢ φ \to - ((Y - ⌊X⌋) ⦋ Y / x ⦌ B - (X - ⌊X⌋) ⦋ Y / x ⦌ B) = - ⦋ Y / x ⦌ B (Y - X)$
291	280 290	eqtr3d	$⊢ φ \to (X - ⌊X⌋) ⦋ Y / x ⦌ B - (Y - ⌊X⌋) ⦋ Y / x ⦌ B = - ⦋ Y / x ⦌ B (Y - X)$
292	291	oveq1d	$⊢ φ \to (X - ⌊X⌋) ⦋ Y / x ⦌ B - (Y - ⌊X⌋) ⦋ Y / x ⦌ B + ⦋ Y / x ⦌ A = - ⦋ Y / x ⦌ B (Y - X) + ⦋ Y / x ⦌ A$
293	77	recnd	$⊢ φ \to ⦋ Y / x ⦌ B (Y - X) \in ℂ$
294	293 278	negsubdid	$⊢ φ \to - (⦋ Y / x ⦌ B (Y - X) - ⦋ Y / x ⦌ A) = - ⦋ Y / x ⦌ B (Y - X) + ⦋ Y / x ⦌ A$
295	292 294	eqtr4d	$⊢ φ \to (X - ⌊X⌋) ⦋ Y / x ⦌ B - (Y - ⌊X⌋) ⦋ Y / x ⦌ B + ⦋ Y / x ⦌ A = - (⦋ Y / x ⦌ B (Y - X) - ⦋ Y / x ⦌ A)$
296	293 278	negsubdi2d	$⊢ φ \to - (⦋ Y / x ⦌ B (Y - X) - ⦋ Y / x ⦌ A) = ⦋ Y / x ⦌ A - ⦋ Y / x ⦌ B (Y - X)$
297	279 295 296	3eqtrd	$⊢ φ \to (X - ⌊X⌋) ⦋ Y / x ⦌ B - ((Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A) = ⦋ Y / x ⦌ A - ⦋ Y / x ⦌ B (Y - X)$
298	275 297	breqtrrd	$⊢ φ \to ⦋ X / x ⦌ A \leq (X - ⌊X⌋) ⦋ Y / x ⦌ B - ((Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A)$
299	64 74 56 298	lesubd	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A \leq (X - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ X / x ⦌ A$
300		flle	$⊢ X \in ℝ \to ⌊X⌋ \leq X$
301	29 300	syl	$⊢ φ \to ⌊X⌋ \leq X$
302	29 31	subge0d	$⊢ φ \to (0 \leq X - ⌊X⌋ \leftrightarrow ⌊X⌋ \leq X)$
303	301 302	mpbird	$⊢ φ \to 0 \leq X - ⌊X⌋$
304	58	breq2d	$⊢ y = X \to (⦋ Y / x ⦌ B \leq ⦋ y / x ⦌ B \leftrightarrow ⦋ Y / x ⦌ B \leq ⦋ X / x ⦌ B)$
305	263	ralrimiva	$⊢ φ \to \forall y \in [X, Y] ⦋ Y / x ⦌ B \leq ⦋ y / x ⦌ B$
306	304 305 268	rspcdva	$⊢ φ \to ⦋ Y / x ⦌ B \leq ⦋ X / x ⦌ B$
307	44 60 57 303 306	lemul2ad	$⊢ φ \to (X - ⌊X⌋) ⦋ Y / x ⦌ B \leq (X - ⌊X⌋) ⦋ X / x ⦌ B$
308	74 61 64 307	lesub1dd	$⊢ φ \to (X - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ X / x ⦌ A \leq (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A$
309	56 75 65 299 308	letrd	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A \leq (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A$
310	56 65 73 309	leadd1dd	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A + \sum_{k = M}^{⌊X⌋} C \leq (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A + \sum_{k = M}^{⌊X⌋} C$
311	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20	dvfsumlem1	$⊢ φ \to H (Y) = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A + \sum_{k = M}^{⌊X⌋} C$
312	29	leidd	$⊢ φ \to X \leq X$
313	265 266 12 18 19	xrletrd	$⊢ φ \to X \leq U$
314		fllep1	$⊢ X \in ℝ \to X \leq ⌊X⌋ + 1$
315	29 314	syl	$⊢ φ \to X \leq ⌊X⌋ + 1$
316	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 15 17 312 313 315	dvfsumlem1	$⊢ φ \to H (X) = (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A + \sum_{k = M}^{⌊X⌋} C$
317	310 311 316	3brtr4d	$⊢ φ \to H (Y) \leq H (X)$
318	65 60	resubcld	$⊢ φ \to (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A - ⦋ X / x ⦌ B \in ℝ$
319	56 44	resubcld	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A - ⦋ Y / x ⦌ B \in ℝ$
320		peano2rem	$⊢ X - ⌊X⌋ \in ℝ \to X - ⌊X⌋ - 1 \in ℝ$
321	57 320	syl	$⊢ φ \to X - ⌊X⌋ - 1 \in ℝ$
322	321 60	remulcld	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B \in ℝ$
323	322 64	resubcld	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A \in ℝ$
324		peano2rem	$⊢ Y - ⌊X⌋ \in ℝ \to Y - ⌊X⌋ - 1 \in ℝ$
325	32 324	syl	$⊢ φ \to Y - ⌊X⌋ - 1 \in ℝ$
326	325 60	remulcld	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B \in ℝ$
327	326 55	resubcld	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ Y / x ⦌ A \in ℝ$
328	325 44	remulcld	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B \in ℝ$
329	328 55	resubcld	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A \in ℝ$
330	322	recnd	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B \in ℂ$
331	326	recnd	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B \in ℂ$
332	330 331	subcld	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B \in ℂ$
333	332 278	addcomd	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B + ⦋ Y / x ⦌ A = ⦋ Y / x ⦌ A + (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B$
334	330 331 278	subsubd	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ((Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ Y / x ⦌ A) = (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B + ⦋ Y / x ⦌ A$
335	278 331 330	subsub2d	$⊢ φ \to ⦋ Y / x ⦌ A - ((Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B) = ⦋ Y / x ⦌ A + (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B$
336	333 334 335	3eqtr4d	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ((Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ Y / x ⦌ A) = ⦋ Y / x ⦌ A - ((Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B)$
337		1cnd	$⊢ φ \to 1 \in ℂ$
338	284 285 337	nnncan2d	$⊢ φ \to (Y - ⌊X⌋) - 1 - (X - ⌊X⌋ - 1) = Y - ⌊X⌋ - (X - ⌊X⌋)$
339	338 282	eqtrd	$⊢ φ \to (Y - ⌊X⌋) - 1 - (X - ⌊X⌋ - 1) = Y - X$
340	339	oveq1d	$⊢ φ \to ((Y - ⌊X⌋) - 1 - (X - ⌊X⌋ - 1)) ⦋ X / x ⦌ B = (Y - X) ⦋ X / x ⦌ B$
341	325	recnd	$⊢ φ \to Y - ⌊X⌋ - 1 \in ℂ$
342	321	recnd	$⊢ φ \to X - ⌊X⌋ - 1 \in ℂ$
343	60	recnd	$⊢ φ \to ⦋ X / x ⦌ B \in ℂ$
344	341 342 343	subdird	$⊢ φ \to ((Y - ⌊X⌋) - 1 - (X - ⌊X⌋ - 1)) ⦋ X / x ⦌ B = (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B$
345	287 343	mulcomd	$⊢ φ \to (Y - X) ⦋ X / x ⦌ B = ⦋ X / x ⦌ B (Y - X)$
346	340 344 345	3eqtr3d	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B = ⦋ X / x ⦌ B (Y - X)$
347	346	oveq2d	$⊢ φ \to ⦋ Y / x ⦌ A - ((Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B) = ⦋ Y / x ⦌ A - ⦋ X / x ⦌ B (Y - X)$
348	336 347	eqtrd	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ((Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ Y / x ⦌ A) = ⦋ Y / x ⦌ A - ⦋ X / x ⦌ B (Y - X)$
349	60 76	remulcld	$⊢ φ \to ⦋ X / x ⦌ B (Y - X) \in ℝ$
350		cncfmptc	$⊢ (⦋ X / x ⦌ B \in ℝ \land [X, Y] \subseteq ℂ \land ℝ \subseteq ℂ) \to (y \in [X, Y] ⟼ ⦋ X / x ⦌ B) : [X, Y] \underset{cn}{⟶} ℝ$
351	60 101 102 350	syl3anc	$⊢ φ \to (y \in [X, Y] ⟼ ⦋ X / x ⦌ B) : [X, Y] \underset{cn}{⟶} ℝ$
352		remulcl	$⊢ (⦋ X / x ⦌ B \in ℝ \land y \in ℝ) \to ⦋ X / x ⦌ B y \in ℝ$
353		simpl	$⊢ (⦋ X / x ⦌ B \in ℝ \land y \in ℝ) \to ⦋ X / x ⦌ B \in ℝ$
354	353	recnd	$⊢ (⦋ X / x ⦌ B \in ℝ \land y \in ℝ) \to ⦋ X / x ⦌ B \in ℂ$
355		simpr	$⊢ (⦋ X / x ⦌ B \in ℝ \land y \in ℝ) \to y \in ℝ$
356	355	recnd	$⊢ (⦋ X / x ⦌ B \in ℝ \land y \in ℝ) \to y \in ℂ$
357	354 356	jca	$⊢ (⦋ X / x ⦌ B \in ℝ \land y \in ℝ) \to (⦋ X / x ⦌ B \in ℂ \land y \in ℂ)$
358		ovmul	$⊢ (⦋ X / x ⦌ B \in ℂ \land y \in ℂ) \to ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y = ⦋ X / x ⦌ B y$
359	358	eqcomd	$⊢ (⦋ X / x ⦌ B \in ℂ \land y \in ℂ) \to ⦋ X / x ⦌ B y = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y$
360	357 359	syl	$⊢ (⦋ X / x ⦌ B \in ℝ \land y \in ℝ) \to ⦋ X / x ⦌ B y = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y$
361	360	eleq1d	$⊢ (⦋ X / x ⦌ B \in ℝ \land y \in ℝ) \to (⦋ X / x ⦌ B y \in ℝ \leftrightarrow ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y \in ℝ)$
362	361	biimpd	$⊢ (⦋ X / x ⦌ B \in ℝ \land y \in ℝ) \to (⦋ X / x ⦌ B y \in ℝ \to ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y \in ℝ)$
363	352 362	mpd	$⊢ (⦋ X / x ⦌ B \in ℝ \land y \in ℝ) \to ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y \in ℝ$
364	82 83 351 106 100 363	cncfmpt2ss	$⊢ φ \to (y \in [X, Y] ⟼ ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y) : [X, Y] \underset{cn}{⟶} ℝ$
365		df-mpt	$⊢ (y \in [X, Y] ⟼ ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y) = \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\}$
366	365	eleq1i	$⊢ (y \in [X, Y] ⟼ ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y) : [X, Y] \underset{cn}{⟶} ℝ \leftrightarrow \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} : [X, Y] \underset{cn}{⟶} ℝ$
367	366	biimpi	$⊢ (y \in [X, Y] ⟼ ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y) : [X, Y] \underset{cn}{⟶} ℝ \to \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} : [X, Y] \underset{cn}{⟶} ℝ$
368	364 367	syl	$⊢ φ \to \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} : [X, Y] \underset{cn}{⟶} ℝ$
369	124	a1dd	$⊢ φ \to (y \in [X, Y] \to (w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y \to y \in [X, Y]))$
370	369	impd	$⊢ φ \to ((y \in [X, Y] \land w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y) \to y \in [X, Y])$
371	343	adantr	$⊢ (φ \land y \in [X, Y]) \to ⦋ X / x ⦌ B \in ℂ$
372	371 142	jca	$⊢ (φ \land y \in [X, Y]) \to (⦋ X / x ⦌ B \in ℂ \land y \in ℂ)$
373	372 358	syl	$⊢ (φ \land y \in [X, Y]) \to ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y = ⦋ X / x ⦌ B y$
374	373	eqeq2d	$⊢ (φ \land y \in [X, Y]) \to (w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y \leftrightarrow w = ⦋ X / x ⦌ B y)$
375	374	biimpd	$⊢ (φ \land y \in [X, Y]) \to (w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y \to w = ⦋ X / x ⦌ B y)$
376	375	ex	$⊢ φ \to (y \in [X, Y] \to (w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y \to w = ⦋ X / x ⦌ B y))$
377	376	impd	$⊢ φ \to ((y \in [X, Y] \land w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y) \to w = ⦋ X / x ⦌ B y)$
378	370 377	jcad	$⊢ φ \to ((y \in [X, Y] \land w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y) \to (y \in [X, Y] \land w = ⦋ X / x ⦌ B y))$
379	124	a1dd	$⊢ φ \to (y \in [X, Y] \to (w = ⦋ X / x ⦌ B y \to y \in [X, Y]))$
380	379	impd	$⊢ φ \to ((y \in [X, Y] \land w = ⦋ X / x ⦌ B y) \to y \in [X, Y])$
381	372 359	syl	$⊢ (φ \land y \in [X, Y]) \to ⦋ X / x ⦌ B y = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y$
382	381	eqeq2d	$⊢ (φ \land y \in [X, Y]) \to (w = ⦋ X / x ⦌ B y \leftrightarrow w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)$
383	382	biimpd	$⊢ (φ \land y \in [X, Y]) \to (w = ⦋ X / x ⦌ B y \to w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)$
384	383	ex	$⊢ φ \to (y \in [X, Y] \to (w = ⦋ X / x ⦌ B y \to w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y))$
385	384	impd	$⊢ φ \to ((y \in [X, Y] \land w = ⦋ X / x ⦌ B y) \to w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)$
386	380 385	jcad	$⊢ φ \to ((y \in [X, Y] \land w = ⦋ X / x ⦌ B y) \to (y \in [X, Y] \land w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y))$
387	378 386	impbid	$⊢ φ \to ((y \in [X, Y] \land w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y) \leftrightarrow (y \in [X, Y] \land w = ⦋ X / x ⦌ B y))$
388	387	opabbidv	$⊢ φ \to \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} = \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ X / x ⦌ B y)\}$
389		df-mpt	$⊢ (y \in [X, Y] ⟼ ⦋ X / x ⦌ B y) = \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ X / x ⦌ B y)\}$
390	389	eqcomi	$⊢ \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ X / x ⦌ B y)\} = (y \in [X, Y] ⟼ ⦋ X / x ⦌ B y)$
391	390	eqeq2i	$⊢ \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} = \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ X / x ⦌ B y)\} \leftrightarrow \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} = (y \in [X, Y] ⟼ ⦋ X / x ⦌ B y)$
392	391	biimpi	$⊢ \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} = \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ X / x ⦌ B y)\} \to \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} = (y \in [X, Y] ⟼ ⦋ X / x ⦌ B y)$
393	388 392	syl	$⊢ φ \to \{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} = (y \in [X, Y] ⟼ ⦋ X / x ⦌ B y)$
394	393	eleq1d	$⊢ φ \to (\{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} : [X, Y] \underset{cn}{⟶} ℝ \leftrightarrow (y \in [X, Y] ⟼ ⦋ X / x ⦌ B y) : [X, Y] \underset{cn}{⟶} ℝ)$
395	394	biimpd	$⊢ φ \to (\{⟨y, w⟩ \| (y \in [X, Y] \land w = ⦋ X / x ⦌ B (u \in ℂ, v \in ℂ ⟼ u v) y)\} : [X, Y] \underset{cn}{⟶} ℝ \to (y \in [X, Y] ⟼ ⦋ X / x ⦌ B y) : [X, Y] \underset{cn}{⟶} ℝ)$
396	368 395	mpd	$⊢ φ \to (y \in [X, Y] ⟼ ⦋ X / x ⦌ B y) : [X, Y] \underset{cn}{⟶} ℝ$
397	181 185 186 194 343	dvmptcmul	$⊢ φ \to \frac{d (y \in (X, Y)⟼ ⦋ X / x ⦌ B y)}{d_{ℝ} y} = (y \in (X, Y) ⟼ ⦋ X / x ⦌ B \cdot 1)$
398	343	mulridd	$⊢ φ \to ⦋ X / x ⦌ B \cdot 1 = ⦋ X / x ⦌ B$
399	398	mpteq2dv	$⊢ φ \to (y \in (X, Y) ⟼ ⦋ X / x ⦌ B \cdot 1) = (y \in (X, Y) ⟼ ⦋ X / x ⦌ B)$
400	397 399	eqtrd	$⊢ φ \to \frac{d (y \in (X, Y)⟼ ⦋ X / x ⦌ B y)}{d_{ℝ} y} = (y \in (X, Y) ⟼ ⦋ X / x ⦌ B)$
401	15	adantr	$⊢ (φ \land y \in [X, Y]) \to X \in S$
402	141	rexrd	$⊢ (φ \land y \in [X, Y]) \to y \in ℝ^{*}$
403	266	adantr	$⊢ (φ \land y \in [X, Y]) \to Y \in ℝ^{*}$
404	12	adantr	$⊢ (φ \land y \in [X, Y]) \to U \in ℝ^{*}$
405	402 403 404 233 234	xrletrd	$⊢ (φ \land y \in [X, Y]) \to y \leq U$
406		vex	$⊢ y \in V$
407		eleq1	$⊢ k = y \to (k \in S \leftrightarrow y \in S)$
408	407	anbi2d	$⊢ k = y \to ((X \in S \land k \in S) \leftrightarrow (X \in S \land y \in S))$
409		breq2	$⊢ k = y \to (X \leq k \leftrightarrow X \leq y)$
410		breq1	$⊢ k = y \to (k \leq U \leftrightarrow y \leq U)$
411	409 410	3anbi23d	$⊢ k = y \to ((D \leq X \land X \leq k \land k \leq U) \leftrightarrow (D \leq X \land X \leq y \land y \leq U))$
412	408 411	3anbi23d	$⊢ k = y \to ((φ \land (X \in S \land k \in S) \land (D \leq X \land X \leq k \land k \leq U)) \leftrightarrow (φ \land (X \in S \land y \in S) \land (D \leq X \land X \leq y \land y \leq U)))$
413		csbeq1	$⊢ k = y \to ⦋ k / x ⦌ B = ⦋ y / x ⦌ B$
414	243 413	eqtr3id	$⊢ k = y \to C = ⦋ y / x ⦌ B$
415	414	breq1d	$⊢ k = y \to (C \leq ⦋ X / x ⦌ B \leftrightarrow ⦋ y / x ⦌ B \leq ⦋ X / x ⦌ B)$
416	412 415	imbi12d	$⊢ k = y \to (((φ \land (X \in S \land k \in S) \land (D \leq X \land X \leq k \land k \leq U)) \to C \leq ⦋ X / x ⦌ B) \leftrightarrow ((φ \land (X \in S \land y \in S) \land (D \leq X \land X \leq y \land y \leq U)) \to ⦋ y / x ⦌ B \leq ⦋ X / x ⦌ B))$
417		simp2l	$⊢ (φ \land (X \in S \land k \in S) \land (D \leq X \land X \leq k \land k \leq U)) \to X \in S$
418		nfv	$⊢ Ⅎ x (φ \land (X \in S \land k \in S) \land (D \leq X \land X \leq k \land k \leq U))$
419		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ X / x ⦌ B$
420	248 249 419	nfbr	$⊢ Ⅎ x C \leq ⦋ X / x ⦌ B$
421	418 420	nfim	$⊢ Ⅎ x ((φ \land (X \in S \land k \in S) \land (D \leq X \land X \leq k \land k \leq U)) \to C \leq ⦋ X / x ⦌ B)$
422		eleq1	$⊢ x = X \to (x \in S \leftrightarrow X \in S)$
423	422	anbi1d	$⊢ x = X \to ((x \in S \land k \in S) \leftrightarrow (X \in S \land k \in S))$
424		breq2	$⊢ x = X \to (D \leq x \leftrightarrow D \leq X)$
425		breq1	$⊢ x = X \to (x \leq k \leftrightarrow X \leq k)$
426	424 425	3anbi12d	$⊢ x = X \to ((D \leq x \land x \leq k \land k \leq U) \leftrightarrow (D \leq X \land X \leq k \land k \leq U))$
427	423 426	3anbi23d	$⊢ x = X \to ((φ \land (x \in S \land k \in S) \land (D \leq x \land x \leq k \land k \leq U)) \leftrightarrow (φ \land (X \in S \land k \in S) \land (D \leq X \land X \leq k \land k \leq U)))$
428		csbeq1a	$⊢ x = X \to B = ⦋ X / x ⦌ B$
429	428	breq2d	$⊢ x = X \to (C \leq B \leftrightarrow C \leq ⦋ X / x ⦌ B)$
430	427 429	imbi12d	$⊢ x = X \to (((φ \land (x \in S \land k \in S) \land (D \leq x \land x \leq k \land k \leq U)) \to C \leq B) \leftrightarrow ((φ \land (X \in S \land k \in S) \land (D \leq X \land X \leq k \land k \leq U)) \to C \leq ⦋ X / x ⦌ B))$
431	421 430 13	vtoclg1f	$⊢ X \in S \to ((φ \land (X \in S \land k \in S) \land (D \leq X \land X \leq k \land k \leq U)) \to C \leq ⦋ X / x ⦌ B)$
432	417 431	mpcom	$⊢ (φ \land (X \in S \land k \in S) \land (D \leq X \land X \leq k \land k \leq U)) \to C \leq ⦋ X / x ⦌ B$
433	406 416 432	vtocl	$⊢ (φ \land (X \in S \land y \in S) \land (D \leq X \land X \leq y \land y \leq U)) \to ⦋ y / x ⦌ B \leq ⦋ X / x ⦌ B$
434	225 401 226 230 231 405 433	syl123anc	$⊢ (φ \land y \in [X, Y]) \to ⦋ y / x ⦌ B \leq ⦋ X / x ⦌ B$
435	224 434	sylan2	$⊢ (φ \land y \in (X, Y)) \to ⦋ y / x ⦌ B \leq ⦋ X / x ⦌ B$
436		oveq2	$⊢ y = X \to ⦋ X / x ⦌ B y = ⦋ X / x ⦌ B X$
437		oveq2	$⊢ y = Y \to ⦋ X / x ⦌ B y = ⦋ X / x ⦌ B Y$
438	29 23 216 223 396 400 435 268 270 18 62 436 46 437	dvle	$⊢ φ \to ⦋ Y / x ⦌ A - ⦋ X / x ⦌ A \leq ⦋ X / x ⦌ B Y - ⦋ X / x ⦌ B X$
439	343 79 80	subdid	$⊢ φ \to ⦋ X / x ⦌ B (Y - X) = ⦋ X / x ⦌ B Y - ⦋ X / x ⦌ B X$
440	438 439	breqtrrd	$⊢ φ \to ⦋ Y / x ⦌ A - ⦋ X / x ⦌ A \leq ⦋ X / x ⦌ B (Y - X)$
441	55 64 349 440	subled	$⊢ φ \to ⦋ Y / x ⦌ A - ⦋ X / x ⦌ B (Y - X) \leq ⦋ X / x ⦌ A$
442	348 441	eqbrtrd	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ((Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ Y / x ⦌ A) \leq ⦋ X / x ⦌ A$
443	322 327 64 442	subled	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A \leq (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ Y / x ⦌ A$
444	325	renegcld	$⊢ φ \to - (Y - ⌊X⌋ - 1) \in ℝ$
445		1red	$⊢ φ \to 1 \in ℝ$
446	23 31 445	lesubadd2d	$⊢ φ \to (Y - ⌊X⌋ \leq 1 \leftrightarrow Y \leq ⌊X⌋ + 1)$
447	20 446	mpbird	$⊢ φ \to Y - ⌊X⌋ \leq 1$
448	32 445	suble0d	$⊢ φ \to (Y - ⌊X⌋ - 1 \leq 0 \leftrightarrow Y - ⌊X⌋ \leq 1)$
449	447 448	mpbird	$⊢ φ \to Y - ⌊X⌋ - 1 \leq 0$
450	325	le0neg1d	$⊢ φ \to (Y - ⌊X⌋ - 1 \leq 0 \leftrightarrow 0 \leq - (Y - ⌊X⌋ - 1))$
451	449 450	mpbid	$⊢ φ \to 0 \leq - (Y - ⌊X⌋ - 1)$
452	44 60 444 451 306	lemul2ad	$⊢ φ \to (- (Y - ⌊X⌋ - 1)) ⦋ Y / x ⦌ B \leq (- (Y - ⌊X⌋ - 1)) ⦋ X / x ⦌ B$
453	341 78	mulneg1d	$⊢ φ \to (- (Y - ⌊X⌋ - 1)) ⦋ Y / x ⦌ B = - (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B$
454	341 343	mulneg1d	$⊢ φ \to (- (Y - ⌊X⌋ - 1)) ⦋ X / x ⦌ B = - (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B$
455	452 453 454	3brtr3d	$⊢ φ \to - (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B \leq - (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B$
456	326 328	lenegd	$⊢ φ \to ((Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B \leq (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B \leftrightarrow - (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B \leq - (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B)$
457	455 456	mpbird	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B \leq (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B$
458	326 328 55 457	lesub1dd	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ Y / x ⦌ A \leq (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A$
459	323 327 329 443 458	letrd	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A \leq (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A$
460	285 337 343	subdird	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B = (X - ⌊X⌋) ⦋ X / x ⦌ B - 1 ⦋ X / x ⦌ B$
461	343	mullidd	$⊢ φ \to 1 ⦋ X / x ⦌ B = ⦋ X / x ⦌ B$
462	461	oveq2d	$⊢ φ \to (X - ⌊X⌋) ⦋ X / x ⦌ B - 1 ⦋ X / x ⦌ B = (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ B$
463	460 462	eqtrd	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B = (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ B$
464	463	oveq1d	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A = (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ B - ⦋ X / x ⦌ A$
465	284 337 78	subdird	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - 1 ⦋ Y / x ⦌ B$
466	78	mullidd	$⊢ φ \to 1 ⦋ Y / x ⦌ B = ⦋ Y / x ⦌ B$
467	466	oveq2d	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B - 1 ⦋ Y / x ⦌ B = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ B$
468	465 467	eqtrd	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ B$
469	468	oveq1d	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A$
470	459 464 469	3brtr3d	$⊢ φ \to (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ B - ⦋ X / x ⦌ A \leq (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A$
471	61	recnd	$⊢ φ \to (X - ⌊X⌋) ⦋ X / x ⦌ B \in ℂ$
472	64	recnd	$⊢ φ \to ⦋ X / x ⦌ A \in ℂ$
473	471 472 343	sub32d	$⊢ φ \to (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A - ⦋ X / x ⦌ B = (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ B - ⦋ X / x ⦌ A$
474	277 278 78	sub32d	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A - ⦋ Y / x ⦌ B = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A$
475	470 473 474	3brtr4d	$⊢ φ \to (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A - ⦋ X / x ⦌ B \leq (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A - ⦋ Y / x ⦌ B$
476	318 319 73 475	leadd1dd	$⊢ φ \to ((X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A) - ⦋ X / x ⦌ B + \sum_{k = M}^{⌊X⌋} C \leq ((Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A) - ⦋ Y / x ⦌ B + \sum_{k = M}^{⌊X⌋} C$
477	65	recnd	$⊢ φ \to (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A \in ℂ$
478	73	recnd	$⊢ φ \to \sum_{k = M}^{⌊X⌋} C \in ℂ$
479	477 478 343	addsubd	$⊢ φ \to ((X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A) + \sum_{k = M}^{⌊X⌋} C - ⦋ X / x ⦌ B = ((X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A) - ⦋ X / x ⦌ B + \sum_{k = M}^{⌊X⌋} C$
480	56	recnd	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A \in ℂ$
481	480 478 78	addsubd	$⊢ φ \to ((Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A) + \sum_{k = M}^{⌊X⌋} C - ⦋ Y / x ⦌ B = ((Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A) - ⦋ Y / x ⦌ B + \sum_{k = M}^{⌊X⌋} C$
482	476 479 481	3brtr4d	$⊢ φ \to ((X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A) + \sum_{k = M}^{⌊X⌋} C - ⦋ X / x ⦌ B \leq ((Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A) + \sum_{k = M}^{⌊X⌋} C - ⦋ Y / x ⦌ B$
483	316	oveq1d	$⊢ φ \to H (X) - ⦋ X / x ⦌ B = ((X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A) + \sum_{k = M}^{⌊X⌋} C - ⦋ X / x ⦌ B$
484	311	oveq1d	$⊢ φ \to H (Y) - ⦋ Y / x ⦌ B = ((Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A) + \sum_{k = M}^{⌊X⌋} C - ⦋ Y / x ⦌ B$
485	482 483 484	3brtr4d	$⊢ φ \to H (X) - ⦋ X / x ⦌ B \leq H (Y) - ⦋ Y / x ⦌ B$
486	317 485	jca	$⊢ φ \to (H (Y) \leq H (X) \land H (X) - ⦋ X / x ⦌ B \leq H (Y) - ⦋ Y / x ⦌ B)$

Metamath Proof Explorer

Theorem gg-dvfsumlem2

Proof