# Metamath Proof Explorer

## Theorem dvfsumlem1

Description: Lemma for dvfsumrlim . (Contributed by Mario Carneiro, 17-May-2016)

Ref Expression
Hypotheses dvfsum.s ${⊢}{S}=\left({T},\mathrm{+\infty }\right)$
dvfsum.z ${⊢}{Z}={ℤ}_{\ge {M}}$
dvfsum.m ${⊢}{\phi }\to {M}\in ℤ$
dvfsum.d ${⊢}{\phi }\to {D}\in ℝ$
dvfsum.md ${⊢}{\phi }\to {M}\le {D}+1$
dvfsum.t ${⊢}{\phi }\to {T}\in ℝ$
dvfsum.a ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {A}\in ℝ$
dvfsum.b1 ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {B}\in {V}$
dvfsum.b2 ${⊢}\left({\phi }\wedge {x}\in {Z}\right)\to {B}\in ℝ$
dvfsum.b3 ${⊢}{\phi }\to \frac{d\left({x}\in {S}⟼{A}\right)}{{d}_{ℝ}{x}}=\left({x}\in {S}⟼{B}\right)$
dvfsum.c ${⊢}{x}={k}\to {B}={C}$
dvfsum.u ${⊢}{\phi }\to {U}\in {ℝ}^{*}$
dvfsum.l ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {k}\in {S}\right)\wedge \left({D}\le {x}\wedge {x}\le {k}\wedge {k}\le {U}\right)\right)\to {C}\le {B}$
dvfsum.h ${⊢}{H}=\left({x}\in {S}⟼\left({x}-⌊{x}⌋\right){B}+\sum _{{k}={M}}^{⌊{x}⌋}{C}-{A}\right)$
dvfsumlem1.1 ${⊢}{\phi }\to {X}\in {S}$
dvfsumlem1.2 ${⊢}{\phi }\to {Y}\in {S}$
dvfsumlem1.3 ${⊢}{\phi }\to {D}\le {X}$
dvfsumlem1.4 ${⊢}{\phi }\to {X}\le {Y}$
dvfsumlem1.5 ${⊢}{\phi }\to {Y}\le {U}$
dvfsumlem1.6 ${⊢}{\phi }\to {Y}\le ⌊{X}⌋+1$
Assertion dvfsumlem1

### Proof

Step Hyp Ref Expression
1 dvfsum.s ${⊢}{S}=\left({T},\mathrm{+\infty }\right)$
2 dvfsum.z ${⊢}{Z}={ℤ}_{\ge {M}}$
3 dvfsum.m ${⊢}{\phi }\to {M}\in ℤ$
4 dvfsum.d ${⊢}{\phi }\to {D}\in ℝ$
5 dvfsum.md ${⊢}{\phi }\to {M}\le {D}+1$
6 dvfsum.t ${⊢}{\phi }\to {T}\in ℝ$
7 dvfsum.a ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {A}\in ℝ$
8 dvfsum.b1 ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {B}\in {V}$
9 dvfsum.b2 ${⊢}\left({\phi }\wedge {x}\in {Z}\right)\to {B}\in ℝ$
10 dvfsum.b3 ${⊢}{\phi }\to \frac{d\left({x}\in {S}⟼{A}\right)}{{d}_{ℝ}{x}}=\left({x}\in {S}⟼{B}\right)$
11 dvfsum.c ${⊢}{x}={k}\to {B}={C}$
12 dvfsum.u ${⊢}{\phi }\to {U}\in {ℝ}^{*}$
13 dvfsum.l ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {k}\in {S}\right)\wedge \left({D}\le {x}\wedge {x}\le {k}\wedge {k}\le {U}\right)\right)\to {C}\le {B}$
14 dvfsum.h ${⊢}{H}=\left({x}\in {S}⟼\left({x}-⌊{x}⌋\right){B}+\sum _{{k}={M}}^{⌊{x}⌋}{C}-{A}\right)$
15 dvfsumlem1.1 ${⊢}{\phi }\to {X}\in {S}$
16 dvfsumlem1.2 ${⊢}{\phi }\to {Y}\in {S}$
17 dvfsumlem1.3 ${⊢}{\phi }\to {D}\le {X}$
18 dvfsumlem1.4 ${⊢}{\phi }\to {X}\le {Y}$
19 dvfsumlem1.5 ${⊢}{\phi }\to {Y}\le {U}$
20 dvfsumlem1.6 ${⊢}{\phi }\to {Y}\le ⌊{X}⌋+1$
21 ioossre ${⊢}\left({T},\mathrm{+\infty }\right)\subseteq ℝ$
22 1 21 eqsstri ${⊢}{S}\subseteq ℝ$
23 22 16 sseldi ${⊢}{\phi }\to {Y}\in ℝ$
24 22 15 sseldi ${⊢}{\phi }\to {X}\in ℝ$
25 24 flcld ${⊢}{\phi }\to ⌊{X}⌋\in ℤ$
26 reflcl ${⊢}{X}\in ℝ\to ⌊{X}⌋\in ℝ$
27 24 26 syl ${⊢}{\phi }\to ⌊{X}⌋\in ℝ$
28 flle ${⊢}{X}\in ℝ\to ⌊{X}⌋\le {X}$
29 24 28 syl ${⊢}{\phi }\to ⌊{X}⌋\le {X}$
30 27 24 23 29 18 letrd ${⊢}{\phi }\to ⌊{X}⌋\le {Y}$
31 flbi ${⊢}\left({Y}\in ℝ\wedge ⌊{X}⌋\in ℤ\right)\to \left(⌊{Y}⌋=⌊{X}⌋↔\left(⌊{X}⌋\le {Y}\wedge {Y}<⌊{X}⌋+1\right)\right)$
32 31 baibd ${⊢}\left(\left({Y}\in ℝ\wedge ⌊{X}⌋\in ℤ\right)\wedge ⌊{X}⌋\le {Y}\right)\to \left(⌊{Y}⌋=⌊{X}⌋↔{Y}<⌊{X}⌋+1\right)$
33 23 25 30 32 syl21anc ${⊢}{\phi }\to \left(⌊{Y}⌋=⌊{X}⌋↔{Y}<⌊{X}⌋+1\right)$
34 33 biimpar ${⊢}\left({\phi }\wedge {Y}<⌊{X}⌋+1\right)\to ⌊{Y}⌋=⌊{X}⌋$
35 34 oveq2d ${⊢}\left({\phi }\wedge {Y}<⌊{X}⌋+1\right)\to {Y}-⌊{Y}⌋={Y}-⌊{X}⌋$
36 35 oveq1d
37 34 oveq2d ${⊢}\left({\phi }\wedge {Y}<⌊{X}⌋+1\right)\to \left({M}\dots ⌊{Y}⌋\right)=\left({M}\dots ⌊{X}⌋\right)$
38 37 sumeq1d ${⊢}\left({\phi }\wedge {Y}<⌊{X}⌋+1\right)\to \sum _{{k}={M}}^{⌊{Y}⌋}{C}=\sum _{{k}={M}}^{⌊{X}⌋}{C}$
39 38 oveq1d
40 36 39 oveq12d
41 simpr ${⊢}\left({\phi }\wedge {Y}=⌊{X}⌋+1\right)\to {Y}=⌊{X}⌋+1$
42 24 adantr ${⊢}\left({\phi }\wedge {Y}=⌊{X}⌋+1\right)\to {X}\in ℝ$
43 42 flcld ${⊢}\left({\phi }\wedge {Y}=⌊{X}⌋+1\right)\to ⌊{X}⌋\in ℤ$
44 43 peano2zd ${⊢}\left({\phi }\wedge {Y}=⌊{X}⌋+1\right)\to ⌊{X}⌋+1\in ℤ$
45 41 44 eqeltrd ${⊢}\left({\phi }\wedge {Y}=⌊{X}⌋+1\right)\to {Y}\in ℤ$
46 flid ${⊢}{Y}\in ℤ\to ⌊{Y}⌋={Y}$
47 45 46 syl ${⊢}\left({\phi }\wedge {Y}=⌊{X}⌋+1\right)\to ⌊{Y}⌋={Y}$
48 47 41 eqtrd ${⊢}\left({\phi }\wedge {Y}=⌊{X}⌋+1\right)\to ⌊{Y}⌋=⌊{X}⌋+1$
49 48 oveq2d ${⊢}\left({\phi }\wedge {Y}=⌊{X}⌋+1\right)\to {Y}-⌊{Y}⌋={Y}-\left(⌊{X}⌋+1\right)$
50 49 oveq1d
51 23 recnd ${⊢}{\phi }\to {Y}\in ℂ$
52 27 recnd ${⊢}{\phi }\to ⌊{X}⌋\in ℂ$
53 51 52 subcld ${⊢}{\phi }\to {Y}-⌊{X}⌋\in ℂ$
54 1cnd ${⊢}{\phi }\to 1\in ℂ$
55 22 a1i ${⊢}{\phi }\to {S}\subseteq ℝ$
56 55 7 8 10 dvmptrecl ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {B}\in ℝ$
57 56 recnd ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {B}\in ℂ$
58 57 ralrimiva ${⊢}{\phi }\to \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{B}\in ℂ$
59 nfcsb1v
60 59 nfel1
61 csbeq1a
62 61 eleq1d
63 60 62 rspc
64 16 58 63 sylc
65 53 54 64 subdird
66 51 52 54 subsub4d ${⊢}{\phi }\to {Y}-⌊{X}⌋-1={Y}-\left(⌊{X}⌋+1\right)$
67 66 oveq1d
68 64 mulid2d
69 68 oveq2d
70 65 67 69 3eqtr3d
72 50 71 eqtrd
73 25 peano2zd ${⊢}{\phi }\to ⌊{X}⌋+1\in ℤ$
74 3 zred ${⊢}{\phi }\to {M}\in ℝ$
75 peano2rem ${⊢}{M}\in ℝ\to {M}-1\in ℝ$
76 74 75 syl ${⊢}{\phi }\to {M}-1\in ℝ$
77 1red ${⊢}{\phi }\to 1\in ℝ$
78 74 77 4 lesubaddd ${⊢}{\phi }\to \left({M}-1\le {D}↔{M}\le {D}+1\right)$
79 5 78 mpbird ${⊢}{\phi }\to {M}-1\le {D}$
80 76 4 24 79 17 letrd ${⊢}{\phi }\to {M}-1\le {X}$
81 peano2zm ${⊢}{M}\in ℤ\to {M}-1\in ℤ$
82 3 81 syl ${⊢}{\phi }\to {M}-1\in ℤ$
83 flge ${⊢}\left({X}\in ℝ\wedge {M}-1\in ℤ\right)\to \left({M}-1\le {X}↔{M}-1\le ⌊{X}⌋\right)$
84 24 82 83 syl2anc ${⊢}{\phi }\to \left({M}-1\le {X}↔{M}-1\le ⌊{X}⌋\right)$
85 80 84 mpbid ${⊢}{\phi }\to {M}-1\le ⌊{X}⌋$
86 74 77 27 lesubaddd ${⊢}{\phi }\to \left({M}-1\le ⌊{X}⌋↔{M}\le ⌊{X}⌋+1\right)$
87 85 86 mpbid ${⊢}{\phi }\to {M}\le ⌊{X}⌋+1$
88 eluz2 ${⊢}⌊{X}⌋+1\in {ℤ}_{\ge {M}}↔\left({M}\in ℤ\wedge ⌊{X}⌋+1\in ℤ\wedge {M}\le ⌊{X}⌋+1\right)$
89 3 73 87 88 syl3anbrc ${⊢}{\phi }\to ⌊{X}⌋+1\in {ℤ}_{\ge {M}}$
90 9 recnd ${⊢}\left({\phi }\wedge {x}\in {Z}\right)\to {B}\in ℂ$
91 90 ralrimiva ${⊢}{\phi }\to \forall {x}\in {Z}\phantom{\rule{.4em}{0ex}}{B}\in ℂ$
92 elfzuz ${⊢}{k}\in \left({M}\dots ⌊{X}⌋+1\right)\to {k}\in {ℤ}_{\ge {M}}$
93 92 2 eleqtrrdi ${⊢}{k}\in \left({M}\dots ⌊{X}⌋+1\right)\to {k}\in {Z}$
94 11 eleq1d ${⊢}{x}={k}\to \left({B}\in ℂ↔{C}\in ℂ\right)$
95 94 rspccva ${⊢}\left(\forall {x}\in {Z}\phantom{\rule{.4em}{0ex}}{B}\in ℂ\wedge {k}\in {Z}\right)\to {C}\in ℂ$
96 91 93 95 syl2an ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots ⌊{X}⌋+1\right)\right)\to {C}\in ℂ$
97 eqvisset ${⊢}{k}=⌊{X}⌋+1\to ⌊{X}⌋+1\in \mathrm{V}$
98 eqeq2 ${⊢}{k}=⌊{X}⌋+1\to \left({x}={k}↔{x}=⌊{X}⌋+1\right)$
99 98 biimpar ${⊢}\left({k}=⌊{X}⌋+1\wedge {x}=⌊{X}⌋+1\right)\to {x}={k}$
100 99 11 syl ${⊢}\left({k}=⌊{X}⌋+1\wedge {x}=⌊{X}⌋+1\right)\to {B}={C}$
101 97 100 csbied
102 101 eqcomd
103 89 96 102 fsumm1
104 ax-1cn ${⊢}1\in ℂ$
105 pncan ${⊢}\left(⌊{X}⌋\in ℂ\wedge 1\in ℂ\right)\to ⌊{X}⌋+1-1=⌊{X}⌋$
106 52 104 105 sylancl ${⊢}{\phi }\to ⌊{X}⌋+1-1=⌊{X}⌋$
107 106 oveq2d ${⊢}{\phi }\to \left({M}\dots ⌊{X}⌋+1-1\right)=\left({M}\dots ⌊{X}⌋\right)$
108 107 sumeq1d ${⊢}{\phi }\to \sum _{{k}={M}}^{⌊{X}⌋+1-1}{C}=\sum _{{k}={M}}^{⌊{X}⌋}{C}$
109 108 oveq1d
110 103 109 eqtrd
112 48 oveq2d ${⊢}\left({\phi }\wedge {Y}=⌊{X}⌋+1\right)\to \left({M}\dots ⌊{Y}⌋\right)=\left({M}\dots ⌊{X}⌋+1\right)$
113 112 sumeq1d ${⊢}\left({\phi }\wedge {Y}=⌊{X}⌋+1\right)\to \sum _{{k}={M}}^{⌊{Y}⌋}{C}=\sum _{{k}={M}}^{⌊{X}⌋+1}{C}$
114 41 csbeq1d
115 114 oveq2d
116 111 113 115 3eqtr4d
117 116 oveq1d
118 fzfid ${⊢}{\phi }\to \left({M}\dots ⌊{X}⌋\right)\in \mathrm{Fin}$
119 elfzuz ${⊢}{k}\in \left({M}\dots ⌊{X}⌋\right)\to {k}\in {ℤ}_{\ge {M}}$
120 119 2 eleqtrrdi ${⊢}{k}\in \left({M}\dots ⌊{X}⌋\right)\to {k}\in {Z}$
121 91 120 95 syl2an ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots ⌊{X}⌋\right)\right)\to {C}\in ℂ$
122 118 121 fsumcl ${⊢}{\phi }\to \sum _{{k}={M}}^{⌊{X}⌋}{C}\in ℂ$
123 7 recnd ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {A}\in ℂ$
124 123 ralrimiva ${⊢}{\phi }\to \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{A}\in ℂ$
125 nfcsb1v
126 125 nfel1
127 csbeq1a
128 127 eleq1d
129 126 128 rspc
130 16 124 129 sylc
133 117 132 eqtrd
134 72 133 oveq12d
135 53 64 mulcld
138 122 130 subcld
140 136 137 139 nppcan3d
141 134 140 eqtrd
142 peano2re ${⊢}⌊{X}⌋\in ℝ\to ⌊{X}⌋+1\in ℝ$
143 27 142 syl ${⊢}{\phi }\to ⌊{X}⌋+1\in ℝ$
144 23 143 leloed ${⊢}{\phi }\to \left({Y}\le ⌊{X}⌋+1↔\left({Y}<⌊{X}⌋+1\vee {Y}=⌊{X}⌋+1\right)\right)$
145 20 144 mpbid ${⊢}{\phi }\to \left({Y}<⌊{X}⌋+1\vee {Y}=⌊{X}⌋+1\right)$
146 40 141 145 mpjaodan
147 ovex
148 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{Y}$
149 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({Y}-⌊{Y}⌋\right)$
150 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}×$
151 149 150 59 nfov
152 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}+$
153 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\sum _{{k}={M}}^{⌊{Y}⌋}{C}$
154 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}-$
155 153 154 125 nfov
156 151 152 155 nfov
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
161 158 oveq2d ${⊢}{x}={Y}\to \left({M}\dots ⌊{x}⌋\right)=\left({M}\dots ⌊{Y}⌋\right)$
162 161 sumeq1d ${⊢}{x}={Y}\to \sum _{{k}={M}}^{⌊{x}⌋}{C}=\sum _{{k}={M}}^{⌊{Y}⌋}{C}$
163 162 127 oveq12d
164 160 163 oveq12d
165 148 156 164 14 fvmptf
166 16 147 165 sylancl