# 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 ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {A}\in {V}$
o1fsum.2 ${⊢}{\phi }\to \left({k}\in ℕ⟼{A}\right)\in 𝑂\left(1\right)$
Assertion o1fsum ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}⟼\frac{\sum _{{k}=1}^{⌊{x}⌋}{A}}{{x}}\right)\in 𝑂\left(1\right)$

### Proof

Step Hyp Ref Expression
1 o1fsum.1 ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {A}\in {V}$
2 o1fsum.2 ${⊢}{\phi }\to \left({k}\in ℕ⟼{A}\right)\in 𝑂\left(1\right)$
3 nnssre ${⊢}ℕ\subseteq ℝ$
4 3 a1i ${⊢}{\phi }\to ℕ\subseteq ℝ$
5 1 2 o1mptrcl ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {A}\in ℂ$
6 1red ${⊢}{\phi }\to 1\in ℝ$
7 4 5 6 elo1mpt2 ${⊢}{\phi }\to \left(\left({k}\in ℕ⟼{A}\right)\in 𝑂\left(1\right)↔\exists {c}\in \left[1,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)$
8 2 7 mpbid ${⊢}{\phi }\to \exists {c}\in \left[1,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)$
9 rpssre ${⊢}{ℝ}^{+}\subseteq ℝ$
10 9 a1i ${⊢}\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\to {ℝ}^{+}\subseteq ℝ$
11 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{A}$
12 nfcsb1v
13 csbeq1a
14 11 12 13 cbvsumi
15 fzfid ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge {x}\in {ℝ}^{+}\right)\to \left(1\dots ⌊{x}⌋\right)\in \mathrm{Fin}$
16 o1f ${⊢}\left({k}\in ℕ⟼{A}\right)\in 𝑂\left(1\right)\to \left({k}\in ℕ⟼{A}\right):\mathrm{dom}\left({k}\in ℕ⟼{A}\right)⟶ℂ$
17 2 16 syl ${⊢}{\phi }\to \left({k}\in ℕ⟼{A}\right):\mathrm{dom}\left({k}\in ℕ⟼{A}\right)⟶ℂ$
18 1 ralrimiva ${⊢}{\phi }\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {V}$
19 dmmptg ${⊢}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {V}\to \mathrm{dom}\left({k}\in ℕ⟼{A}\right)=ℕ$
20 18 19 syl ${⊢}{\phi }\to \mathrm{dom}\left({k}\in ℕ⟼{A}\right)=ℕ$
21 20 feq2d ${⊢}{\phi }\to \left(\left({k}\in ℕ⟼{A}\right):\mathrm{dom}\left({k}\in ℕ⟼{A}\right)⟶ℂ↔\left({k}\in ℕ⟼{A}\right):ℕ⟶ℂ\right)$
22 17 21 mpbid ${⊢}{\phi }\to \left({k}\in ℕ⟼{A}\right):ℕ⟶ℂ$
23 eqid ${⊢}\left({k}\in ℕ⟼{A}\right)=\left({k}\in ℕ⟼{A}\right)$
24 23 fmpt ${⊢}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in ℂ↔\left({k}\in ℕ⟼{A}\right):ℕ⟶ℂ$
25 22 24 sylibr ${⊢}{\phi }\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in ℂ$
26 25 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge {x}\in {ℝ}^{+}\right)\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in ℂ$
27 elfznn ${⊢}{n}\in \left(1\dots ⌊{x}⌋\right)\to {n}\in ℕ$
28 12 nfel1
29 13 eleq1d
30 28 29 rspc
31 30 impcom
32 26 27 31 syl2an
33 15 32 fsumcl
34 14 33 eqeltrid ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge {x}\in {ℝ}^{+}\right)\to \sum _{{k}=1}^{⌊{x}⌋}{A}\in ℂ$
35 rpcn ${⊢}{x}\in {ℝ}^{+}\to {x}\in ℂ$
36 35 adantl ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge {x}\in {ℝ}^{+}\right)\to {x}\in ℂ$
37 rpne0 ${⊢}{x}\in {ℝ}^{+}\to {x}\ne 0$
38 37 adantl ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge {x}\in {ℝ}^{+}\right)\to {x}\ne 0$
39 34 36 38 divcld ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge {x}\in {ℝ}^{+}\right)\to \frac{\sum _{{k}=1}^{⌊{x}⌋}{A}}{{x}}\in ℂ$
40 simplrl ${⊢}\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\to {c}\in \left[1,\mathrm{+\infty }\right)$
41 1re ${⊢}1\in ℝ$
42 elicopnf ${⊢}1\in ℝ\to \left({c}\in \left[1,\mathrm{+\infty }\right)↔\left({c}\in ℝ\wedge 1\le {c}\right)\right)$
43 41 42 ax-mp ${⊢}{c}\in \left[1,\mathrm{+\infty }\right)↔\left({c}\in ℝ\wedge 1\le {c}\right)$
44 40 43 sylib ${⊢}\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\to \left({c}\in ℝ\wedge 1\le {c}\right)$
45 44 simpld ${⊢}\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\to {c}\in ℝ$
46 fzfid ${⊢}\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\to \left(1\dots ⌊{c}⌋\right)\in \mathrm{Fin}$
47 25 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in ℂ$
48 elfznn ${⊢}{n}\in \left(1\dots ⌊{c}⌋\right)\to {n}\in ℕ$
49 47 48 31 syl2an
50 49 abscld
51 46 50 fsumrecl
52 simplrr ${⊢}\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\to {m}\in ℝ$
54 34 36 38 absdivd ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge {x}\in {ℝ}^{+}\right)\to \left|\frac{\sum _{{k}=1}^{⌊{x}⌋}{A}}{{x}}\right|=\frac{\left|\sum _{{k}=1}^{⌊{x}⌋}{A}\right|}{\left|{x}\right|}$
55 54 adantrr ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left|\frac{\sum _{{k}=1}^{⌊{x}⌋}{A}}{{x}}\right|=\frac{\left|\sum _{{k}=1}^{⌊{x}⌋}{A}\right|}{\left|{x}\right|}$
56 rprege0 ${⊢}{x}\in {ℝ}^{+}\to \left({x}\in ℝ\wedge 0\le {x}\right)$
57 56 ad2antrl ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left({x}\in ℝ\wedge 0\le {x}\right)$
58 absid ${⊢}\left({x}\in ℝ\wedge 0\le {x}\right)\to \left|{x}\right|={x}$
59 57 58 syl ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left|{x}\right|={x}$
60 59 oveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \frac{\left|\sum _{{k}=1}^{⌊{x}⌋}{A}\right|}{\left|{x}\right|}=\frac{\left|\sum _{{k}=1}^{⌊{x}⌋}{A}\right|}{{x}}$
61 55 60 eqtrd ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left|\frac{\sum _{{k}=1}^{⌊{x}⌋}{A}}{{x}}\right|=\frac{\left|\sum _{{k}=1}^{⌊{x}⌋}{A}\right|}{{x}}$
62 34 adantrr ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \sum _{{k}=1}^{⌊{x}⌋}{A}\in ℂ$
63 62 abscld ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left|\sum _{{k}=1}^{⌊{x}⌋}{A}\right|\in ℝ$
64 fzfid ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left(1\dots ⌊{x}⌋\right)\in \mathrm{Fin}$
65 47 27 31 syl2an
67 66 abscld
68 64 67 fsumrecl
69 57 simpld ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to {x}\in ℝ$
71 52 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to {m}\in ℝ$
73 69 72 remulcld
74 14 fveq2i
75 64 66 fsumabs
76 74 75 eqbrtrid
77 fzfid ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\in \mathrm{Fin}$
78 ssun2 ${⊢}\left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\subseteq \left(1\dots ⌊{c}⌋\right)\cup \left(⌊{c}⌋+1\dots ⌊{x}⌋\right)$
79 flge1nn ${⊢}\left({c}\in ℝ\wedge 1\le {c}\right)\to ⌊{c}⌋\in ℕ$
80 44 79 syl ${⊢}\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\to ⌊{c}⌋\in ℕ$
81 80 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to ⌊{c}⌋\in ℕ$
82 81 nnred ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to ⌊{c}⌋\in ℝ$
83 45 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to {c}\in ℝ$
84 flle ${⊢}{c}\in ℝ\to ⌊{c}⌋\le {c}$
85 83 84 syl ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to ⌊{c}⌋\le {c}$
86 simprr ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to {c}\le {x}$
87 82 83 69 85 86 letrd ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to ⌊{c}⌋\le {x}$
88 fznnfl ${⊢}{x}\in ℝ\to \left(⌊{c}⌋\in \left(1\dots ⌊{x}⌋\right)↔\left(⌊{c}⌋\in ℕ\wedge ⌊{c}⌋\le {x}\right)\right)$
89 69 88 syl ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left(⌊{c}⌋\in \left(1\dots ⌊{x}⌋\right)↔\left(⌊{c}⌋\in ℕ\wedge ⌊{c}⌋\le {x}\right)\right)$
90 81 87 89 mpbir2and ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to ⌊{c}⌋\in \left(1\dots ⌊{x}⌋\right)$
91 fzsplit ${⊢}⌊{c}⌋\in \left(1\dots ⌊{x}⌋\right)\to \left(1\dots ⌊{x}⌋\right)=\left(1\dots ⌊{c}⌋\right)\cup \left(⌊{c}⌋+1\dots ⌊{x}⌋\right)$
92 90 91 syl ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left(1\dots ⌊{x}⌋\right)=\left(1\dots ⌊{c}⌋\right)\cup \left(⌊{c}⌋+1\dots ⌊{x}⌋\right)$
93 78 92 sseqtrrid ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\subseteq \left(1\dots ⌊{x}⌋\right)$
94 93 sselda ${⊢}\left(\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\wedge {n}\in \left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\right)\to {n}\in \left(1\dots ⌊{x}⌋\right)$
95 65 abscld
97 94 96 syldan
98 77 97 fsumrecl
99 69 70 remulcld
100 69 71 remulcld ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to {x}{m}\in ℝ$
101 70 recnd
102 101 mulid2d
103 1red ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to 1\in ℝ$
104 49 absge0d
105 46 50 104 fsumge0
106 51 105 jca
108 44 simprd ${⊢}\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\to 1\le {c}$
109 108 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to 1\le {c}$
110 103 83 69 109 86 letrd ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to 1\le {x}$
111 lemul1a
112 103 69 107 110 111 syl31anc
113 102 112 eqbrtrrd
114 hashcl ${⊢}\left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\in \mathrm{Fin}\to \left|\left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\right|\in {ℕ}_{0}$
115 nn0re ${⊢}\left|\left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\right|\in {ℕ}_{0}\to \left|\left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\right|\in ℝ$
116 77 114 115 3syl ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left|\left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\right|\in ℝ$
117 116 71 remulcld ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left|\left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\right|{m}\in ℝ$
118 71 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\wedge {n}\in \left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\right)\to {m}\in ℝ$
119 elfzuz ${⊢}{n}\in \left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\to {n}\in {ℤ}_{\ge \left(⌊{c}⌋+1\right)}$
120 81 peano2nnd ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to ⌊{c}⌋+1\in ℕ$
121 eluznn ${⊢}\left(⌊{c}⌋+1\in ℕ\wedge {n}\in {ℤ}_{\ge \left(⌊{c}⌋+1\right)}\right)\to {n}\in ℕ$
122 120 121 sylan ${⊢}\left(\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\wedge {n}\in {ℤ}_{\ge \left(⌊{c}⌋+1\right)}\right)\to {n}\in ℕ$
123 simpllr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\wedge {n}\in {ℤ}_{\ge \left(⌊{c}⌋+1\right)}\right)\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)$
124 83 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\wedge {n}\in {ℤ}_{\ge \left(⌊{c}⌋+1\right)}\right)\to {c}\in ℝ$
125 reflcl ${⊢}{c}\in ℝ\to ⌊{c}⌋\in ℝ$
126 peano2re ${⊢}⌊{c}⌋\in ℝ\to ⌊{c}⌋+1\in ℝ$
127 124 125 126 3syl ${⊢}\left(\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\wedge {n}\in {ℤ}_{\ge \left(⌊{c}⌋+1\right)}\right)\to ⌊{c}⌋+1\in ℝ$
128 122 nnred ${⊢}\left(\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\wedge {n}\in {ℤ}_{\ge \left(⌊{c}⌋+1\right)}\right)\to {n}\in ℝ$
129 fllep1 ${⊢}{c}\in ℝ\to {c}\le ⌊{c}⌋+1$
130 124 129 syl ${⊢}\left(\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\wedge {n}\in {ℤ}_{\ge \left(⌊{c}⌋+1\right)}\right)\to {c}\le ⌊{c}⌋+1$
131 eluzle ${⊢}{n}\in {ℤ}_{\ge \left(⌊{c}⌋+1\right)}\to ⌊{c}⌋+1\le {n}$
132 131 adantl ${⊢}\left(\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\wedge {n}\in {ℤ}_{\ge \left(⌊{c}⌋+1\right)}\right)\to ⌊{c}⌋+1\le {n}$
133 124 127 128 130 132 letrd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\wedge {n}\in {ℤ}_{\ge \left(⌊{c}⌋+1\right)}\right)\to {c}\le {n}$
134 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{c}\le {n}$
135 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\mathrm{abs}$
136 135 12 nffv
137 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\le$
138 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{m}$
139 136 137 138 nfbr
140 134 139 nfim
141 breq2 ${⊢}{k}={n}\to \left({c}\le {k}↔{c}\le {n}\right)$
142 13 fveq2d
143 142 breq1d
144 141 143 imbi12d
145 140 144 rspc
146 122 123 133 145 syl3c
147 119 146 sylan2
148 77 97 118 147 fsumle
149 71 recnd ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to {m}\in ℂ$
150 fsumconst ${⊢}\left(\left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\in \mathrm{Fin}\wedge {m}\in ℂ\right)\to \sum _{{n}=⌊{c}⌋+1}^{⌊{x}⌋}{m}=\left|\left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\right|{m}$
151 77 149 150 syl2anc ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \sum _{{n}=⌊{c}⌋+1}^{⌊{x}⌋}{m}=\left|\left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\right|{m}$
152 148 151 breqtrd
153 biidd ${⊢}{n}=⌊{c}⌋+1\to \left(0\le {m}↔0\le {m}\right)$
154 0red ${⊢}\left(\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\wedge {n}\in {ℤ}_{\ge \left(⌊{c}⌋+1\right)}\right)\to 0\in ℝ$
155 47 30 mpan9
157 122 156 syldan
158 157 abscld
159 71 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\wedge {n}\in {ℤ}_{\ge \left(⌊{c}⌋+1\right)}\right)\to {m}\in ℝ$
160 157 absge0d
161 154 158 159 160 146 letrd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\wedge {n}\in {ℤ}_{\ge \left(⌊{c}⌋+1\right)}\right)\to 0\le {m}$
162 161 ralrimiva ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \forall {n}\in {ℤ}_{\ge \left(⌊{c}⌋+1\right)}\phantom{\rule{.4em}{0ex}}0\le {m}$
163 120 nnzd ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to ⌊{c}⌋+1\in ℤ$
164 uzid ${⊢}⌊{c}⌋+1\in ℤ\to ⌊{c}⌋+1\in {ℤ}_{\ge \left(⌊{c}⌋+1\right)}$
165 163 164 syl ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to ⌊{c}⌋+1\in {ℤ}_{\ge \left(⌊{c}⌋+1\right)}$
166 153 162 165 rspcdva ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to 0\le {m}$
167 reflcl ${⊢}{x}\in ℝ\to ⌊{x}⌋\in ℝ$
168 69 167 syl ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to ⌊{x}⌋\in ℝ$
169 ssdomg ${⊢}\left(1\dots ⌊{x}⌋\right)\in \mathrm{Fin}\to \left(\left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\subseteq \left(1\dots ⌊{x}⌋\right)\to \left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\preccurlyeq \left(1\dots ⌊{x}⌋\right)\right)$
170 64 93 169 sylc ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\preccurlyeq \left(1\dots ⌊{x}⌋\right)$
171 hashdomi ${⊢}\left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\preccurlyeq \left(1\dots ⌊{x}⌋\right)\to \left|\left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\right|\le \left|\left(1\dots ⌊{x}⌋\right)\right|$
172 170 171 syl ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left|\left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\right|\le \left|\left(1\dots ⌊{x}⌋\right)\right|$
173 flge0nn0 ${⊢}\left({x}\in ℝ\wedge 0\le {x}\right)\to ⌊{x}⌋\in {ℕ}_{0}$
174 hashfz1 ${⊢}⌊{x}⌋\in {ℕ}_{0}\to \left|\left(1\dots ⌊{x}⌋\right)\right|=⌊{x}⌋$
175 57 173 174 3syl ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left|\left(1\dots ⌊{x}⌋\right)\right|=⌊{x}⌋$
176 172 175 breqtrd ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left|\left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\right|\le ⌊{x}⌋$
177 flle ${⊢}{x}\in ℝ\to ⌊{x}⌋\le {x}$
178 69 177 syl ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to ⌊{x}⌋\le {x}$
179 116 168 69 176 178 letrd ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left|\left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\right|\le {x}$
180 116 69 71 166 179 lemul1ad ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left|\left(⌊{c}⌋+1\dots ⌊{x}⌋\right)\right|{m}\le {x}{m}$
181 98 117 100 152 180 letrd
182 70 98 99 100 113 181 le2addd
183 ltp1 ${⊢}⌊{c}⌋\in ℝ\to ⌊{c}⌋<⌊{c}⌋+1$
184 fzdisj ${⊢}⌊{c}⌋<⌊{c}⌋+1\to \left(1\dots ⌊{c}⌋\right)\cap \left(⌊{c}⌋+1\dots ⌊{x}⌋\right)=\varnothing$
185 82 183 184 3syl ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left(1\dots ⌊{c}⌋\right)\cap \left(⌊{c}⌋+1\dots ⌊{x}⌋\right)=\varnothing$
186 96 recnd
187 185 92 64 186 fsumsplit
188 36 adantrr ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to {x}\in ℂ$
192 rpregt0 ${⊢}{x}\in {ℝ}^{+}\to \left({x}\in ℝ\wedge 0<{x}\right)$
193 192 ad2antrl ${⊢}\left(\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\wedge \left({x}\in {ℝ}^{+}\wedge {c}\le {x}\right)\right)\to \left({x}\in ℝ\wedge 0<{x}\right)$
198 10 39 45 53 197 elo1d ${⊢}\left(\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\right)\to \left({x}\in {ℝ}^{+}⟼\frac{\sum _{{k}=1}^{⌊{x}⌋}{A}}{{x}}\right)\in 𝑂\left(1\right)$
199 198 ex ${⊢}\left({\phi }\wedge \left({c}\in \left[1,\mathrm{+\infty }\right)\wedge {m}\in ℝ\right)\right)\to \left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\to \left({x}\in {ℝ}^{+}⟼\frac{\sum _{{k}=1}^{⌊{x}⌋}{A}}{{x}}\right)\in 𝑂\left(1\right)\right)$
200 199 rexlimdvva ${⊢}{\phi }\to \left(\exists {c}\in \left[1,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({c}\le {k}\to \left|{A}\right|\le {m}\right)\to \left({x}\in {ℝ}^{+}⟼\frac{\sum _{{k}=1}^{⌊{x}⌋}{A}}{{x}}\right)\in 𝑂\left(1\right)\right)$
201 8 200 mpd ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}⟼\frac{\sum _{{k}=1}^{⌊{x}⌋}{A}}{{x}}\right)\in 𝑂\left(1\right)$