dvfsumlem2OLD

Description: Obsolete version of dvfsumlem2 as of 17-Apr-2025. (Contributed by Mario Carneiro, 17-May-2016) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		dvfsum.s	$⊢ S = (T, +∞)$
2		dvfsum.z	$⊢ Z = ℤ_{\geq M}$
3		dvfsum.m	$⊢ φ \to M \in ℤ$
4		dvfsum.d	$⊢ φ \to D \in ℝ$
5		dvfsum.md	$⊢ φ \to M \leq D + 1$
6		dvfsum.t	$⊢ φ \to T \in ℝ$
7		dvfsum.a	$⊢ (φ \land x \in S) \to A \in ℝ$
8		dvfsum.b1	$⊢ (φ \land x \in S) \to B \in V$
9		dvfsum.b2	$⊢ (φ \land x \in Z) \to B \in ℝ$
10		dvfsum.b3	$⊢ φ \to \frac{d (x \in S⟼ A)}{d_{ℝ} x} = (x \in S ⟼ B)$
11		dvfsum.c	$⊢ x = k \to B = C$
12		dvfsum.u	$⊢ φ \to U \in ℝ^{*}$
13		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		dvfsum.h	$⊢ H = (x \in S ⟼ (x - ⌊x⌋) B + \sum_{k = M}^{⌊x⌋} C - A)$
15		dvfsumlem1.1	$⊢ φ \to X \in S$
16		dvfsumlem1.2	$⊢ φ \to Y \in S$
17		dvfsumlem1.3	$⊢ φ \to D \leq X$
18		dvfsumlem1.4	$⊢ φ \to X \leq Y$
19		dvfsumlem1.5	$⊢ φ \to Y \leq U$
20		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	mulcn	$⊢ \times \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
84		pnfxr	$⊢ +∞ \in ℝ^{*}$
85	84	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
86	28	simprd	$⊢ φ \to T < X$
87	23	ltpnfd	$⊢ φ \to Y < +∞$
88		iccssioo	$⊢ ((T \in ℝ^{} \land +∞ \in ℝ^{}) \land (T < X \land Y < +∞)) \to [X, Y] \subseteq (T, +∞)$
89	25 85 86 87 88	syl22anc	$⊢ φ \to [X, Y] \subseteq (T, +∞)$
90	89 21	sstrdi	$⊢ φ \to [X, Y] \subseteq ℝ$
91		ax-resscn	$⊢ ℝ \subseteq ℂ$
92	90 91	sstrdi	$⊢ φ \to [X, Y] \subseteq ℂ$
93	91	a1i	$⊢ φ \to ℝ \subseteq ℂ$
94		cncfmptc	$⊢ (⦋ Y / x ⦌ B \in ℝ \land [X, Y] \subseteq ℂ \land ℝ \subseteq ℂ) \to (y \in [X, Y] ⟼ ⦋ Y / x ⦌ B) : [X, Y] \underset{cn}{⟶} ℝ$
95	44 92 93 94	syl3anc	$⊢ φ \to (y \in [X, Y] ⟼ ⦋ Y / x ⦌ B) : [X, Y] \underset{cn}{⟶} ℝ$
96		cncfmptid	$⊢ ([X, Y] \subseteq ℝ \land ℝ \subseteq ℂ) \to (y \in [X, Y] ⟼ y) : [X, Y] \underset{cn}{⟶} ℝ$
97	90 91 96	sylancl	$⊢ φ \to (y \in [X, Y] ⟼ y) : [X, Y] \underset{cn}{⟶} ℝ$
98		remulcl	$⊢ (⦋ Y / x ⦌ B \in ℝ \land y \in ℝ) \to ⦋ Y / x ⦌ B y \in ℝ$
99	82 83 95 97 91 98	cncfmpt2ss	$⊢ φ \to (y \in [X, Y] ⟼ ⦋ Y / x ⦌ B y) : [X, Y] \underset{cn}{⟶} ℝ$
100		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
101	100	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
102		ioossicc	$⊢ (X, Y) \subseteq [X, Y]$
103	102 90	sstrid	$⊢ φ \to (X, Y) \subseteq ℝ$
104	103	sselda	$⊢ (φ \land y \in (X, Y)) \to y \in ℝ$
105	104	recnd	$⊢ (φ \land y \in (X, Y)) \to y \in ℂ$
106		1cnd	$⊢ (φ \land y \in (X, Y)) \to 1 \in ℂ$
107		simpr	$⊢ (φ \land y \in ℝ) \to y \in ℝ$
108	107	recnd	$⊢ (φ \land y \in ℝ) \to y \in ℂ$
109		1cnd	$⊢ (φ \land y \in ℝ) \to 1 \in ℂ$
110	101	dvmptid	$⊢ φ \to \frac{d (y \in ℝ⟼ y)}{d_{ℝ} y} = (y \in ℝ ⟼ 1)$
111	82	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
112		iooretop	$⊢ (X, Y) \in topGen (ran (.))$
113	112	a1i	$⊢ φ \to (X, Y) \in topGen (ran (.))$
114	101 108 109 110 103 111 82 113	dvmptres	$⊢ φ \to \frac{d (y \in (X, Y)⟼ y)}{d_{ℝ} y} = (y \in (X, Y) ⟼ 1)$
115	101 105 106 114 78	dvmptcmul	$⊢ φ \to \frac{d (y \in (X, Y)⟼ ⦋ Y / x ⦌ B y)}{d_{ℝ} y} = (y \in (X, Y) ⟼ ⦋ Y / x ⦌ B \cdot 1)$
116	78	mulridd	$⊢ φ \to ⦋ Y / x ⦌ B \cdot 1 = ⦋ Y / x ⦌ B$
117	116	mpteq2dv	$⊢ φ \to (y \in (X, Y) ⟼ ⦋ Y / x ⦌ B \cdot 1) = (y \in (X, Y) ⟼ ⦋ Y / x ⦌ B)$
118	115 117	eqtrd	$⊢ φ \to \frac{d (y \in (X, Y)⟼ ⦋ Y / x ⦌ B y)}{d_{ℝ} y} = (y \in (X, Y) ⟼ ⦋ Y / x ⦌ B)$
119	89 1	sseqtrrdi	$⊢ φ \to [X, Y] \subseteq S$
120	119	resmptd	$⊢ φ \to {(y \in S ⟼ ⦋ y / x ⦌ A) ↾}_{[X, Y]} = (y \in [X, Y] ⟼ ⦋ y / x ⦌ A)$
121	7	recnd	$⊢ (φ \land x \in S) \to A \in ℂ$
122	121	fmpttd	$⊢ φ \to (x \in S ⟼ A) : S ⟶ ℂ$
123	10	dmeqd	$⊢ φ \to dom \frac{d (x \in S⟼ A)}{d_{ℝ} x} = dom (x \in S ⟼ B)$
124	8	ralrimiva	$⊢ φ \to \forall x \in S B \in V$
125		dmmptg	$⊢ \forall x \in S B \in V \to dom (x \in S ⟼ B) = S$
126	124 125	syl	$⊢ φ \to dom (x \in S ⟼ B) = S$
127	123 126	eqtrd	$⊢ φ \to dom \frac{d (x \in S⟼ A)}{d_{ℝ} x} = S$
128		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}{⟶} ℂ$
129	93 122 35 127 128	syl31anc	$⊢ φ \to (x \in S ⟼ A) : S \underset{cn}{⟶} ℂ$
130		cncfcdm	$⊢ (ℝ \subseteq ℂ \land (x \in S ⟼ A) : S \underset{cn}{⟶} ℂ) \to ((x \in S ⟼ A) : S \underset{cn}{⟶} ℝ \leftrightarrow (x \in S ⟼ A) : S ⟶ ℝ)$
131	91 129 130	sylancr	$⊢ φ \to ((x \in S ⟼ A) : S \underset{cn}{⟶} ℝ \leftrightarrow (x \in S ⟼ A) : S ⟶ ℝ)$
132	48 131	mpbird	$⊢ φ \to (x \in S ⟼ A) : S \underset{cn}{⟶} ℝ$
133	52 132	eqeltrrid	$⊢ φ \to (y \in S ⟼ ⦋ y / x ⦌ A) : S \underset{cn}{⟶} ℝ$
134		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}{⟶} ℝ)$
135	119 133 134	sylc	$⊢ φ \to ({(y \in S ⟼ ⦋ y / x ⦌ A) ↾}_{[X, Y]}) : [X, Y] \underset{cn}{⟶} ℝ$
136	120 135	eqeltrrd	$⊢ φ \to (y \in [X, Y] ⟼ ⦋ y / x ⦌ A) : [X, Y] \underset{cn}{⟶} ℝ$
137	54	r19.21bi	$⊢ (φ \land y \in S) \to ⦋ y / x ⦌ A \in ℝ$
138	137	recnd	$⊢ (φ \land y \in S) \to ⦋ y / x ⦌ A \in ℂ$
139	43	r19.21bi	$⊢ (φ \land y \in S) \to ⦋ y / x ⦌ B \in ℝ$
140	52	oveq2i	$⊢ \frac{d (x \in S⟼ A)}{d_{ℝ} x} = \frac{d (y \in S⟼ ⦋ y / x ⦌ A)}{d_{ℝ} y}$
141	10 140 41	3eqtr3g	$⊢ φ \to \frac{d (y \in S⟼ ⦋ y / x ⦌ A)}{d_{ℝ} y} = (y \in S ⟼ ⦋ y / x ⦌ B)$
142	102 119	sstrid	$⊢ φ \to (X, Y) \subseteq S$
143	101 138 139 141 142 111 82 113	dvmptres	$⊢ φ \to \frac{d (y \in (X, Y)⟼ ⦋ y / x ⦌ A)}{d_{ℝ} y} = (y \in (X, Y) ⟼ ⦋ y / x ⦌ B)$
144	102	sseli	$⊢ y \in (X, Y) \to y \in [X, Y]$
145		simpl	$⊢ (φ \land y \in [X, Y]) \to φ$
146	119	sselda	$⊢ (φ \land y \in [X, Y]) \to y \in S$
147	16	adantr	$⊢ (φ \land y \in [X, Y]) \to Y \in S$
148	4	adantr	$⊢ (φ \land y \in [X, Y]) \to D \in ℝ$
149	29	adantr	$⊢ (φ \land y \in [X, Y]) \to X \in ℝ$
150		elicc2	$⊢ (X \in ℝ \land Y \in ℝ) \to (y \in [X, Y] \leftrightarrow (y \in ℝ \land X \leq y \land y \leq Y))$
151	29 23 150	syl2anc	$⊢ φ \to (y \in [X, Y] \leftrightarrow (y \in ℝ \land X \leq y \land y \leq Y))$
152	151	biimpa	$⊢ (φ \land y \in [X, Y]) \to (y \in ℝ \land X \leq y \land y \leq Y)$
153	152	simp1d	$⊢ (φ \land y \in [X, Y]) \to y \in ℝ$
154	17	adantr	$⊢ (φ \land y \in [X, Y]) \to D \leq X$
155	152	simp2d	$⊢ (φ \land y \in [X, Y]) \to X \leq y$
156	148 149 153 154 155	letrd	$⊢ (φ \land y \in [X, Y]) \to D \leq y$
157	152	simp3d	$⊢ (φ \land y \in [X, Y]) \to y \leq Y$
158	19	adantr	$⊢ (φ \land y \in [X, Y]) \to Y \leq U$
159		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$
160		eleq1	$⊢ k = Y \to (k \in S \leftrightarrow Y \in S)$
161	160	anbi2d	$⊢ k = Y \to ((y \in S \land k \in S) \leftrightarrow (y \in S \land Y \in S))$
162		breq2	$⊢ k = Y \to (y \leq k \leftrightarrow y \leq Y)$
163		breq1	$⊢ k = Y \to (k \leq U \leftrightarrow Y \leq U)$
164	162 163	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))$
165	161 164	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)))$
166		vex	$⊢ k \in V$
167	166 11	csbie	$⊢ ⦋ k / x ⦌ B = C$
168		csbeq1	$⊢ k = Y \to ⦋ k / x ⦌ B = ⦋ Y / x ⦌ B$
169	167 168	eqtr3id	$⊢ k = Y \to C = ⦋ Y / x ⦌ B$
170	169	breq1d	$⊢ k = Y \to (C \leq ⦋ y / x ⦌ B \leftrightarrow ⦋ Y / x ⦌ B \leq ⦋ y / x ⦌ B)$
171	165 170	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))$
172		nfv	$⊢ Ⅎ x (φ \land (y \in S \land k \in S) \land (D \leq y \land y \leq k \land k \leq U))$
173		nfcv	$⊢ \underline{Ⅎ} x C$
174		nfcv	$⊢ \underline{Ⅎ} x \leq$
175	173 174 39	nfbr	$⊢ Ⅎ x C \leq ⦋ y / x ⦌ B$
176	172 175	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)$
177		eleq1	$⊢ x = y \to (x \in S \leftrightarrow y \in S)$
178	177	anbi1d	$⊢ x = y \to ((x \in S \land k \in S) \leftrightarrow (y \in S \land k \in S))$
179		breq2	$⊢ x = y \to (D \leq x \leftrightarrow D \leq y)$
180		breq1	$⊢ x = y \to (x \leq k \leftrightarrow y \leq k)$
181	179 180	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))$
182	178 181	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)))$
183	40	breq2d	$⊢ x = y \to (C \leq B \leftrightarrow C \leq ⦋ y / x ⦌ B)$
184	182 183	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))$
185	176 184 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$
186	171 185	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)$
187	159 186	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$
188	145 146 147 156 157 158 187	syl123anc	$⊢ (φ \land y \in [X, Y]) \to ⦋ Y / x ⦌ B \leq ⦋ y / x ⦌ B$
189	144 188	sylan2	$⊢ (φ \land y \in (X, Y)) \to ⦋ Y / x ⦌ B \leq ⦋ y / x ⦌ B$
190	29	rexrd	$⊢ φ \to X \in ℝ^{*}$
191	23	rexrd	$⊢ φ \to Y \in ℝ^{*}$
192		lbicc2	$⊢ (X \in ℝ^{} \land Y \in ℝ^{} \land X \leq Y) \to X \in [X, Y]$
193	190 191 18 192	syl3anc	$⊢ φ \to X \in [X, Y]$
194		ubicc2	$⊢ (X \in ℝ^{} \land Y \in ℝ^{} \land X \leq Y) \to Y \in [X, Y]$
195	190 191 18 194	syl3anc	$⊢ φ \to Y \in [X, Y]$
196		oveq2	$⊢ y = X \to ⦋ Y / x ⦌ B y = ⦋ Y / x ⦌ B X$
197		oveq2	$⊢ y = Y \to ⦋ Y / x ⦌ B y = ⦋ Y / x ⦌ B Y$
198	29 23 99 118 136 143 189 193 195 18 196 62 197 46	dvle	$⊢ φ \to ⦋ Y / x ⦌ B Y - ⦋ Y / x ⦌ B X \leq ⦋ Y / x ⦌ A - ⦋ X / x ⦌ A$
199	81 198	eqbrtrd	$⊢ φ \to ⦋ Y / x ⦌ B (Y - X) \leq ⦋ Y / x ⦌ A - ⦋ X / x ⦌ A$
200	77 55 64 199	lesubd	$⊢ φ \to ⦋ X / x ⦌ A \leq ⦋ Y / x ⦌ A - ⦋ Y / x ⦌ B (Y - X)$
201	74	recnd	$⊢ φ \to (X - ⌊X⌋) ⦋ Y / x ⦌ B \in ℂ$
202	45	recnd	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B \in ℂ$
203	55	recnd	$⊢ φ \to ⦋ Y / x ⦌ A \in ℂ$
204	201 202 203	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$
205	202 201	negsubdi2d	$⊢ φ \to - ((Y - ⌊X⌋) ⦋ Y / x ⦌ B - (X - ⌊X⌋) ⦋ Y / x ⦌ B) = (X - ⌊X⌋) ⦋ Y / x ⦌ B - (Y - ⌊X⌋) ⦋ Y / x ⦌ B$
206	31	recnd	$⊢ φ \to ⌊X⌋ \in ℂ$
207	79 80 206	nnncan2d	$⊢ φ \to Y - ⌊X⌋ - (X - ⌊X⌋) = Y - X$
208	207	oveq1d	$⊢ φ \to (Y - ⌊X⌋ - (X - ⌊X⌋)) ⦋ Y / x ⦌ B = (Y - X) ⦋ Y / x ⦌ B$
209	32	recnd	$⊢ φ \to Y - ⌊X⌋ \in ℂ$
210	57	recnd	$⊢ φ \to X - ⌊X⌋ \in ℂ$
211	209 210 78	subdird	$⊢ φ \to (Y - ⌊X⌋ - (X - ⌊X⌋)) ⦋ Y / x ⦌ B = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - (X - ⌊X⌋) ⦋ Y / x ⦌ B$
212	76	recnd	$⊢ φ \to Y - X \in ℂ$
213	212 78	mulcomd	$⊢ φ \to (Y - X) ⦋ Y / x ⦌ B = ⦋ Y / x ⦌ B (Y - X)$
214	208 211 213	3eqtr3d	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B - (X - ⌊X⌋) ⦋ Y / x ⦌ B = ⦋ Y / x ⦌ B (Y - X)$
215	214	negeqd	$⊢ φ \to - ((Y - ⌊X⌋) ⦋ Y / x ⦌ B - (X - ⌊X⌋) ⦋ Y / x ⦌ B) = - ⦋ Y / x ⦌ B (Y - X)$
216	205 215	eqtr3d	$⊢ φ \to (X - ⌊X⌋) ⦋ Y / x ⦌ B - (Y - ⌊X⌋) ⦋ Y / x ⦌ B = - ⦋ Y / x ⦌ B (Y - X)$
217	216	oveq1d	$⊢ φ \to (X - ⌊X⌋) ⦋ Y / x ⦌ B - (Y - ⌊X⌋) ⦋ Y / x ⦌ B + ⦋ Y / x ⦌ A = - ⦋ Y / x ⦌ B (Y - X) + ⦋ Y / x ⦌ A$
218	77	recnd	$⊢ φ \to ⦋ Y / x ⦌ B (Y - X) \in ℂ$
219	218 203	negsubdid	$⊢ φ \to - (⦋ Y / x ⦌ B (Y - X) - ⦋ Y / x ⦌ A) = - ⦋ Y / x ⦌ B (Y - X) + ⦋ Y / x ⦌ A$
220	217 219	eqtr4d	$⊢ φ \to (X - ⌊X⌋) ⦋ Y / x ⦌ B - (Y - ⌊X⌋) ⦋ Y / x ⦌ B + ⦋ Y / x ⦌ A = - (⦋ Y / x ⦌ B (Y - X) - ⦋ Y / x ⦌ A)$
221	218 203	negsubdi2d	$⊢ φ \to - (⦋ Y / x ⦌ B (Y - X) - ⦋ Y / x ⦌ A) = ⦋ Y / x ⦌ A - ⦋ Y / x ⦌ B (Y - X)$
222	204 220 221	3eqtrd	$⊢ φ \to (X - ⌊X⌋) ⦋ Y / x ⦌ B - ((Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A) = ⦋ Y / x ⦌ A - ⦋ Y / x ⦌ B (Y - X)$
223	200 222	breqtrrd	$⊢ φ \to ⦋ X / x ⦌ A \leq (X - ⌊X⌋) ⦋ Y / x ⦌ B - ((Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A)$
224	64 74 56 223	lesubd	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A \leq (X - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ X / x ⦌ A$
225		flle	$⊢ X \in ℝ \to ⌊X⌋ \leq X$
226	29 225	syl	$⊢ φ \to ⌊X⌋ \leq X$
227	29 31	subge0d	$⊢ φ \to (0 \leq X - ⌊X⌋ \leftrightarrow ⌊X⌋ \leq X)$
228	226 227	mpbird	$⊢ φ \to 0 \leq X - ⌊X⌋$
229	58	breq2d	$⊢ y = X \to (⦋ Y / x ⦌ B \leq ⦋ y / x ⦌ B \leftrightarrow ⦋ Y / x ⦌ B \leq ⦋ X / x ⦌ B)$
230	188	ralrimiva	$⊢ φ \to \forall y \in [X, Y] ⦋ Y / x ⦌ B \leq ⦋ y / x ⦌ B$
231	229 230 193	rspcdva	$⊢ φ \to ⦋ Y / x ⦌ B \leq ⦋ X / x ⦌ B$
232	44 60 57 228 231	lemul2ad	$⊢ φ \to (X - ⌊X⌋) ⦋ Y / x ⦌ B \leq (X - ⌊X⌋) ⦋ X / x ⦌ B$
233	74 61 64 232	lesub1dd	$⊢ φ \to (X - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ X / x ⦌ A \leq (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A$
234	56 75 65 224 233	letrd	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A \leq (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A$
235	56 65 73 234	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$
236	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$
237	29	leidd	$⊢ φ \to X \leq X$
238	190 191 12 18 19	xrletrd	$⊢ φ \to X \leq U$
239		fllep1	$⊢ X \in ℝ \to X \leq ⌊X⌋ + 1$
240	29 239	syl	$⊢ φ \to X \leq ⌊X⌋ + 1$
241	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 15 17 237 238 240	dvfsumlem1	$⊢ φ \to H (X) = (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A + \sum_{k = M}^{⌊X⌋} C$
242	235 236 241	3brtr4d	$⊢ φ \to H (Y) \leq H (X)$
243	65 60	resubcld	$⊢ φ \to (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A - ⦋ X / x ⦌ B \in ℝ$
244	56 44	resubcld	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A - ⦋ Y / x ⦌ B \in ℝ$
245		peano2rem	$⊢ X - ⌊X⌋ \in ℝ \to X - ⌊X⌋ - 1 \in ℝ$
246	57 245	syl	$⊢ φ \to X - ⌊X⌋ - 1 \in ℝ$
247	246 60	remulcld	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B \in ℝ$
248	247 64	resubcld	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A \in ℝ$
249		peano2rem	$⊢ Y - ⌊X⌋ \in ℝ \to Y - ⌊X⌋ - 1 \in ℝ$
250	32 249	syl	$⊢ φ \to Y - ⌊X⌋ - 1 \in ℝ$
251	250 60	remulcld	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B \in ℝ$
252	251 55	resubcld	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ Y / x ⦌ A \in ℝ$
253	250 44	remulcld	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B \in ℝ$
254	253 55	resubcld	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A \in ℝ$
255	247	recnd	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B \in ℂ$
256	251	recnd	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B \in ℂ$
257	255 256	subcld	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B \in ℂ$
258	257 203	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$
259	255 256 203	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$
260	203 256 255	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$
261	258 259 260	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)$
262		1cnd	$⊢ φ \to 1 \in ℂ$
263	209 210 262	nnncan2d	$⊢ φ \to (Y - ⌊X⌋) - 1 - (X - ⌊X⌋ - 1) = Y - ⌊X⌋ - (X - ⌊X⌋)$
264	263 207	eqtrd	$⊢ φ \to (Y - ⌊X⌋) - 1 - (X - ⌊X⌋ - 1) = Y - X$
265	264	oveq1d	$⊢ φ \to ((Y - ⌊X⌋) - 1 - (X - ⌊X⌋ - 1)) ⦋ X / x ⦌ B = (Y - X) ⦋ X / x ⦌ B$
266	250	recnd	$⊢ φ \to Y - ⌊X⌋ - 1 \in ℂ$
267	246	recnd	$⊢ φ \to X - ⌊X⌋ - 1 \in ℂ$
268	60	recnd	$⊢ φ \to ⦋ X / x ⦌ B \in ℂ$
269	266 267 268	subdird	$⊢ φ \to ((Y - ⌊X⌋) - 1 - (X - ⌊X⌋ - 1)) ⦋ X / x ⦌ B = (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B$
270	212 268	mulcomd	$⊢ φ \to (Y - X) ⦋ X / x ⦌ B = ⦋ X / x ⦌ B (Y - X)$
271	265 269 270	3eqtr3d	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B = ⦋ X / x ⦌ B (Y - X)$
272	271	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)$
273	261 272	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)$
274	60 76	remulcld	$⊢ φ \to ⦋ X / x ⦌ B (Y - X) \in ℝ$
275		cncfmptc	$⊢ (⦋ X / x ⦌ B \in ℝ \land [X, Y] \subseteq ℂ \land ℝ \subseteq ℂ) \to (y \in [X, Y] ⟼ ⦋ X / x ⦌ B) : [X, Y] \underset{cn}{⟶} ℝ$
276	60 92 93 275	syl3anc	$⊢ φ \to (y \in [X, Y] ⟼ ⦋ X / x ⦌ B) : [X, Y] \underset{cn}{⟶} ℝ$
277		remulcl	$⊢ (⦋ X / x ⦌ B \in ℝ \land y \in ℝ) \to ⦋ X / x ⦌ B y \in ℝ$
278	82 83 276 97 91 277	cncfmpt2ss	$⊢ φ \to (y \in [X, Y] ⟼ ⦋ X / x ⦌ B y) : [X, Y] \underset{cn}{⟶} ℝ$
279	101 105 106 114 268	dvmptcmul	$⊢ φ \to \frac{d (y \in (X, Y)⟼ ⦋ X / x ⦌ B y)}{d_{ℝ} y} = (y \in (X, Y) ⟼ ⦋ X / x ⦌ B \cdot 1)$
280	268	mulridd	$⊢ φ \to ⦋ X / x ⦌ B \cdot 1 = ⦋ X / x ⦌ B$
281	280	mpteq2dv	$⊢ φ \to (y \in (X, Y) ⟼ ⦋ X / x ⦌ B \cdot 1) = (y \in (X, Y) ⟼ ⦋ X / x ⦌ B)$
282	279 281	eqtrd	$⊢ φ \to \frac{d (y \in (X, Y)⟼ ⦋ X / x ⦌ B y)}{d_{ℝ} y} = (y \in (X, Y) ⟼ ⦋ X / x ⦌ B)$
283	15	adantr	$⊢ (φ \land y \in [X, Y]) \to X \in S$
284	153	rexrd	$⊢ (φ \land y \in [X, Y]) \to y \in ℝ^{*}$
285	191	adantr	$⊢ (φ \land y \in [X, Y]) \to Y \in ℝ^{*}$
286	12	adantr	$⊢ (φ \land y \in [X, Y]) \to U \in ℝ^{*}$
287	284 285 286 157 158	xrletrd	$⊢ (φ \land y \in [X, Y]) \to y \leq U$
288		vex	$⊢ y \in V$
289		eleq1	$⊢ k = y \to (k \in S \leftrightarrow y \in S)$
290	289	anbi2d	$⊢ k = y \to ((X \in S \land k \in S) \leftrightarrow (X \in S \land y \in S))$
291		breq2	$⊢ k = y \to (X \leq k \leftrightarrow X \leq y)$
292		breq1	$⊢ k = y \to (k \leq U \leftrightarrow y \leq U)$
293	291 292	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))$
294	290 293	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)))$
295		csbeq1	$⊢ k = y \to ⦋ k / x ⦌ B = ⦋ y / x ⦌ B$
296	167 295	eqtr3id	$⊢ k = y \to C = ⦋ y / x ⦌ B$
297	296	breq1d	$⊢ k = y \to (C \leq ⦋ X / x ⦌ B \leftrightarrow ⦋ y / x ⦌ B \leq ⦋ X / x ⦌ B)$
298	294 297	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))$
299		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$
300		nfv	$⊢ Ⅎ x (φ \land (X \in S \land k \in S) \land (D \leq X \land X \leq k \land k \leq U))$
301		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ X / x ⦌ B$
302	173 174 301	nfbr	$⊢ Ⅎ x C \leq ⦋ X / x ⦌ B$
303	300 302	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)$
304		eleq1	$⊢ x = X \to (x \in S \leftrightarrow X \in S)$
305	304	anbi1d	$⊢ x = X \to ((x \in S \land k \in S) \leftrightarrow (X \in S \land k \in S))$
306		breq2	$⊢ x = X \to (D \leq x \leftrightarrow D \leq X)$
307		breq1	$⊢ x = X \to (x \leq k \leftrightarrow X \leq k)$
308	306 307	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))$
309	305 308	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)))$
310		csbeq1a	$⊢ x = X \to B = ⦋ X / x ⦌ B$
311	310	breq2d	$⊢ x = X \to (C \leq B \leftrightarrow C \leq ⦋ X / x ⦌ B)$
312	309 311	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))$
313	303 312 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)$
314	299 313	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$
315	288 298 314	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$
316	145 283 146 154 155 287 315	syl123anc	$⊢ (φ \land y \in [X, Y]) \to ⦋ y / x ⦌ B \leq ⦋ X / x ⦌ B$
317	144 316	sylan2	$⊢ (φ \land y \in (X, Y)) \to ⦋ y / x ⦌ B \leq ⦋ X / x ⦌ B$
318		oveq2	$⊢ y = X \to ⦋ X / x ⦌ B y = ⦋ X / x ⦌ B X$
319		oveq2	$⊢ y = Y \to ⦋ X / x ⦌ B y = ⦋ X / x ⦌ B Y$
320	29 23 136 143 278 282 317 193 195 18 62 318 46 319	dvle	$⊢ φ \to ⦋ Y / x ⦌ A - ⦋ X / x ⦌ A \leq ⦋ X / x ⦌ B Y - ⦋ X / x ⦌ B X$
321	268 79 80	subdid	$⊢ φ \to ⦋ X / x ⦌ B (Y - X) = ⦋ X / x ⦌ B Y - ⦋ X / x ⦌ B X$
322	320 321	breqtrrd	$⊢ φ \to ⦋ Y / x ⦌ A - ⦋ X / x ⦌ A \leq ⦋ X / x ⦌ B (Y - X)$
323	55 64 274 322	subled	$⊢ φ \to ⦋ Y / x ⦌ A - ⦋ X / x ⦌ B (Y - X) \leq ⦋ X / x ⦌ A$
324	273 323	eqbrtrd	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ((Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ Y / x ⦌ A) \leq ⦋ X / x ⦌ A$
325	247 252 64 324	subled	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A \leq (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ Y / x ⦌ A$
326	250	renegcld	$⊢ φ \to - (Y - ⌊X⌋ - 1) \in ℝ$
327		1red	$⊢ φ \to 1 \in ℝ$
328	23 31 327	lesubadd2d	$⊢ φ \to (Y - ⌊X⌋ \leq 1 \leftrightarrow Y \leq ⌊X⌋ + 1)$
329	20 328	mpbird	$⊢ φ \to Y - ⌊X⌋ \leq 1$
330	32 327	suble0d	$⊢ φ \to (Y - ⌊X⌋ - 1 \leq 0 \leftrightarrow Y - ⌊X⌋ \leq 1)$
331	329 330	mpbird	$⊢ φ \to Y - ⌊X⌋ - 1 \leq 0$
332	250	le0neg1d	$⊢ φ \to (Y - ⌊X⌋ - 1 \leq 0 \leftrightarrow 0 \leq - (Y - ⌊X⌋ - 1))$
333	331 332	mpbid	$⊢ φ \to 0 \leq - (Y - ⌊X⌋ - 1)$
334	44 60 326 333 231	lemul2ad	$⊢ φ \to (- (Y - ⌊X⌋ - 1)) ⦋ Y / x ⦌ B \leq (- (Y - ⌊X⌋ - 1)) ⦋ X / x ⦌ B$
335	266 78	mulneg1d	$⊢ φ \to (- (Y - ⌊X⌋ - 1)) ⦋ Y / x ⦌ B = - (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B$
336	266 268	mulneg1d	$⊢ φ \to (- (Y - ⌊X⌋ - 1)) ⦋ X / x ⦌ B = - (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B$
337	334 335 336	3brtr3d	$⊢ φ \to - (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B \leq - (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B$
338	251 253	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)$
339	337 338	mpbird	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B \leq (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B$
340	251 253 55 339	lesub1dd	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ Y / x ⦌ A \leq (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A$
341	248 252 254 325 340	letrd	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A \leq (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A$
342	210 262 268	subdird	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B = (X - ⌊X⌋) ⦋ X / x ⦌ B - 1 ⦋ X / x ⦌ B$
343	268	mullidd	$⊢ φ \to 1 ⦋ X / x ⦌ B = ⦋ X / x ⦌ B$
344	343	oveq2d	$⊢ φ \to (X - ⌊X⌋) ⦋ X / x ⦌ B - 1 ⦋ X / x ⦌ B = (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ B$
345	342 344	eqtrd	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B = (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ B$
346	345	oveq1d	$⊢ φ \to (X - ⌊X⌋ - 1) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A = (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ B - ⦋ X / x ⦌ A$
347	209 262 78	subdird	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - 1 ⦋ Y / x ⦌ B$
348	78	mullidd	$⊢ φ \to 1 ⦋ Y / x ⦌ B = ⦋ Y / x ⦌ B$
349	348	oveq2d	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B - 1 ⦋ Y / x ⦌ B = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ B$
350	347 349	eqtrd	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ B$
351	350	oveq1d	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A$
352	341 346 351	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$
353	61	recnd	$⊢ φ \to (X - ⌊X⌋) ⦋ X / x ⦌ B \in ℂ$
354	64	recnd	$⊢ φ \to ⦋ X / x ⦌ A \in ℂ$
355	353 354 268	sub32d	$⊢ φ \to (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A - ⦋ X / x ⦌ B = (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ B - ⦋ X / x ⦌ A$
356	202 203 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$
357	352 355 356	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$
358	243 244 73 357	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$
359	65	recnd	$⊢ φ \to (X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A \in ℂ$
360	73	recnd	$⊢ φ \to \sum_{k = M}^{⌊X⌋} C \in ℂ$
361	359 360 268	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$
362	56	recnd	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A \in ℂ$
363	362 360 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$
364	358 361 363	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$
365	241	oveq1d	$⊢ φ \to H (X) - ⦋ X / x ⦌ B = ((X - ⌊X⌋) ⦋ X / x ⦌ B - ⦋ X / x ⦌ A) + \sum_{k = M}^{⌊X⌋} C - ⦋ X / x ⦌ B$
366	236	oveq1d	$⊢ φ \to H (Y) - ⦋ Y / x ⦌ B = ((Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A) + \sum_{k = M}^{⌊X⌋} C - ⦋ Y / x ⦌ B$
367	364 365 366	3brtr4d	$⊢ φ \to H (X) - ⦋ X / x ⦌ B \leq H (Y) - ⦋ Y / x ⦌ B$
368	242 367	jca	$⊢ φ \to (H (Y) \leq H (X) \land H (X) - ⦋ X / x ⦌ B \leq H (Y) - ⦋ Y / x ⦌ B)$

Metamath Proof Explorer

Theorem dvfsumlem2OLD

Proof