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) )