MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  o1fsum Unicode version

Theorem o1fsum 13627
Description: If A( ) is O(1), then sum_ x,A( ) is O( ). (Contributed by Mario Carneiro, 23-May-2016.)
Hypotheses
Ref Expression
o1fsum.1
o1fsum.2
Assertion
Ref Expression
o1fsum
Distinct variable groups:   ,   , ,

Proof of Theorem o1fsum
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 o1fsum.2 . . 3
2 nnssre 10565 . . . . 5
32a1i 11 . . . 4
4 o1fsum.1 . . . . 5
54, 1o1mptrcl 13445 . . . 4
6 1red 9632 . . . 4
73, 5, 6elo1mpt2 13358 . . 3
81, 7mpbid 210 . 2
9 rpssre 11259 . . . . . 6
109a1i 11 . . . . 5
11 nfcv 2619 . . . . . . . 8
12 nfcsb1v 3450 . . . . . . . 8
13 csbeq1a 3443 . . . . . . . 8
1411, 12, 13cbvsumi 13519 . . . . . . 7
15 fzfid 12083 . . . . . . . 8
16 o1f 13352 . . . . . . . . . . . . 13
171, 16syl 16 . . . . . . . . . . . 12
184ralrimiva 2871 . . . . . . . . . . . . . 14
19 dmmptg 5509 . . . . . . . . . . . . . 14
2018, 19syl 16 . . . . . . . . . . . . 13
2120feq2d 5723 . . . . . . . . . . . 12
2217, 21mpbid 210 . . . . . . . . . . 11
23 eqid 2457 . . . . . . . . . . . 12
2423fmpt 6052 . . . . . . . . . . 11
2522, 24sylibr 212 . . . . . . . . . 10
2625ad3antrrr 729 . . . . . . . . 9
27 elfznn 11743 . . . . . . . . 9
2812nfel1 2635 . . . . . . . . . . 11
2913eleq1d 2526 . . . . . . . . . . 11
3028, 29rspc 3204 . . . . . . . . . 10
3130impcom 430 . . . . . . . . 9
3226, 27, 31syl2an 477 . . . . . . . 8
3315, 32fsumcl 13555 . . . . . . 7
3414, 33syl5eqel 2549 . . . . . 6
35 rpcn 11257 . . . . . . 7
3635adantl 466 . . . . . 6
37 rpne0 11264 . . . . . . 7
3837adantl 466 . . . . . 6
3934, 36, 38divcld 10345 . . . . 5
40 simplrl 761 . . . . . . 7
41 1re 9616 . . . . . . . 8
42 elicopnf 11649 . . . . . . . 8
4341, 42ax-mp 5 . . . . . . 7
4440, 43sylib 196 . . . . . 6
4544simpld 459 . . . . 5
46 fzfid 12083 . . . . . . 7
4725ad2antrr 725 . . . . . . . . 9
48 elfznn 11743 . . . . . . . . 9
4947, 48, 31syl2an 477 . . . . . . . 8
5049abscld 13267 . . . . . . 7
5146, 50fsumrecl 13556 . . . . . 6
52 simplrr 762 . . . . . 6
5351, 52readdcld 9644 . . . . 5
5434, 36, 38absdivd 13286 . . . . . . . 8
5554adantrr 716 . . . . . . 7
56 rprege0 11263 . . . . . . . . . 10
5756ad2antrl 727 . . . . . . . . 9
58 absid 13129 . . . . . . . . 9
5957, 58syl 16 . . . . . . . 8
6059oveq2d 6312 . . . . . . 7
6155, 60eqtrd 2498 . . . . . 6
6234adantrr 716 . . . . . . . . 9
6362abscld 13267 . . . . . . . 8
64 fzfid 12083 . . . . . . . . 9
6547, 27, 31syl2an 477 . . . . . . . . . . 11
6665adantlr 714 . . . . . . . . . 10
6766abscld 13267 . . . . . . . . 9
6864, 67fsumrecl 13556 . . . . . . . 8
6957simpld 459 . . . . . . . . 9
7051adantr 465 . . . . . . . . . 10
7152adantr 465 . . . . . . . . . 10
7270, 71readdcld 9644 . . . . . . . . 9
7369, 72remulcld 9645 . . . . . . . 8
7414fveq2i 5874 . . . . . . . . 9
7564, 66fsumabs 13615 . . . . . . . . 9
7674, 75syl5eqbr 4485 . . . . . . . 8
77 fzfid 12083 . . . . . . . . . . 11
78 ssun2 3667 . . . . . . . . . . . . . 14
79 flge1nn 11955 . . . . . . . . . . . . . . . . . 18
8044, 79syl 16 . . . . . . . . . . . . . . . . 17
8180adantr 465 . . . . . . . . . . . . . . . 16
8281nnred 10576 . . . . . . . . . . . . . . . . 17
8345adantr 465 . . . . . . . . . . . . . . . . 17
84 flle 11936 . . . . . . . . . . . . . . . . . 18
8583, 84syl 16 . . . . . . . . . . . . . . . . 17
86 simprr 757 . . . . . . . . . . . . . . . . 17
8782, 83, 69, 85, 86letrd 9760 . . . . . . . . . . . . . . . 16
88 fznnfl 11989 . . . . . . . . . . . . . . . . 17
8969, 88syl 16 . . . . . . . . . . . . . . . 16
9081, 87, 89mpbir2and 922 . . . . . . . . . . . . . . 15
91 fzsplit 11740 . . . . . . . . . . . . . . 15
9290, 91syl 16 . . . . . . . . . . . . . 14
9378, 92syl5sseqr 3552 . . . . . . . . . . . . 13
9493sselda 3503 . . . . . . . . . . . 12
9565abscld 13267 . . . . . . . . . . . . 13
9695adantlr 714 . . . . . . . . . . . 12
9794, 96syldan 470 . . . . . . . . . . 11
9877, 97fsumrecl 13556 . . . . . . . . . 10
9969, 70remulcld 9645 . . . . . . . . . 10
10069, 71remulcld 9645 . . . . . . . . . 10
10170recnd 9643 . . . . . . . . . . . 12
102101mulid2d 9635 . . . . . . . . . . 11
103 1red 9632 . . . . . . . . . . . 12
10449absge0d 13275 . . . . . . . . . . . . . . 15
10546, 50, 104fsumge0 13609 . . . . . . . . . . . . . 14
10651, 105jca 532 . . . . . . . . . . . . 13
107106adantr 465 . . . . . . . . . . . 12
10844simprd 463 . . . . . . . . . . . . . 14
109108adantr 465 . . . . . . . . . . . . 13
110103, 83, 69, 109, 86letrd 9760 . . . . . . . . . . . 12
111 lemul1a 10421 . . . . . . . . . . . 12
112103, 69, 107, 110, 111syl31anc 1231 . . . . . . . . . . 11
113102, 112eqbrtrrd 4474 . . . . . . . . . 10
114 hashcl 12428 . . . . . . . . . . . . 13
115 nn0re 10829 . . . . . . . . . . . . 13
11677, 114, 1153syl 20 . . . . . . . . . . . 12
117116, 71remulcld 9645 . . . . . . . . . . 11
11871adantr 465 . . . . . . . . . . . . 13
119 elfzuz 11713 . . . . . . . . . . . . . 14
12081peano2nnd 10578 . . . . . . . . . . . . . . . 16
121 eluznn 11181 . . . . . . . . . . . . . . . 16
122120, 121sylan 471 . . . . . . . . . . . . . . 15
123 simpllr 760 . . . . . . . . . . . . . . 15
12483adantr 465 . . . . . . . . . . . . . . . 16
125 reflcl 11933 . . . . . . . . . . . . . . . . 17
126 peano2re 9774 . . . . . . . . . . . . . . . . 17
127124, 125, 1263syl 20 . . . . . . . . . . . . . . . 16
128122nnred 10576 . . . . . . . . . . . . . . . 16
129 fllep1 11938 . . . . . . . . . . . . . . . . 17
130124, 129syl 16 . . . . . . . . . . . . . . . 16
131 eluzle 11122 . . . . . . . . . . . . . . . . 17
132131adantl 466 . . . . . . . . . . . . . . . 16
133124, 127, 128, 130, 132letrd 9760 . . . . . . . . . . . . . . 15
134 nfv 1707 . . . . . . . . . . . . . . . . 17
135 nfcv 2619 . . . . . . . . . . . . . . . . . . 19
136135, 12nffv 5878 . . . . . . . . . . . . . . . . . 18
137 nfcv 2619 . . . . . . . . . . . . . . . . . 18
138 nfcv 2619 . . . . . . . . . . . . . . . . . 18
139136, 137, 138nfbr 4496 . . . . . . . . . . . . . . . . 17
140134, 139nfim 1920 . . . . . . . . . . . . . . . 16
141 breq2 4456 . . . . . . . . . . . . . . . . 17
14213fveq2d 5875 . . . . . . . . . . . . . . . . . 18
143142breq1d 4462 . . . . . . . . . . . . . . . . 17
144141, 143imbi12d 320 . . . . . . . . . . . . . . . 16
145140, 144rspc 3204 . . . . . . . . . . . . . . 15
146122, 123, 133, 145syl3c 61 . . . . . . . . . . . . . 14
147119, 146sylan2 474 . . . . . . . . . . . . 13
14877, 97, 118, 147fsumle 13613 . . . . . . . . . . . 12
14971recnd 9643 . . . . . . . . . . . . 13
150 fsumconst 13605 . . . . . . . . . . . . 13
15177, 149, 150syl2anc 661 . . . . . . . . . . . 12
152148, 151breqtrd 4476 . . . . . . . . . . 11