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 ( ( 𝜑𝑘 ∈ ℕ ) → 𝐴𝑉 )
o1fsum.2 ( 𝜑 → ( 𝑘 ∈ ℕ ↦ 𝐴 ) ∈ 𝑂(1) )
Assertion o1fsum ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 / 𝑥 ) ) ∈ 𝑂(1) )

Proof

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