Metamath Proof Explorer


Theorem o1fsum

Description: If A ( k ) is O(1), then sum_ k <_ x , A ( k ) is O( x ). (Contributed by Mario Carneiro, 23-May-2016)

Ref Expression
Hypotheses o1fsum.1 φkAV
o1fsum.2 φkA𝑂1
Assertion o1fsum φx+k=1xAx𝑂1

Proof

Step Hyp Ref Expression
1 o1fsum.1 φkAV
2 o1fsum.2 φkA𝑂1
3 nnssre
4 3 a1i φ
5 1 2 o1mptrcl φkA
6 1red φ1
7 4 5 6 elo1mpt2 φkA𝑂1c1+∞mkckAm
8 2 7 mpbid φc1+∞mkckAm
9 rpssre +
10 9 a1i φc1+∞mkckAm+
11 nfcv _nA
12 nfcsb1v _kn/kA
13 csbeq1a k=nA=n/kA
14 11 12 13 cbvsumi k=1xA=n=1xn/kA
15 fzfid φc1+∞mkckAmx+1xFin
16 o1f kA𝑂1kA:domkA
17 2 16 syl φkA:domkA
18 1 ralrimiva φkAV
19 dmmptg kAVdomkA=
20 18 19 syl φdomkA=
21 20 feq2d φkA:domkAkA:
22 17 21 mpbid φkA:
23 eqid kA=kA
24 23 fmpt kAkA:
25 22 24 sylibr φkA
26 25 ad3antrrr φc1+∞mkckAmx+kA
27 elfznn n1xn
28 12 nfel1 kn/kA
29 13 eleq1d k=nAn/kA
30 28 29 rspc nkAn/kA
31 30 impcom kAnn/kA
32 26 27 31 syl2an φc1+∞mkckAmx+n1xn/kA
33 15 32 fsumcl φc1+∞mkckAmx+n=1xn/kA
34 14 33 eqeltrid φc1+∞mkckAmx+k=1xA
35 rpcn x+x
36 35 adantl φc1+∞mkckAmx+x
37 rpne0 x+x0
38 37 adantl φc1+∞mkckAmx+x0
39 34 36 38 divcld φc1+∞mkckAmx+k=1xAx
40 simplrl φc1+∞mkckAmc1+∞
41 1re 1
42 elicopnf 1c1+∞c1c
43 41 42 ax-mp c1+∞c1c
44 40 43 sylib φc1+∞mkckAmc1c
45 44 simpld φc1+∞mkckAmc
46 fzfid φc1+∞mkckAm1cFin
47 25 ad2antrr φc1+∞mkckAmkA
48 elfznn n1cn
49 47 48 31 syl2an φc1+∞mkckAmn1cn/kA
50 49 abscld φc1+∞mkckAmn1cn/kA
51 46 50 fsumrecl φc1+∞mkckAmn=1cn/kA
52 simplrr φc1+∞mkckAmm
53 51 52 readdcld φc1+∞mkckAmn=1cn/kA+m
54 34 36 38 absdivd φc1+∞mkckAmx+k=1xAx=k=1xAx
55 54 adantrr φc1+∞mkckAmx+cxk=1xAx=k=1xAx
56 rprege0 x+x0x
57 56 ad2antrl φc1+∞mkckAmx+cxx0x
58 absid x0xx=x
59 57 58 syl φc1+∞mkckAmx+cxx=x
60 59 oveq2d φc1+∞mkckAmx+cxk=1xAx=k=1xAx
61 55 60 eqtrd φc1+∞mkckAmx+cxk=1xAx=k=1xAx
62 34 adantrr φc1+∞mkckAmx+cxk=1xA
63 62 abscld φc1+∞mkckAmx+cxk=1xA
64 fzfid φc1+∞mkckAmx+cx1xFin
65 47 27 31 syl2an φc1+∞mkckAmn1xn/kA
66 65 adantlr φc1+∞mkckAmx+cxn1xn/kA
67 66 abscld φc1+∞mkckAmx+cxn1xn/kA
68 64 67 fsumrecl φc1+∞mkckAmx+cxn=1xn/kA
69 57 simpld φc1+∞mkckAmx+cxx
70 51 adantr φc1+∞mkckAmx+cxn=1cn/kA
71 52 adantr φc1+∞mkckAmx+cxm
72 70 71 readdcld φc1+∞mkckAmx+cxn=1cn/kA+m
73 69 72 remulcld φc1+∞mkckAmx+cxxn=1cn/kA+m
74 14 fveq2i k=1xA=n=1xn/kA
75 64 66 fsumabs φc1+∞mkckAmx+cxn=1xn/kAn=1xn/kA
76 74 75 eqbrtrid φc1+∞mkckAmx+cxk=1xAn=1xn/kA
77 fzfid φc1+∞mkckAmx+cxc+1xFin
78 ssun2 c+1x1cc+1x
79 flge1nn c1cc
80 44 79 syl φc1+∞mkckAmc
81 80 adantr φc1+∞mkckAmx+cxc
82 81 nnred φc1+∞mkckAmx+cxc
83 45 adantr φc1+∞mkckAmx+cxc
84 flle ccc
85 83 84 syl φc1+∞mkckAmx+cxcc
86 simprr φc1+∞mkckAmx+cxcx
87 82 83 69 85 86 letrd φc1+∞mkckAmx+cxcx
88 fznnfl xc1xccx
89 69 88 syl φc1+∞mkckAmx+cxc1xccx
90 81 87 89 mpbir2and φc1+∞mkckAmx+cxc1x
91 fzsplit c1x1x=1cc+1x
92 90 91 syl φc1+∞mkckAmx+cx1x=1cc+1x
93 78 92 sseqtrrid φc1+∞mkckAmx+cxc+1x1x
94 93 sselda φc1+∞mkckAmx+cxnc+1xn1x
95 65 abscld φc1+∞mkckAmn1xn/kA
96 95 adantlr φc1+∞mkckAmx+cxn1xn/kA
97 94 96 syldan φc1+∞mkckAmx+cxnc+1xn/kA
98 77 97 fsumrecl φc1+∞mkckAmx+cxn=c+1xn/kA
99 69 70 remulcld φc1+∞mkckAmx+cxxn=1cn/kA
100 69 71 remulcld φc1+∞mkckAmx+cxxm
101 70 recnd φc1+∞mkckAmx+cxn=1cn/kA
102 101 mulid2d φc1+∞mkckAmx+cx1n=1cn/kA=n=1cn/kA
103 1red φc1+∞mkckAmx+cx1
104 49 absge0d φc1+∞mkckAmn1c0n/kA
105 46 50 104 fsumge0 φc1+∞mkckAm0n=1cn/kA
106 51 105 jca φc1+∞mkckAmn=1cn/kA0n=1cn/kA
107 106 adantr φc1+∞mkckAmx+cxn=1cn/kA0n=1cn/kA
108 44 simprd φc1+∞mkckAm1c
109 108 adantr φc1+∞mkckAmx+cx1c
110 103 83 69 109 86 letrd φc1+∞mkckAmx+cx1x
111 lemul1a 1xn=1cn/kA0n=1cn/kA1x1n=1cn/kAxn=1cn/kA
112 103 69 107 110 111 syl31anc φc1+∞mkckAmx+cx1n=1cn/kAxn=1cn/kA
113 102 112 eqbrtrrd φc1+∞mkckAmx+cxn=1cn/kAxn=1cn/kA
114 hashcl c+1xFinc+1x0
115 nn0re c+1x0c+1x
116 77 114 115 3syl φc1+∞mkckAmx+cxc+1x
117 116 71 remulcld φc1+∞mkckAmx+cxc+1xm
118 71 adantr φc1+∞mkckAmx+cxnc+1xm
119 elfzuz nc+1xnc+1
120 81 peano2nnd φc1+∞mkckAmx+cxc+1
121 eluznn c+1nc+1n
122 120 121 sylan φc1+∞mkckAmx+cxnc+1n
123 simpllr φc1+∞mkckAmx+cxnc+1kckAm
124 83 adantr φc1+∞mkckAmx+cxnc+1c
125 reflcl cc
126 peano2re cc+1
127 124 125 126 3syl φc1+∞mkckAmx+cxnc+1c+1
128 122 nnred φc1+∞mkckAmx+cxnc+1n
129 fllep1 ccc+1
130 124 129 syl φc1+∞mkckAmx+cxnc+1cc+1
131 eluzle nc+1c+1n
132 131 adantl φc1+∞mkckAmx+cxnc+1c+1n
133 124 127 128 130 132 letrd φc1+∞mkckAmx+cxnc+1cn
134 nfv kcn
135 nfcv _kabs
136 135 12 nffv _kn/kA
137 nfcv _k
138 nfcv _km
139 136 137 138 nfbr kn/kAm
140 134 139 nfim kcnn/kAm
141 breq2 k=nckcn
142 13 fveq2d k=nA=n/kA
143 142 breq1d k=nAmn/kAm
144 141 143 imbi12d k=nckAmcnn/kAm
145 140 144 rspc nkckAmcnn/kAm
146 122 123 133 145 syl3c φc1+∞mkckAmx+cxnc+1n/kAm
147 119 146 sylan2 φc1+∞mkckAmx+cxnc+1xn/kAm
148 77 97 118 147 fsumle φc1+∞mkckAmx+cxn=c+1xn/kAn=c+1xm
149 71 recnd φc1+∞mkckAmx+cxm
150 fsumconst c+1xFinmn=c+1xm=c+1xm
151 77 149 150 syl2anc φc1+∞mkckAmx+cxn=c+1xm=c+1xm
152 148 151 breqtrd φc1+∞mkckAmx+cxn=c+1xn/kAc+1xm
153 biidd n=c+10m0m
154 0red φc1+∞mkckAmx+cxnc+10
155 47 30 mpan9 φc1+∞mkckAmnn/kA
156 155 adantlr φc1+∞mkckAmx+cxnn/kA
157 122 156 syldan φc1+∞mkckAmx+cxnc+1n/kA
158 157 abscld φc1+∞mkckAmx+cxnc+1n/kA
159 71 adantr φc1+∞mkckAmx+cxnc+1m
160 157 absge0d φc1+∞mkckAmx+cxnc+10n/kA
161 154 158 159 160 146 letrd φc1+∞mkckAmx+cxnc+10m
162 161 ralrimiva φc1+∞mkckAmx+cxnc+10m
163 120 nnzd φc1+∞mkckAmx+cxc+1
164 uzid c+1c+1c+1
165 163 164 syl φc1+∞mkckAmx+cxc+1c+1
166 153 162 165 rspcdva φc1+∞mkckAmx+cx0m
167 reflcl xx
168 69 167 syl φc1+∞mkckAmx+cxx
169 ssdomg 1xFinc+1x1xc+1x1x
170 64 93 169 sylc φc1+∞mkckAmx+cxc+1x1x
171 hashdomi c+1x1xc+1x1x
172 170 171 syl φc1+∞mkckAmx+cxc+1x1x
173 flge0nn0 x0xx0
174 hashfz1 x01x=x
175 57 173 174 3syl φc1+∞mkckAmx+cx1x=x
176 172 175 breqtrd φc1+∞mkckAmx+cxc+1xx
177 flle xxx
178 69 177 syl φc1+∞mkckAmx+cxxx
179 116 168 69 176 178 letrd φc1+∞mkckAmx+cxc+1xx
180 116 69 71 166 179 lemul1ad φc1+∞mkckAmx+cxc+1xmxm
181 98 117 100 152 180 letrd φc1+∞mkckAmx+cxn=c+1xn/kAxm
182 70 98 99 100 113 181 le2addd φc1+∞mkckAmx+cxn=1cn/kA+n=c+1xn/kAxn=1cn/kA+xm
183 ltp1 cc<c+1
184 fzdisj c<c+11cc+1x=
185 82 183 184 3syl φc1+∞mkckAmx+cx1cc+1x=
186 96 recnd φc1+∞mkckAmx+cxn1xn/kA
187 185 92 64 186 fsumsplit φc1+∞mkckAmx+cxn=1xn/kA=n=1cn/kA+n=c+1xn/kA
188 36 adantrr φc1+∞mkckAmx+cxx
189 188 101 149 adddid φc1+∞mkckAmx+cxxn=1cn/kA+m=xn=1cn/kA+xm
190 182 187 189 3brtr4d φc1+∞mkckAmx+cxn=1xn/kAxn=1cn/kA+m
191 63 68 73 76 190 letrd φc1+∞mkckAmx+cxk=1xAxn=1cn/kA+m
192 rpregt0 x+x0<x
193 192 ad2antrl φc1+∞mkckAmx+cxx0<x
194 ledivmul k=1xAn=1cn/kA+mx0<xk=1xAxn=1cn/kA+mk=1xAxn=1cn/kA+m
195 63 72 193 194 syl3anc φc1+∞mkckAmx+cxk=1xAxn=1cn/kA+mk=1xAxn=1cn/kA+m
196 191 195 mpbird φc1+∞mkckAmx+cxk=1xAxn=1cn/kA+m
197 61 196 eqbrtrd φc1+∞mkckAmx+cxk=1xAxn=1cn/kA+m
198 10 39 45 53 197 elo1d φc1+∞mkckAmx+k=1xAx𝑂1
199 198 ex φc1+∞mkckAmx+k=1xAx𝑂1
200 199 rexlimdvva φc1+∞mkckAmx+k=1xAx𝑂1
201 8 200 mpd φx+k=1xAx𝑂1