dvfsumlem1

	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	dvfsumlem1	$⊢ φ \to H (Y) = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A + \sum_{k = M}^{⌊X⌋} C$

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	22 15	sselid	$⊢ φ \to X \in ℝ$
25	24	flcld	$⊢ φ \to ⌊X⌋ \in ℤ$
26		reflcl	$⊢ X \in ℝ \to ⌊X⌋ \in ℝ$
27	24 26	syl	$⊢ φ \to ⌊X⌋ \in ℝ$
28		flle	$⊢ X \in ℝ \to ⌊X⌋ \leq X$
29	24 28	syl	$⊢ φ \to ⌊X⌋ \leq X$
30	27 24 23 29 18	letrd	$⊢ φ \to ⌊X⌋ \leq Y$
31		flbi	$⊢ (Y \in ℝ \land ⌊X⌋ \in ℤ) \to (⌊Y⌋ = ⌊X⌋ \leftrightarrow (⌊X⌋ \leq Y \land Y < ⌊X⌋ + 1))$
32	31	baibd	$⊢ ((Y \in ℝ \land ⌊X⌋ \in ℤ) \land ⌊X⌋ \leq Y) \to (⌊Y⌋ = ⌊X⌋ \leftrightarrow Y < ⌊X⌋ + 1)$
33	23 25 30 32	syl21anc	$⊢ φ \to (⌊Y⌋ = ⌊X⌋ \leftrightarrow Y < ⌊X⌋ + 1)$
34	33	biimpar	$⊢ (φ \land Y < ⌊X⌋ + 1) \to ⌊Y⌋ = ⌊X⌋$
35	34	oveq2d	$⊢ (φ \land Y < ⌊X⌋ + 1) \to Y - ⌊Y⌋ = Y - ⌊X⌋$
36	35	oveq1d	$⊢ (φ \land Y < ⌊X⌋ + 1) \to (Y - ⌊Y⌋) ⦋ Y / x ⦌ B = (Y - ⌊X⌋) ⦋ Y / x ⦌ B$
37	34	oveq2d	$⊢ (φ \land Y < ⌊X⌋ + 1) \to (M \dots ⌊Y⌋) = (M \dots ⌊X⌋)$
38	37	sumeq1d	$⊢ (φ \land Y < ⌊X⌋ + 1) \to \sum_{k = M}^{⌊Y⌋} C = \sum_{k = M}^{⌊X⌋} C$
39	38	oveq1d	$⊢ (φ \land Y < ⌊X⌋ + 1) \to \sum_{k = M}^{⌊Y⌋} C - ⦋ Y / x ⦌ A = \sum_{k = M}^{⌊X⌋} C - ⦋ Y / x ⦌ A$
40	36 39	oveq12d	$⊢ (φ \land Y < ⌊X⌋ + 1) \to (Y - ⌊Y⌋) ⦋ Y / x ⦌ B + \sum_{k = M}^{⌊Y⌋} C - ⦋ Y / x ⦌ A = (Y - ⌊X⌋) ⦋ Y / x ⦌ B + \sum_{k = M}^{⌊X⌋} C - ⦋ Y / x ⦌ A$
41		simpr	$⊢ (φ \land Y = ⌊X⌋ + 1) \to Y = ⌊X⌋ + 1$
42	24	adantr	$⊢ (φ \land Y = ⌊X⌋ + 1) \to X \in ℝ$
43	42	flcld	$⊢ (φ \land Y = ⌊X⌋ + 1) \to ⌊X⌋ \in ℤ$
44	43	peano2zd	$⊢ (φ \land Y = ⌊X⌋ + 1) \to ⌊X⌋ + 1 \in ℤ$
45	41 44	eqeltrd	$⊢ (φ \land Y = ⌊X⌋ + 1) \to Y \in ℤ$
46		flid	$⊢ Y \in ℤ \to ⌊Y⌋ = Y$
47	45 46	syl	$⊢ (φ \land Y = ⌊X⌋ + 1) \to ⌊Y⌋ = Y$
48	47 41	eqtrd	$⊢ (φ \land Y = ⌊X⌋ + 1) \to ⌊Y⌋ = ⌊X⌋ + 1$
49	48	oveq2d	$⊢ (φ \land Y = ⌊X⌋ + 1) \to Y - ⌊Y⌋ = Y - (⌊X⌋ + 1)$
50	49	oveq1d	$⊢ (φ \land Y = ⌊X⌋ + 1) \to (Y - ⌊Y⌋) ⦋ Y / x ⦌ B = (Y - (⌊X⌋ + 1)) ⦋ Y / x ⦌ B$
51	23	recnd	$⊢ φ \to Y \in ℂ$
52	27	recnd	$⊢ φ \to ⌊X⌋ \in ℂ$
53	51 52	subcld	$⊢ φ \to Y - ⌊X⌋ \in ℂ$
54		1cnd	$⊢ φ \to 1 \in ℂ$
55	22	a1i	$⊢ φ \to S \subseteq ℝ$
56	55 7 8 10	dvmptrecl	$⊢ (φ \land x \in S) \to B \in ℝ$
57	56	recnd	$⊢ (φ \land x \in S) \to B \in ℂ$
58	57	ralrimiva	$⊢ φ \to \forall x \in S B \in ℂ$
59		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ Y / x ⦌ B$
60	59	nfel1	$⊢ Ⅎ x ⦋ Y / x ⦌ B \in ℂ$
61		csbeq1a	$⊢ x = Y \to B = ⦋ Y / x ⦌ B$
62	61	eleq1d	$⊢ x = Y \to (B \in ℂ \leftrightarrow ⦋ Y / x ⦌ B \in ℂ)$
63	60 62	rspc	$⊢ Y \in S \to (\forall x \in S B \in ℂ \to ⦋ Y / x ⦌ B \in ℂ)$
64	16 58 63	sylc	$⊢ φ \to ⦋ Y / x ⦌ B \in ℂ$
65	53 54 64	subdird	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - 1 ⦋ Y / x ⦌ B$
66	51 52 54	subsub4d	$⊢ φ \to Y - ⌊X⌋ - 1 = Y - (⌊X⌋ + 1)$
67	66	oveq1d	$⊢ φ \to (Y - ⌊X⌋ - 1) ⦋ Y / x ⦌ B = (Y - (⌊X⌋ + 1)) ⦋ Y / x ⦌ B$
68	64	mulid2d	$⊢ φ \to 1 ⦋ Y / x ⦌ B = ⦋ Y / x ⦌ B$
69	68	oveq2d	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B - 1 ⦋ Y / x ⦌ B = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ B$
70	65 67 69	3eqtr3d	$⊢ φ \to (Y - (⌊X⌋ + 1)) ⦋ Y / x ⦌ B = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ B$
71	70	adantr	$⊢ (φ \land Y = ⌊X⌋ + 1) \to (Y - (⌊X⌋ + 1)) ⦋ Y / x ⦌ B = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ B$
72	50 71	eqtrd	$⊢ (φ \land Y = ⌊X⌋ + 1) \to (Y - ⌊Y⌋) ⦋ Y / x ⦌ B = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ B$
73	25	peano2zd	$⊢ φ \to ⌊X⌋ + 1 \in ℤ$
74	3	zred	$⊢ φ \to M \in ℝ$
75		peano2rem	$⊢ M \in ℝ \to M - 1 \in ℝ$
76	74 75	syl	$⊢ φ \to M - 1 \in ℝ$
77		1red	$⊢ φ \to 1 \in ℝ$
78	74 77 4	lesubaddd	$⊢ φ \to (M - 1 \leq D \leftrightarrow M \leq D + 1)$
79	5 78	mpbird	$⊢ φ \to M - 1 \leq D$
80	76 4 24 79 17	letrd	$⊢ φ \to M - 1 \leq X$
81		peano2zm	$⊢ M \in ℤ \to M - 1 \in ℤ$
82	3 81	syl	$⊢ φ \to M - 1 \in ℤ$
83		flge	$⊢ (X \in ℝ \land M - 1 \in ℤ) \to (M - 1 \leq X \leftrightarrow M - 1 \leq ⌊X⌋)$
84	24 82 83	syl2anc	$⊢ φ \to (M - 1 \leq X \leftrightarrow M - 1 \leq ⌊X⌋)$
85	80 84	mpbid	$⊢ φ \to M - 1 \leq ⌊X⌋$
86	74 77 27	lesubaddd	$⊢ φ \to (M - 1 \leq ⌊X⌋ \leftrightarrow M \leq ⌊X⌋ + 1)$
87	85 86	mpbid	$⊢ φ \to M \leq ⌊X⌋ + 1$
88		eluz2	$⊢ ⌊X⌋ + 1 \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land ⌊X⌋ + 1 \in ℤ \land M \leq ⌊X⌋ + 1)$
89	3 73 87 88	syl3anbrc	$⊢ φ \to ⌊X⌋ + 1 \in ℤ_{\geq M}$
90	9	recnd	$⊢ (φ \land x \in Z) \to B \in ℂ$
91	90	ralrimiva	$⊢ φ \to \forall x \in Z B \in ℂ$
92		elfzuz	$⊢ k \in (M \dots ⌊X⌋ + 1) \to k \in ℤ_{\geq M}$
93	92 2	eleqtrrdi	$⊢ k \in (M \dots ⌊X⌋ + 1) \to k \in Z$
94	11	eleq1d	$⊢ x = k \to (B \in ℂ \leftrightarrow C \in ℂ)$
95	94	rspccva	$⊢ (\forall x \in Z B \in ℂ \land k \in Z) \to C \in ℂ$
96	91 93 95	syl2an	$⊢ (φ \land k \in (M \dots ⌊X⌋ + 1)) \to C \in ℂ$
97		eqvisset	$⊢ k = ⌊X⌋ + 1 \to ⌊X⌋ + 1 \in V$
98		eqeq2	$⊢ k = ⌊X⌋ + 1 \to (x = k \leftrightarrow x = ⌊X⌋ + 1)$
99	98	biimpar	$⊢ (k = ⌊X⌋ + 1 \land x = ⌊X⌋ + 1) \to x = k$
100	99 11	syl	$⊢ (k = ⌊X⌋ + 1 \land x = ⌊X⌋ + 1) \to B = C$
101	97 100	csbied	$⊢ k = ⌊X⌋ + 1 \to ⦋ (⌊X⌋ + 1) / x ⦌ B = C$
102	101	eqcomd	$⊢ k = ⌊X⌋ + 1 \to C = ⦋ (⌊X⌋ + 1) / x ⦌ B$
103	89 96 102	fsumm1	$⊢ φ \to \sum_{k = M}^{⌊X⌋ + 1} C = \sum_{k = M}^{⌊X⌋ + 1 - 1} C + ⦋ (⌊X⌋ + 1) / x ⦌ B$
104		ax-1cn	$⊢ 1 \in ℂ$
105		pncan	$⊢ (⌊X⌋ \in ℂ \land 1 \in ℂ) \to ⌊X⌋ + 1 - 1 = ⌊X⌋$
106	52 104 105	sylancl	$⊢ φ \to ⌊X⌋ + 1 - 1 = ⌊X⌋$
107	106	oveq2d	$⊢ φ \to (M \dots ⌊X⌋ + 1 - 1) = (M \dots ⌊X⌋)$
108	107	sumeq1d	$⊢ φ \to \sum_{k = M}^{⌊X⌋ + 1 - 1} C = \sum_{k = M}^{⌊X⌋} C$
109	108	oveq1d	$⊢ φ \to \sum_{k = M}^{⌊X⌋ + 1 - 1} C + ⦋ (⌊X⌋ + 1) / x ⦌ B = \sum_{k = M}^{⌊X⌋} C + ⦋ (⌊X⌋ + 1) / x ⦌ B$
110	103 109	eqtrd	$⊢ φ \to \sum_{k = M}^{⌊X⌋ + 1} C = \sum_{k = M}^{⌊X⌋} C + ⦋ (⌊X⌋ + 1) / x ⦌ B$
111	110	adantr	$⊢ (φ \land Y = ⌊X⌋ + 1) \to \sum_{k = M}^{⌊X⌋ + 1} C = \sum_{k = M}^{⌊X⌋} C + ⦋ (⌊X⌋ + 1) / x ⦌ B$
112	48	oveq2d	$⊢ (φ \land Y = ⌊X⌋ + 1) \to (M \dots ⌊Y⌋) = (M \dots ⌊X⌋ + 1)$
113	112	sumeq1d	$⊢ (φ \land Y = ⌊X⌋ + 1) \to \sum_{k = M}^{⌊Y⌋} C = \sum_{k = M}^{⌊X⌋ + 1} C$
114	41	csbeq1d	$⊢ (φ \land Y = ⌊X⌋ + 1) \to ⦋ Y / x ⦌ B = ⦋ (⌊X⌋ + 1) / x ⦌ B$
115	114	oveq2d	$⊢ (φ \land Y = ⌊X⌋ + 1) \to \sum_{k = M}^{⌊X⌋} C + ⦋ Y / x ⦌ B = \sum_{k = M}^{⌊X⌋} C + ⦋ (⌊X⌋ + 1) / x ⦌ B$
116	111 113 115	3eqtr4d	$⊢ (φ \land Y = ⌊X⌋ + 1) \to \sum_{k = M}^{⌊Y⌋} C = \sum_{k = M}^{⌊X⌋} C + ⦋ Y / x ⦌ B$
117	116	oveq1d	$⊢ (φ \land Y = ⌊X⌋ + 1) \to \sum_{k = M}^{⌊Y⌋} C - ⦋ Y / x ⦌ A = \sum_{k = M}^{⌊X⌋} C + ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A$
118		fzfid	$⊢ φ \to (M \dots ⌊X⌋) \in Fin$
119		elfzuz	$⊢ k \in (M \dots ⌊X⌋) \to k \in ℤ_{\geq M}$
120	119 2	eleqtrrdi	$⊢ k \in (M \dots ⌊X⌋) \to k \in Z$
121	91 120 95	syl2an	$⊢ (φ \land k \in (M \dots ⌊X⌋)) \to C \in ℂ$
122	118 121	fsumcl	$⊢ φ \to \sum_{k = M}^{⌊X⌋} C \in ℂ$
123	7	recnd	$⊢ (φ \land x \in S) \to A \in ℂ$
124	123	ralrimiva	$⊢ φ \to \forall x \in S A \in ℂ$
125		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ Y / x ⦌ A$
126	125	nfel1	$⊢ Ⅎ x ⦋ Y / x ⦌ A \in ℂ$
127		csbeq1a	$⊢ x = Y \to A = ⦋ Y / x ⦌ A$
128	127	eleq1d	$⊢ x = Y \to (A \in ℂ \leftrightarrow ⦋ Y / x ⦌ A \in ℂ)$
129	126 128	rspc	$⊢ Y \in S \to (\forall x \in S A \in ℂ \to ⦋ Y / x ⦌ A \in ℂ)$
130	16 124 129	sylc	$⊢ φ \to ⦋ Y / x ⦌ A \in ℂ$
131	122 64 130	addsubd	$⊢ φ \to \sum_{k = M}^{⌊X⌋} C + ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A = \sum_{k = M}^{⌊X⌋} C - ⦋ Y / x ⦌ A + ⦋ Y / x ⦌ B$
132	131	adantr	$⊢ (φ \land Y = ⌊X⌋ + 1) \to \sum_{k = M}^{⌊X⌋} C + ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A = \sum_{k = M}^{⌊X⌋} C - ⦋ Y / x ⦌ A + ⦋ Y / x ⦌ B$
133	117 132	eqtrd	$⊢ (φ \land Y = ⌊X⌋ + 1) \to \sum_{k = M}^{⌊Y⌋} C - ⦋ Y / x ⦌ A = \sum_{k = M}^{⌊X⌋} C - ⦋ Y / x ⦌ A + ⦋ Y / x ⦌ B$
134	72 133	oveq12d	$⊢ (φ \land Y = ⌊X⌋ + 1) \to (Y - ⌊Y⌋) ⦋ Y / x ⦌ B + \sum_{k = M}^{⌊Y⌋} C - ⦋ Y / x ⦌ A = ((Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ B) + (\sum_{k = M}^{⌊X⌋} C - ⦋ Y / x ⦌ A) + ⦋ Y / x ⦌ B$
135	53 64	mulcld	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B \in ℂ$
136	135	adantr	$⊢ (φ \land Y = ⌊X⌋ + 1) \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B \in ℂ$
137	64	adantr	$⊢ (φ \land Y = ⌊X⌋ + 1) \to ⦋ Y / x ⦌ B \in ℂ$
138	122 130	subcld	$⊢ φ \to \sum_{k = M}^{⌊X⌋} C - ⦋ Y / x ⦌ A \in ℂ$
139	138	adantr	$⊢ (φ \land Y = ⌊X⌋ + 1) \to \sum_{k = M}^{⌊X⌋} C - ⦋ Y / x ⦌ A \in ℂ$
140	136 137 139	nppcan3d	$⊢ (φ \land Y = ⌊X⌋ + 1) \to ((Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ B) + (\sum_{k = M}^{⌊X⌋} C - ⦋ Y / x ⦌ A) + ⦋ Y / x ⦌ B = (Y - ⌊X⌋) ⦋ Y / x ⦌ B + \sum_{k = M}^{⌊X⌋} C - ⦋ Y / x ⦌ A$
141	134 140	eqtrd	$⊢ (φ \land Y = ⌊X⌋ + 1) \to (Y - ⌊Y⌋) ⦋ Y / x ⦌ B + \sum_{k = M}^{⌊Y⌋} C - ⦋ Y / x ⦌ A = (Y - ⌊X⌋) ⦋ Y / x ⦌ B + \sum_{k = M}^{⌊X⌋} C - ⦋ Y / x ⦌ A$
142		peano2re	$⊢ ⌊X⌋ \in ℝ \to ⌊X⌋ + 1 \in ℝ$
143	27 142	syl	$⊢ φ \to ⌊X⌋ + 1 \in ℝ$
144	23 143	leloed	$⊢ φ \to (Y \leq ⌊X⌋ + 1 \leftrightarrow (Y < ⌊X⌋ + 1 \lor Y = ⌊X⌋ + 1))$
145	20 144	mpbid	$⊢ φ \to (Y < ⌊X⌋ + 1 \lor Y = ⌊X⌋ + 1)$
146	40 141 145	mpjaodan	$⊢ φ \to (Y - ⌊Y⌋) ⦋ Y / x ⦌ B + \sum_{k = M}^{⌊Y⌋} C - ⦋ Y / x ⦌ A = (Y - ⌊X⌋) ⦋ Y / x ⦌ B + \sum_{k = M}^{⌊X⌋} C - ⦋ Y / x ⦌ A$
147		ovex	$⊢ (Y - ⌊Y⌋) ⦋ Y / x ⦌ B + \sum_{k = M}^{⌊Y⌋} C - ⦋ Y / x ⦌ A \in V$
148		nfcv	$⊢ \underline{Ⅎ} x Y$
149		nfcv	$⊢ \underline{Ⅎ} x (Y - ⌊Y⌋)$
150		nfcv	$⊢ \underline{Ⅎ} x \times$
151	149 150 59	nfov	$⊢ \underline{Ⅎ} x (Y - ⌊Y⌋) ⦋ Y / x ⦌ B$
152		nfcv	$⊢ \underline{Ⅎ} x +$
153		nfcv	$⊢ \underline{Ⅎ} x \sum_{k = M}^{⌊Y⌋} C$
154		nfcv	$⊢ \underline{Ⅎ} x -$
155	153 154 125	nfov	$⊢ \underline{Ⅎ} x (\sum_{k = M}^{⌊Y⌋} C - ⦋ Y / x ⦌ A)$
156	151 152 155	nfov	$⊢ \underline{Ⅎ} x ((Y - ⌊Y⌋) ⦋ Y / x ⦌ B + \sum_{k = M}^{⌊Y⌋} C - ⦋ Y / x ⦌ A)$
157		id	$⊢ x = Y \to x = Y$
158		fveq2	$⊢ x = Y \to ⌊x⌋ = ⌊Y⌋$
159	157 158	oveq12d	$⊢ x = Y \to x - ⌊x⌋ = Y - ⌊Y⌋$
160	159 61	oveq12d	$⊢ x = Y \to (x - ⌊x⌋) B = (Y - ⌊Y⌋) ⦋ Y / x ⦌ B$
161	158	oveq2d	$⊢ x = Y \to (M \dots ⌊x⌋) = (M \dots ⌊Y⌋)$
162	161	sumeq1d	$⊢ x = Y \to \sum_{k = M}^{⌊x⌋} C = \sum_{k = M}^{⌊Y⌋} C$
163	162 127	oveq12d	$⊢ x = Y \to \sum_{k = M}^{⌊x⌋} C - A = \sum_{k = M}^{⌊Y⌋} C - ⦋ Y / x ⦌ A$
164	160 163	oveq12d	$⊢ x = Y \to (x - ⌊x⌋) B + \sum_{k = M}^{⌊x⌋} C - A = (Y - ⌊Y⌋) ⦋ Y / x ⦌ B + \sum_{k = M}^{⌊Y⌋} C - ⦋ Y / x ⦌ A$
165	148 156 164 14	fvmptf	$⊢ (Y \in S \land (Y - ⌊Y⌋) ⦋ Y / x ⦌ B + \sum_{k = M}^{⌊Y⌋} C - ⦋ Y / x ⦌ A \in V) \to H (Y) = (Y - ⌊Y⌋) ⦋ Y / x ⦌ B + \sum_{k = M}^{⌊Y⌋} C - ⦋ Y / x ⦌ A$
166	16 147 165	sylancl	$⊢ φ \to H (Y) = (Y - ⌊Y⌋) ⦋ Y / x ⦌ B + \sum_{k = M}^{⌊Y⌋} C - ⦋ Y / x ⦌ A$
167	135 130 122	subadd23d	$⊢ φ \to (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A + \sum_{k = M}^{⌊X⌋} C = (Y - ⌊X⌋) ⦋ Y / x ⦌ B + \sum_{k = M}^{⌊X⌋} C - ⦋ Y / x ⦌ A$
168	146 166 167	3eqtr4d	$⊢ φ \to H (Y) = (Y - ⌊X⌋) ⦋ Y / x ⦌ B - ⦋ Y / x ⦌ A + \sum_{k = M}^{⌊X⌋} C$

Metamath Proof Explorer

Theorem dvfsumlem1

Proof