dvfsumlem3

	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$
Assertion	dvfsumlem3	$⊢ φ \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		ioossre	$⊢ (T, +∞) \subseteq ℝ$
21	1 20	eqsstri	$⊢ S \subseteq ℝ$
22	21 16	sseldi	$⊢ φ \to Y \in ℝ$
23	21 15	sseldi	$⊢ φ \to X \in ℝ$
24		reflcl	$⊢ X \in ℝ \to ⌊X⌋ \in ℝ$
25		peano2re	$⊢ ⌊X⌋ \in ℝ \to ⌊X⌋ + 1 \in ℝ$
26	23 24 25	3syl	$⊢ φ \to ⌊X⌋ + 1 \in ℝ$
27	3	adantr	$⊢ (φ \land Y \leq ⌊X⌋ + 1) \to M \in ℤ$
28	4	adantr	$⊢ (φ \land Y \leq ⌊X⌋ + 1) \to D \in ℝ$
29	5	adantr	$⊢ (φ \land Y \leq ⌊X⌋ + 1) \to M \leq D + 1$
30	6	adantr	$⊢ (φ \land Y \leq ⌊X⌋ + 1) \to T \in ℝ$
31	7	adantlr	$⊢ ((φ \land Y \leq ⌊X⌋ + 1) \land x \in S) \to A \in ℝ$
32	8	adantlr	$⊢ ((φ \land Y \leq ⌊X⌋ + 1) \land x \in S) \to B \in V$
33	9	adantlr	$⊢ ((φ \land Y \leq ⌊X⌋ + 1) \land x \in Z) \to B \in ℝ$
34	10	adantr	$⊢ (φ \land Y \leq ⌊X⌋ + 1) \to \frac{d (x \in S⟼ A)}{d_{ℝ} x} = (x \in S ⟼ B)$
35	12	adantr	$⊢ (φ \land Y \leq ⌊X⌋ + 1) \to U \in ℝ^{*}$
36	13	3adant1r	$⊢ ((φ \land Y \leq ⌊X⌋ + 1) \land (x \in S \land k \in S) \land (D \leq x \land x \leq k \land k \leq U)) \to C \leq B$
37	15	adantr	$⊢ (φ \land Y \leq ⌊X⌋ + 1) \to X \in S$
38	16	adantr	$⊢ (φ \land Y \leq ⌊X⌋ + 1) \to Y \in S$
39	17	adantr	$⊢ (φ \land Y \leq ⌊X⌋ + 1) \to D \leq X$
40	18	adantr	$⊢ (φ \land Y \leq ⌊X⌋ + 1) \to X \leq Y$
41	19	adantr	$⊢ (φ \land Y \leq ⌊X⌋ + 1) \to Y \leq U$
42		simpr	$⊢ (φ \land Y \leq ⌊X⌋ + 1) \to Y \leq ⌊X⌋ + 1$
43	1 2 27 28 29 30 31 32 33 34 11 35 36 14 37 38 39 40 41 42	dvfsumlem2	$⊢ (φ \land Y \leq ⌊X⌋ + 1) \to (H (Y) \leq H (X) \land H (X) - ⦋ X / x ⦌ B \leq H (Y) - ⦋ Y / x ⦌ B)$
44	21	a1i	$⊢ φ \to S \subseteq ℝ$
45	44	sselda	$⊢ (φ \land x \in S) \to x \in ℝ$
46		reflcl	$⊢ x \in ℝ \to ⌊x⌋ \in ℝ$
47	45 46	syl	$⊢ (φ \land x \in S) \to ⌊x⌋ \in ℝ$
48	45 47	resubcld	$⊢ (φ \land x \in S) \to x - ⌊x⌋ \in ℝ$
49	44 7 8 10	dvmptrecl	$⊢ (φ \land x \in S) \to B \in ℝ$
50	48 49	remulcld	$⊢ (φ \land x \in S) \to (x - ⌊x⌋) B \in ℝ$
51		fzfid	$⊢ (φ \land x \in S) \to (M \dots ⌊x⌋) \in Fin$
52	9	ralrimiva	$⊢ φ \to \forall x \in Z B \in ℝ$
53	52	adantr	$⊢ (φ \land x \in S) \to \forall x \in Z B \in ℝ$
54		elfzuz	$⊢ k \in (M \dots ⌊x⌋) \to k \in ℤ_{\geq M}$
55	54 2	eleqtrrdi	$⊢ k \in (M \dots ⌊x⌋) \to k \in Z$
56	11	eleq1d	$⊢ x = k \to (B \in ℝ \leftrightarrow C \in ℝ)$
57	56	rspccva	$⊢ (\forall x \in Z B \in ℝ \land k \in Z) \to C \in ℝ$
58	53 55 57	syl2an	$⊢ ((φ \land x \in S) \land k \in (M \dots ⌊x⌋)) \to C \in ℝ$
59	51 58	fsumrecl	$⊢ (φ \land x \in S) \to \sum_{k = M}^{⌊x⌋} C \in ℝ$
60	59 7	resubcld	$⊢ (φ \land x \in S) \to \sum_{k = M}^{⌊x⌋} C - A \in ℝ$
61	50 60	readdcld	$⊢ (φ \land x \in S) \to (x - ⌊x⌋) B + \sum_{k = M}^{⌊x⌋} C - A \in ℝ$
62	61 14	fmptd	$⊢ φ \to H : S ⟶ ℝ$
63	62	adantr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H : S ⟶ ℝ$
64	16	adantr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to Y \in S$
65	63 64	ffvelrnd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (Y) \in ℝ$
66	22	adantr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to Y \in ℝ$
67		reflcl	$⊢ Y \in ℝ \to ⌊Y⌋ \in ℝ$
68	66 67	syl	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊Y⌋ \in ℝ$
69	6	adantr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to T \in ℝ$
70	23	adantr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to X \in ℝ$
71	70 24 25	3syl	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊X⌋ + 1 \in ℝ$
72	15 1	eleqtrdi	$⊢ φ \to X \in (T, +∞)$
73	6	rexrd	$⊢ φ \to T \in ℝ^{*}$
74		elioopnf	$⊢ T \in ℝ^{*} \to (X \in (T, +∞) \leftrightarrow (X \in ℝ \land T < X))$
75	73 74	syl	$⊢ φ \to (X \in (T, +∞) \leftrightarrow (X \in ℝ \land T < X))$
76	72 75	mpbid	$⊢ φ \to (X \in ℝ \land T < X)$
77	76	simprd	$⊢ φ \to T < X$
78		fllep1	$⊢ X \in ℝ \to X \leq ⌊X⌋ + 1$
79	23 78	syl	$⊢ φ \to X \leq ⌊X⌋ + 1$
80	6 23 26 77 79	ltletrd	$⊢ φ \to T < ⌊X⌋ + 1$
81	80	adantr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to T < ⌊X⌋ + 1$
82		simpr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊X⌋ + 1 \leq Y$
83	70	flcld	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊X⌋ \in ℤ$
84	83	peano2zd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊X⌋ + 1 \in ℤ$
85		flge	$⊢ (Y \in ℝ \land ⌊X⌋ + 1 \in ℤ) \to (⌊X⌋ + 1 \leq Y \leftrightarrow ⌊X⌋ + 1 \leq ⌊Y⌋)$
86	66 84 85	syl2anc	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to (⌊X⌋ + 1 \leq Y \leftrightarrow ⌊X⌋ + 1 \leq ⌊Y⌋)$
87	82 86	mpbid	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊X⌋ + 1 \leq ⌊Y⌋$
88	69 71 68 81 87	ltletrd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to T < ⌊Y⌋$
89	73	adantr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to T \in ℝ^{*}$
90		elioopnf	$⊢ T \in ℝ^{*} \to (⌊Y⌋ \in (T, +∞) \leftrightarrow (⌊Y⌋ \in ℝ \land T < ⌊Y⌋))$
91	89 90	syl	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to (⌊Y⌋ \in (T, +∞) \leftrightarrow (⌊Y⌋ \in ℝ \land T < ⌊Y⌋))$
92	68 88 91	mpbir2and	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊Y⌋ \in (T, +∞)$
93	92 1	eleqtrrdi	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊Y⌋ \in S$
94	63 93	ffvelrnd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (⌊Y⌋) \in ℝ$
95	15	adantr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to X \in S$
96	63 95	ffvelrnd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (X) \in ℝ$
97	3	adantr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to M \in ℤ$
98	4	adantr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to D \in ℝ$
99	5	adantr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to M \leq D + 1$
100	7	adantlr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land x \in S) \to A \in ℝ$
101	8	adantlr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land x \in S) \to B \in V$
102	9	adantlr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land x \in Z) \to B \in ℝ$
103	10	adantr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to \frac{d (x \in S⟼ A)}{d_{ℝ} x} = (x \in S ⟼ B)$
104	12	adantr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to U \in ℝ^{*}$
105	13	3adant1r	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land (x \in S \land k \in S) \land (D \leq x \land x \leq k \land k \leq U)) \to C \leq B$
106	17	adantr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to D \leq X$
107	70 78	syl	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to X \leq ⌊X⌋ + 1$
108	98 70 71 106 107	letrd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to D \leq ⌊X⌋ + 1$
109	98 71 68 108 87	letrd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to D \leq ⌊Y⌋$
110		flle	$⊢ Y \in ℝ \to ⌊Y⌋ \leq Y$
111	66 110	syl	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊Y⌋ \leq Y$
112	19	adantr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to Y \leq U$
113		fllep1	$⊢ Y \in ℝ \to Y \leq ⌊Y⌋ + 1$
114	66 113	syl	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to Y \leq ⌊Y⌋ + 1$
115		flidm	$⊢ Y \in ℝ \to ⌊⌊Y⌋⌋ = ⌊Y⌋$
116	66 115	syl	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊⌊Y⌋⌋ = ⌊Y⌋$
117	116	oveq1d	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊⌊Y⌋⌋ + 1 = ⌊Y⌋ + 1$
118	114 117	breqtrrd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to Y \leq ⌊⌊Y⌋⌋ + 1$
119	1 2 97 98 99 69 100 101 102 103 11 104 105 14 93 64 109 111 112 118	dvfsumlem2	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to (H (Y) \leq H (⌊Y⌋) \land H (⌊Y⌋) - ⦋ ⌊Y⌋ / x ⦌ B \leq H (Y) - ⦋ Y / x ⦌ B)$
120	119	simpld	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (Y) \leq H (⌊Y⌋)$
121		elioopnf	$⊢ T \in ℝ^{*} \to (⌊X⌋ + 1 \in (T, +∞) \leftrightarrow (⌊X⌋ + 1 \in ℝ \land T < ⌊X⌋ + 1))$
122	73 121	syl	$⊢ φ \to (⌊X⌋ + 1 \in (T, +∞) \leftrightarrow (⌊X⌋ + 1 \in ℝ \land T < ⌊X⌋ + 1))$
123	26 80 122	mpbir2and	$⊢ φ \to ⌊X⌋ + 1 \in (T, +∞)$
124	123 1	eleqtrrdi	$⊢ φ \to ⌊X⌋ + 1 \in S$
125	124	adantr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊X⌋ + 1 \in S$
126	63 125	ffvelrnd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (⌊X⌋ + 1) \in ℝ$
127	66	flcld	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊Y⌋ \in ℤ$
128		eluz2	$⊢ ⌊Y⌋ \in ℤ_{\geq (⌊X⌋ + 1)} \leftrightarrow (⌊X⌋ + 1 \in ℤ \land ⌊Y⌋ \in ℤ \land ⌊X⌋ + 1 \leq ⌊Y⌋)$
129	84 127 87 128	syl3anbrc	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊Y⌋ \in ℤ_{\geq (⌊X⌋ + 1)}$
130	63	adantr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋)) \to H : S ⟶ ℝ$
131		elfzelz	$⊢ m \in (⌊X⌋ + 1 \dots ⌊Y⌋) \to m \in ℤ$
132	131	adantl	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋)) \to m \in ℤ$
133	132	zred	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋)) \to m \in ℝ$
134	69	adantr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋)) \to T \in ℝ$
135	71	adantr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋)) \to ⌊X⌋ + 1 \in ℝ$
136	80	ad2antrr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋)) \to T < ⌊X⌋ + 1$
137		elfzle1	$⊢ m \in (⌊X⌋ + 1 \dots ⌊Y⌋) \to ⌊X⌋ + 1 \leq m$
138	137	adantl	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋)) \to ⌊X⌋ + 1 \leq m$
139	134 135 133 136 138	ltletrd	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋)) \to T < m$
140	73	ad2antrr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋)) \to T \in ℝ^{*}$
141		elioopnf	$⊢ T \in ℝ^{*} \to (m \in (T, +∞) \leftrightarrow (m \in ℝ \land T < m))$
142	140 141	syl	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋)) \to (m \in (T, +∞) \leftrightarrow (m \in ℝ \land T < m))$
143	133 139 142	mpbir2and	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋)) \to m \in (T, +∞)$
144	143 1	eleqtrrdi	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋)) \to m \in S$
145	130 144	ffvelrnd	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋)) \to H (m) \in ℝ$
146	97	adantr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to M \in ℤ$
147	98	adantr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to D \in ℝ$
148	5	ad2antrr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to M \leq D + 1$
149	69	adantr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to T \in ℝ$
150	100	adantlr	$⊢ (((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \land x \in S) \to A \in ℝ$
151	101	adantlr	$⊢ (((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \land x \in S) \to B \in V$
152	102	adantlr	$⊢ (((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \land x \in Z) \to B \in ℝ$
153	103	adantr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to \frac{d (x \in S⟼ A)}{d_{ℝ} x} = (x \in S ⟼ B)$
154	104	adantr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to U \in ℝ^{*}$
155	105	3adant1r	$⊢ (((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \land (x \in S \land k \in S) \land (D \leq x \land x \leq k \land k \leq U)) \to C \leq B$
156		elfzelz	$⊢ m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1) \to m \in ℤ$
157	156	adantl	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to m \in ℤ$
158	157	zred	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to m \in ℝ$
159	71	adantr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to ⌊X⌋ + 1 \in ℝ$
160	80	ad2antrr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to T < ⌊X⌋ + 1$
161		elfzle1	$⊢ m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1) \to ⌊X⌋ + 1 \leq m$
162	161	adantl	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to ⌊X⌋ + 1 \leq m$
163	149 159 158 160 162	ltletrd	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to T < m$
164	149	rexrd	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to T \in ℝ^{*}$
165	164 141	syl	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to (m \in (T, +∞) \leftrightarrow (m \in ℝ \land T < m))$
166	158 163 165	mpbir2and	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to m \in (T, +∞)$
167	166 1	eleqtrrdi	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to m \in S$
168		peano2re	$⊢ m \in ℝ \to m + 1 \in ℝ$
169	158 168	syl	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to m + 1 \in ℝ$
170	158	lep1d	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to m \leq m + 1$
171	149 158 169 163 170	ltletrd	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to T < m + 1$
172		elioopnf	$⊢ T \in ℝ^{*} \to (m + 1 \in (T, +∞) \leftrightarrow (m + 1 \in ℝ \land T < m + 1))$
173	164 172	syl	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to (m + 1 \in (T, +∞) \leftrightarrow (m + 1 \in ℝ \land T < m + 1))$
174	169 171 173	mpbir2and	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to m + 1 \in (T, +∞)$
175	174 1	eleqtrrdi	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to m + 1 \in S$
176	108	adantr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to D \leq ⌊X⌋ + 1$
177	147 159 158 176 162	letrd	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to D \leq m$
178	169	rexrd	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to m + 1 \in ℝ^{*}$
179	68	rexrd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊Y⌋ \in ℝ^{*}$
180	179	adantr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to ⌊Y⌋ \in ℝ^{*}$
181		elfzle2	$⊢ m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1) \to m \leq ⌊Y⌋ - 1$
182	181	adantl	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to m \leq ⌊Y⌋ - 1$
183		1red	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to 1 \in ℝ$
184	66	adantr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to Y \in ℝ$
185	184 67	syl	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to ⌊Y⌋ \in ℝ$
186		leaddsub	$⊢ (m \in ℝ \land 1 \in ℝ \land ⌊Y⌋ \in ℝ) \to (m + 1 \leq ⌊Y⌋ \leftrightarrow m \leq ⌊Y⌋ - 1)$
187	158 183 185 186	syl3anc	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to (m + 1 \leq ⌊Y⌋ \leftrightarrow m \leq ⌊Y⌋ - 1)$
188	182 187	mpbird	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to m + 1 \leq ⌊Y⌋$
189	66	rexrd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to Y \in ℝ^{*}$
190	179 189 104 111 112	xrletrd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊Y⌋ \leq U$
191	190	adantr	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to ⌊Y⌋ \leq U$
192	178 180 154 188 191	xrletrd	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to m + 1 \leq U$
193		flid	$⊢ m \in ℤ \to ⌊m⌋ = m$
194	157 193	syl	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to ⌊m⌋ = m$
195	194	eqcomd	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to m = ⌊m⌋$
196	195	oveq1d	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to m + 1 = ⌊m⌋ + 1$
197	169 196	eqled	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to m + 1 \leq ⌊m⌋ + 1$
198	1 2 146 147 148 149 150 151 152 153 11 154 155 14 167 175 177 170 192 197	dvfsumlem2	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to (H (m + 1) \leq H (m) \land H (m) - ⦋ m / x ⦌ B \leq H (m + 1) - ⦋ (m + 1) / x ⦌ B)$
199	198	simpld	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to H (m + 1) \leq H (m)$
200	129 145 199	monoord2	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (⌊Y⌋) \leq H (⌊X⌋ + 1)$
201	71	rexrd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊X⌋ + 1 \in ℝ^{*}$
202	201 179 104 87 190	xrletrd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊X⌋ + 1 \leq U$
203	71	leidd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⌊X⌋ + 1 \leq ⌊X⌋ + 1$
204	1 2 97 98 99 69 100 101 102 103 11 104 105 14 95 125 106 107 202 203	dvfsumlem2	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to (H (⌊X⌋ + 1) \leq H (X) \land H (X) - ⦋ X / x ⦌ B \leq H (⌊X⌋ + 1) - ⦋ (⌊X⌋ + 1) / x ⦌ B)$
205	204	simpld	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (⌊X⌋ + 1) \leq H (X)$
206	94 126 96 200 205	letrd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (⌊Y⌋) \leq H (X)$
207	65 94 96 120 206	letrd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (Y) \leq H (X)$
208		csbeq1	$⊢ m = X \to ⦋ m / x ⦌ B = ⦋ X / x ⦌ B$
209	208	eleq1d	$⊢ m = X \to (⦋ m / x ⦌ B \in ℝ \leftrightarrow ⦋ X / x ⦌ B \in ℝ)$
210	49	ralrimiva	$⊢ φ \to \forall x \in S B \in ℝ$
211	210	adantr	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to \forall x \in S B \in ℝ$
212		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ m / x ⦌ B$
213	212	nfel1	$⊢ Ⅎ x ⦋ m / x ⦌ B \in ℝ$
214		csbeq1a	$⊢ x = m \to B = ⦋ m / x ⦌ B$
215	214	eleq1d	$⊢ x = m \to (B \in ℝ \leftrightarrow ⦋ m / x ⦌ B \in ℝ)$
216	213 215	rspc	$⊢ m \in S \to (\forall x \in S B \in ℝ \to ⦋ m / x ⦌ B \in ℝ)$
217	211 216	mpan9	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in S) \to ⦋ m / x ⦌ B \in ℝ$
218	217	ralrimiva	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to \forall m \in S ⦋ m / x ⦌ B \in ℝ$
219	209 218 95	rspcdva	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⦋ X / x ⦌ B \in ℝ$
220	96 219	resubcld	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (X) - ⦋ X / x ⦌ B \in ℝ$
221		csbeq1	$⊢ m = ⌊Y⌋ \to ⦋ m / x ⦌ B = ⦋ ⌊Y⌋ / x ⦌ B$
222	221	eleq1d	$⊢ m = ⌊Y⌋ \to (⦋ m / x ⦌ B \in ℝ \leftrightarrow ⦋ ⌊Y⌋ / x ⦌ B \in ℝ)$
223	222 218 93	rspcdva	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⦋ ⌊Y⌋ / x ⦌ B \in ℝ$
224	94 223	resubcld	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (⌊Y⌋) - ⦋ ⌊Y⌋ / x ⦌ B \in ℝ$
225		csbeq1	$⊢ m = Y \to ⦋ m / x ⦌ B = ⦋ Y / x ⦌ B$
226	225	eleq1d	$⊢ m = Y \to (⦋ m / x ⦌ B \in ℝ \leftrightarrow ⦋ Y / x ⦌ B \in ℝ)$
227	226 218 64	rspcdva	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⦋ Y / x ⦌ B \in ℝ$
228	65 227	resubcld	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (Y) - ⦋ Y / x ⦌ B \in ℝ$
229		csbeq1	$⊢ m = ⌊X⌋ + 1 \to ⦋ m / x ⦌ B = ⦋ (⌊X⌋ + 1) / x ⦌ B$
230	229	eleq1d	$⊢ m = ⌊X⌋ + 1 \to (⦋ m / x ⦌ B \in ℝ \leftrightarrow ⦋ (⌊X⌋ + 1) / x ⦌ B \in ℝ)$
231	230 218 125	rspcdva	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to ⦋ (⌊X⌋ + 1) / x ⦌ B \in ℝ$
232	126 231	resubcld	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (⌊X⌋ + 1) - ⦋ (⌊X⌋ + 1) / x ⦌ B \in ℝ$
233	204	simprd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (X) - ⦋ X / x ⦌ B \leq H (⌊X⌋ + 1) - ⦋ (⌊X⌋ + 1) / x ⦌ B$
234		fveq2	$⊢ y = m \to H (y) = H (m)$
235		csbeq1	$⊢ y = m \to ⦋ y / x ⦌ B = ⦋ m / x ⦌ B$
236	234 235	oveq12d	$⊢ y = m \to H (y) - ⦋ y / x ⦌ B = H (m) - ⦋ m / x ⦌ B$
237		eqid	$⊢ (y \in V ⟼ H (y) - ⦋ y / x ⦌ B) = (y \in V ⟼ H (y) - ⦋ y / x ⦌ B)$
238		ovex	$⊢ H (y) - ⦋ y / x ⦌ B \in V$
239	236 237 238	fvmpt3i	$⊢ m \in V \to (y \in V ⟼ H (y) - ⦋ y / x ⦌ B) (m) = H (m) - ⦋ m / x ⦌ B$
240	239	elv	$⊢ (y \in V ⟼ H (y) - ⦋ y / x ⦌ B) (m) = H (m) - ⦋ m / x ⦌ B$
241	144 217	syldan	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋)) \to ⦋ m / x ⦌ B \in ℝ$
242	145 241	resubcld	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋)) \to H (m) - ⦋ m / x ⦌ B \in ℝ$
243	240 242	eqeltrid	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋)) \to (y \in V ⟼ H (y) - ⦋ y / x ⦌ B) (m) \in ℝ$
244	198	simprd	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to H (m) - ⦋ m / x ⦌ B \leq H (m + 1) - ⦋ (m + 1) / x ⦌ B$
245		ovex	$⊢ m + 1 \in V$
246		fveq2	$⊢ y = m + 1 \to H (y) = H (m + 1)$
247		csbeq1	$⊢ y = m + 1 \to ⦋ y / x ⦌ B = ⦋ (m + 1) / x ⦌ B$
248	246 247	oveq12d	$⊢ y = m + 1 \to H (y) - ⦋ y / x ⦌ B = H (m + 1) - ⦋ (m + 1) / x ⦌ B$
249	248 237 238	fvmpt3i	$⊢ m + 1 \in V \to (y \in V ⟼ H (y) - ⦋ y / x ⦌ B) (m + 1) = H (m + 1) - ⦋ (m + 1) / x ⦌ B$
250	245 249	ax-mp	$⊢ (y \in V ⟼ H (y) - ⦋ y / x ⦌ B) (m + 1) = H (m + 1) - ⦋ (m + 1) / x ⦌ B$
251	244 240 250	3brtr4g	$⊢ ((φ \land ⌊X⌋ + 1 \leq Y) \land m \in (⌊X⌋ + 1 \dots ⌊Y⌋ - 1)) \to (y \in V ⟼ H (y) - ⦋ y / x ⦌ B) (m) \leq (y \in V ⟼ H (y) - ⦋ y / x ⦌ B) (m + 1)$
252	129 243 251	monoord	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to (y \in V ⟼ H (y) - ⦋ y / x ⦌ B) (⌊X⌋ + 1) \leq (y \in V ⟼ H (y) - ⦋ y / x ⦌ B) (⌊Y⌋)$
253		ovex	$⊢ ⌊X⌋ + 1 \in V$
254		fveq2	$⊢ y = ⌊X⌋ + 1 \to H (y) = H (⌊X⌋ + 1)$
255		csbeq1	$⊢ y = ⌊X⌋ + 1 \to ⦋ y / x ⦌ B = ⦋ (⌊X⌋ + 1) / x ⦌ B$
256	254 255	oveq12d	$⊢ y = ⌊X⌋ + 1 \to H (y) - ⦋ y / x ⦌ B = H (⌊X⌋ + 1) - ⦋ (⌊X⌋ + 1) / x ⦌ B$
257	256 237 238	fvmpt3i	$⊢ ⌊X⌋ + 1 \in V \to (y \in V ⟼ H (y) - ⦋ y / x ⦌ B) (⌊X⌋ + 1) = H (⌊X⌋ + 1) - ⦋ (⌊X⌋ + 1) / x ⦌ B$
258	253 257	ax-mp	$⊢ (y \in V ⟼ H (y) - ⦋ y / x ⦌ B) (⌊X⌋ + 1) = H (⌊X⌋ + 1) - ⦋ (⌊X⌋ + 1) / x ⦌ B$
259		fvex	$⊢ ⌊Y⌋ \in V$
260		fveq2	$⊢ y = ⌊Y⌋ \to H (y) = H (⌊Y⌋)$
261		csbeq1	$⊢ y = ⌊Y⌋ \to ⦋ y / x ⦌ B = ⦋ ⌊Y⌋ / x ⦌ B$
262	260 261	oveq12d	$⊢ y = ⌊Y⌋ \to H (y) - ⦋ y / x ⦌ B = H (⌊Y⌋) - ⦋ ⌊Y⌋ / x ⦌ B$
263	262 237 238	fvmpt3i	$⊢ ⌊Y⌋ \in V \to (y \in V ⟼ H (y) - ⦋ y / x ⦌ B) (⌊Y⌋) = H (⌊Y⌋) - ⦋ ⌊Y⌋ / x ⦌ B$
264	259 263	ax-mp	$⊢ (y \in V ⟼ H (y) - ⦋ y / x ⦌ B) (⌊Y⌋) = H (⌊Y⌋) - ⦋ ⌊Y⌋ / x ⦌ B$
265	252 258 264	3brtr3g	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (⌊X⌋ + 1) - ⦋ (⌊X⌋ + 1) / x ⦌ B \leq H (⌊Y⌋) - ⦋ ⌊Y⌋ / x ⦌ B$
266	220 232 224 233 265	letrd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (X) - ⦋ X / x ⦌ B \leq H (⌊Y⌋) - ⦋ ⌊Y⌋ / x ⦌ B$
267	119	simprd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (⌊Y⌋) - ⦋ ⌊Y⌋ / x ⦌ B \leq H (Y) - ⦋ Y / x ⦌ B$
268	220 224 228 266 267	letrd	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to H (X) - ⦋ X / x ⦌ B \leq H (Y) - ⦋ Y / x ⦌ B$
269	207 268	jca	$⊢ (φ \land ⌊X⌋ + 1 \leq Y) \to (H (Y) \leq H (X) \land H (X) - ⦋ X / x ⦌ B \leq H (Y) - ⦋ Y / x ⦌ B)$
270	22 26 43 269	lecasei	$⊢ φ \to (H (Y) \leq H (X) \land H (X) - ⦋ X / x ⦌ B \leq H (Y) - ⦋ Y / x ⦌ B)$

Metamath Proof Explorer

Theorem dvfsumlem3

Proof