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

Theorem o1fsum 15849
Description: If 𝐴(𝑘) is O(1), then Σ𝑘𝑥, 𝐴(𝑘) is O(𝑥). (Contributed by Mario Carneiro, 23-May-2016.)
Hypotheses
Ref Expression
o1fsum.1 ((𝜑𝑘 ∈ ℕ) → 𝐴𝑉)
o1fsum.2 (𝜑 → (𝑘 ∈ ℕ ↦ 𝐴) ∈ 𝑂(1))
Assertion
Ref Expression
o1fsum (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) ∈ 𝑂(1))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑘,𝜑
Allowed substitution hints:   𝐴(𝑘)   𝑉(𝑥,𝑘)

Proof of Theorem o1fsum
Dummy variables 𝑚 𝑐 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 o1fsum.2 . . 3 (𝜑 → (𝑘 ∈ ℕ ↦ 𝐴) ∈ 𝑂(1))
2 nnssre 12270 . . . . 5 ℕ ⊆ ℝ
32a1i 11 . . . 4 (𝜑 → ℕ ⊆ ℝ)
4 o1fsum.1 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝐴𝑉)
54, 1o1mptrcl 15659 . . . 4 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ ℂ)
6 1red 11262 . . . 4 (𝜑 → 1 ∈ ℝ)
73, 5, 6elo1mpt2 15571 . . 3 (𝜑 → ((𝑘 ∈ ℕ ↦ 𝐴) ∈ 𝑂(1) ↔ ∃𝑐 ∈ (1[,)+∞)∃𝑚 ∈ ℝ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)))
81, 7mpbid 232 . 2 (𝜑 → ∃𝑐 ∈ (1[,)+∞)∃𝑚 ∈ ℝ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚))
9 rpssre 13042 . . . . . 6 + ⊆ ℝ
109a1i 11 . . . . 5 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → ℝ+ ⊆ ℝ)
11 csbeq1a 3913 . . . . . . . 8 (𝑘 = 𝑛𝐴 = 𝑛 / 𝑘𝐴)
12 nfcv 2905 . . . . . . . 8 𝑛𝐴
13 nfcsb1v 3923 . . . . . . . 8 𝑘𝑛 / 𝑘𝐴
1411, 12, 13cbvsum 15731 . . . . . . 7 Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 = Σ𝑛 ∈ (1...(⌊‘𝑥))𝑛 / 𝑘𝐴
15 fzfid 14014 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
16 o1f 15565 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ↦ 𝐴) ∈ 𝑂(1) → (𝑘 ∈ ℕ ↦ 𝐴):dom (𝑘 ∈ ℕ ↦ 𝐴)⟶ℂ)
171, 16syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ ℕ ↦ 𝐴):dom (𝑘 ∈ ℕ ↦ 𝐴)⟶ℂ)
184ralrimiva 3146 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑘 ∈ ℕ 𝐴𝑉)
19 dmmptg 6262 . . . . . . . . . . . . . 14 (∀𝑘 ∈ ℕ 𝐴𝑉 → dom (𝑘 ∈ ℕ ↦ 𝐴) = ℕ)
2018, 19syl 17 . . . . . . . . . . . . 13 (𝜑 → dom (𝑘 ∈ ℕ ↦ 𝐴) = ℕ)
2120feq2d 6722 . . . . . . . . . . . 12 (𝜑 → ((𝑘 ∈ ℕ ↦ 𝐴):dom (𝑘 ∈ ℕ ↦ 𝐴)⟶ℂ ↔ (𝑘 ∈ ℕ ↦ 𝐴):ℕ⟶ℂ))
2217, 21mpbid 232 . . . . . . . . . . 11 (𝜑 → (𝑘 ∈ ℕ ↦ 𝐴):ℕ⟶ℂ)
23 eqid 2737 . . . . . . . . . . . 12 (𝑘 ∈ ℕ ↦ 𝐴) = (𝑘 ∈ ℕ ↦ 𝐴)
2423fmpt 7130 . . . . . . . . . . 11 (∀𝑘 ∈ ℕ 𝐴 ∈ ℂ ↔ (𝑘 ∈ ℕ ↦ 𝐴):ℕ⟶ℂ)
2522, 24sylibr 234 . . . . . . . . . 10 (𝜑 → ∀𝑘 ∈ ℕ 𝐴 ∈ ℂ)
2625ad3antrrr 730 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) → ∀𝑘 ∈ ℕ 𝐴 ∈ ℂ)
27 elfznn 13593 . . . . . . . . 9 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
2813nfel1 2922 . . . . . . . . . . 11 𝑘𝑛 / 𝑘𝐴 ∈ ℂ
2911eleq1d 2826 . . . . . . . . . . 11 (𝑘 = 𝑛 → (𝐴 ∈ ℂ ↔ 𝑛 / 𝑘𝐴 ∈ ℂ))
3028, 29rspc 3610 . . . . . . . . . 10 (𝑛 ∈ ℕ → (∀𝑘 ∈ ℕ 𝐴 ∈ ℂ → 𝑛 / 𝑘𝐴 ∈ ℂ))
3130impcom 407 . . . . . . . . 9 ((∀𝑘 ∈ ℕ 𝐴 ∈ ℂ ∧ 𝑛 ∈ ℕ) → 𝑛 / 𝑘𝐴 ∈ ℂ)
3226, 27, 31syl2an 596 . . . . . . . 8 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 / 𝑘𝐴 ∈ ℂ)
3315, 32fsumcl 15769 . . . . . . 7 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))𝑛 / 𝑘𝐴 ∈ ℂ)
3414, 33eqeltrid 2845 . . . . . 6 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 ∈ ℂ)
35 rpcn 13045 . . . . . . 7 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
3635adantl 481 . . . . . 6 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
37 rpne0 13051 . . . . . . 7 (𝑥 ∈ ℝ+𝑥 ≠ 0)
3837adantl 481 . . . . . 6 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
3934, 36, 38divcld 12043 . . . . 5 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) → (Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥) ∈ ℂ)
40 simplrl 777 . . . . . . 7 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → 𝑐 ∈ (1[,)+∞))
41 1re 11261 . . . . . . . 8 1 ∈ ℝ
42 elicopnf 13485 . . . . . . . 8 (1 ∈ ℝ → (𝑐 ∈ (1[,)+∞) ↔ (𝑐 ∈ ℝ ∧ 1 ≤ 𝑐)))
4341, 42ax-mp 5 . . . . . . 7 (𝑐 ∈ (1[,)+∞) ↔ (𝑐 ∈ ℝ ∧ 1 ≤ 𝑐))
4440, 43sylib 218 . . . . . 6 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → (𝑐 ∈ ℝ ∧ 1 ≤ 𝑐))
4544simpld 494 . . . . 5 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → 𝑐 ∈ ℝ)
46 fzfid 14014 . . . . . . 7 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → (1...(⌊‘𝑐)) ∈ Fin)
4725ad2antrr 726 . . . . . . . . 9 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → ∀𝑘 ∈ ℕ 𝐴 ∈ ℂ)
48 elfznn 13593 . . . . . . . . 9 (𝑛 ∈ (1...(⌊‘𝑐)) → 𝑛 ∈ ℕ)
4947, 48, 31syl2an 596 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑛 ∈ (1...(⌊‘𝑐))) → 𝑛 / 𝑘𝐴 ∈ ℂ)
5049abscld 15475 . . . . . . 7 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑛 ∈ (1...(⌊‘𝑐))) → (abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
5146, 50fsumrecl 15770 . . . . . 6 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
52 simplrr 778 . . . . . 6 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → 𝑚 ∈ ℝ)
5351, 52readdcld 11290 . . . . 5 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚) ∈ ℝ)
5434, 36, 38absdivd 15494 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) = ((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) / (abs‘𝑥)))
5554adantrr 717 . . . . . . 7 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) = ((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) / (abs‘𝑥)))
56 rprege0 13050 . . . . . . . . . 10 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
5756ad2antrl 728 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
58 absid 15335 . . . . . . . . 9 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
5957, 58syl 17 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (abs‘𝑥) = 𝑥)
6059oveq2d 7447 . . . . . . 7 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) / (abs‘𝑥)) = ((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) / 𝑥))
6155, 60eqtrd 2777 . . . . . 6 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) = ((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) / 𝑥))
6234adantrr 717 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 ∈ ℂ)
6362abscld 15475 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) ∈ ℝ)
64 fzfid 14014 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (1...(⌊‘𝑥)) ∈ Fin)
6547, 27, 31syl2an 596 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 / 𝑘𝐴 ∈ ℂ)
6665adantlr 715 . . . . . . . . . 10 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 / 𝑘𝐴 ∈ ℂ)
6766abscld 15475 . . . . . . . . 9 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
6864, 67fsumrecl 15770 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
6957simpld 494 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 𝑥 ∈ ℝ)
7051adantr 480 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
7152adantr 480 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 𝑚 ∈ ℝ)
7270, 71readdcld 11290 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚) ∈ ℝ)
7369, 72remulcld 11291 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (𝑥 · (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚)) ∈ ℝ)
7414fveq2i 6909 . . . . . . . . 9 (abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) = (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))𝑛 / 𝑘𝐴)
7564, 66fsumabs 15837 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))𝑛 / 𝑘𝐴) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴))
7674, 75eqbrtrid 5178 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴))
77 fzfid 14014 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (((⌊‘𝑐) + 1)...(⌊‘𝑥)) ∈ Fin)
78 ssun2 4179 . . . . . . . . . . . . . 14 (((⌊‘𝑐) + 1)...(⌊‘𝑥)) ⊆ ((1...(⌊‘𝑐)) ∪ (((⌊‘𝑐) + 1)...(⌊‘𝑥)))
79 flge1nn 13861 . . . . . . . . . . . . . . . . . 18 ((𝑐 ∈ ℝ ∧ 1 ≤ 𝑐) → (⌊‘𝑐) ∈ ℕ)
8044, 79syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → (⌊‘𝑐) ∈ ℕ)
8180adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (⌊‘𝑐) ∈ ℕ)
8281nnred 12281 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (⌊‘𝑐) ∈ ℝ)
8345adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 𝑐 ∈ ℝ)
84 flle 13839 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ ℝ → (⌊‘𝑐) ≤ 𝑐)
8583, 84syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (⌊‘𝑐) ≤ 𝑐)
86 simprr 773 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 𝑐𝑥)
8782, 83, 69, 85, 86letrd 11418 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (⌊‘𝑐) ≤ 𝑥)
88 fznnfl 13902 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → ((⌊‘𝑐) ∈ (1...(⌊‘𝑥)) ↔ ((⌊‘𝑐) ∈ ℕ ∧ (⌊‘𝑐) ≤ 𝑥)))
8969, 88syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((⌊‘𝑐) ∈ (1...(⌊‘𝑥)) ↔ ((⌊‘𝑐) ∈ ℕ ∧ (⌊‘𝑐) ≤ 𝑥)))
9081, 87, 89mpbir2and 713 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (⌊‘𝑐) ∈ (1...(⌊‘𝑥)))
91 fzsplit 13590 . . . . . . . . . . . . . . 15 ((⌊‘𝑐) ∈ (1...(⌊‘𝑥)) → (1...(⌊‘𝑥)) = ((1...(⌊‘𝑐)) ∪ (((⌊‘𝑐) + 1)...(⌊‘𝑥))))
9290, 91syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (1...(⌊‘𝑥)) = ((1...(⌊‘𝑐)) ∪ (((⌊‘𝑐) + 1)...(⌊‘𝑥))))
9378, 92sseqtrrid 4027 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (((⌊‘𝑐) + 1)...(⌊‘𝑥)) ⊆ (1...(⌊‘𝑥)))
9493sselda 3983 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))) → 𝑛 ∈ (1...(⌊‘𝑥)))
9565abscld 15475 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
9695adantlr 715 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
9794, 96syldan 591 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))) → (abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
9877, 97fsumrecl 15770 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
9969, 70remulcld 11291 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)) ∈ ℝ)
10069, 71remulcld 11291 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (𝑥 · 𝑚) ∈ ℝ)
10170recnd 11289 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) ∈ ℂ)
102101mullidd 11279 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (1 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)) = Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴))
103 1red 11262 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 1 ∈ ℝ)
10449absge0d 15483 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑛 ∈ (1...(⌊‘𝑐))) → 0 ≤ (abs‘𝑛 / 𝑘𝐴))
10546, 50, 104fsumge0 15831 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴))
10651, 105jca 511 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) ∈ ℝ ∧ 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)))
107106adantr 480 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) ∈ ℝ ∧ 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)))
10844simprd 495 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → 1 ≤ 𝑐)
109108adantr 480 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 1 ≤ 𝑐)
110103, 83, 69, 109, 86letrd 11418 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 1 ≤ 𝑥)
111 lemul1a 12121 . . . . . . . . . . . 12 (((1 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) ∈ ℝ ∧ 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴))) ∧ 1 ≤ 𝑥) → (1 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)) ≤ (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)))
112103, 69, 107, 110, 111syl31anc 1375 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (1 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)) ≤ (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)))
113102, 112eqbrtrrd 5167 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) ≤ (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)))
114 hashcl 14395 . . . . . . . . . . . . 13 ((((⌊‘𝑐) + 1)...(⌊‘𝑥)) ∈ Fin → (♯‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) ∈ ℕ0)
115 nn0re 12535 . . . . . . . . . . . . 13 ((♯‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) ∈ ℕ0 → (♯‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) ∈ ℝ)
11677, 114, 1153syl 18 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (♯‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) ∈ ℝ)
117116, 71remulcld 11291 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((♯‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) · 𝑚) ∈ ℝ)
11871adantr 480 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))) → 𝑚 ∈ ℝ)
119 elfzuz 13560 . . . . . . . . . . . . . 14 (𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥)) → 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1)))
12081peano2nnd 12283 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((⌊‘𝑐) + 1) ∈ ℕ)
121 eluznn 12960 . . . . . . . . . . . . . . . 16 ((((⌊‘𝑐) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 𝑛 ∈ ℕ)
122120, 121sylan 580 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 𝑛 ∈ ℕ)
123 simpllr 776 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚))
12483adantr 480 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 𝑐 ∈ ℝ)
125 reflcl 13836 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ℝ → (⌊‘𝑐) ∈ ℝ)
126 peano2re 11434 . . . . . . . . . . . . . . . . 17 ((⌊‘𝑐) ∈ ℝ → ((⌊‘𝑐) + 1) ∈ ℝ)
127124, 125, 1263syl 18 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → ((⌊‘𝑐) + 1) ∈ ℝ)
128122nnred 12281 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 𝑛 ∈ ℝ)
129 fllep1 13841 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ℝ → 𝑐 ≤ ((⌊‘𝑐) + 1))
130124, 129syl 17 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 𝑐 ≤ ((⌊‘𝑐) + 1))
131 eluzle 12891 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1)) → ((⌊‘𝑐) + 1) ≤ 𝑛)
132131adantl 481 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → ((⌊‘𝑐) + 1) ≤ 𝑛)
133124, 127, 128, 130, 132letrd 11418 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 𝑐𝑛)
134 nfv 1914 . . . . . . . . . . . . . . . . 17 𝑘 𝑐𝑛
135 nfcv 2905 . . . . . . . . . . . . . . . . . . 19 𝑘abs
136135, 13nffv 6916 . . . . . . . . . . . . . . . . . 18 𝑘(abs‘𝑛 / 𝑘𝐴)
137 nfcv 2905 . . . . . . . . . . . . . . . . . 18 𝑘
138 nfcv 2905 . . . . . . . . . . . . . . . . . 18 𝑘𝑚
139136, 137, 138nfbr 5190 . . . . . . . . . . . . . . . . 17 𝑘(abs‘𝑛 / 𝑘𝐴) ≤ 𝑚
140134, 139nfim 1896 . . . . . . . . . . . . . . . 16 𝑘(𝑐𝑛 → (abs‘𝑛 / 𝑘𝐴) ≤ 𝑚)
141 breq2 5147 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → (𝑐𝑘𝑐𝑛))
14211fveq2d 6910 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → (abs‘𝐴) = (abs‘𝑛 / 𝑘𝐴))
143142breq1d 5153 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → ((abs‘𝐴) ≤ 𝑚 ↔ (abs‘𝑛 / 𝑘𝐴) ≤ 𝑚))
144141, 143imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → ((𝑐𝑘 → (abs‘𝐴) ≤ 𝑚) ↔ (𝑐𝑛 → (abs‘𝑛 / 𝑘𝐴) ≤ 𝑚)))
145140, 144rspc 3610 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚) → (𝑐𝑛 → (abs‘𝑛 / 𝑘𝐴) ≤ 𝑚)))
146122, 123, 133, 145syl3c 66 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → (abs‘𝑛 / 𝑘𝐴) ≤ 𝑚)
147119, 146sylan2 593 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))) → (abs‘𝑛 / 𝑘𝐴) ≤ 𝑚)
14877, 97, 118, 147fsumle 15835 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴) ≤ Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))𝑚)
14971recnd 11289 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 𝑚 ∈ ℂ)
150 fsumconst 15826 . . . . . . . . . . . . 13 (((((⌊‘𝑐) + 1)...(⌊‘𝑥)) ∈ Fin ∧ 𝑚 ∈ ℂ) → Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))𝑚 = ((♯‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) · 𝑚))
15177, 149, 150syl2anc 584 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))𝑚 = ((♯‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) · 𝑚))
152148, 151breqtrd 5169 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴) ≤ ((♯‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) · 𝑚))
153 biidd 262 . . . . . . . . . . . . 13 (𝑛 = ((⌊‘𝑐) + 1) → (0 ≤ 𝑚 ↔ 0 ≤ 𝑚))
154 0red 11264 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 0 ∈ ℝ)
15547, 30mpan9 506 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑛 ∈ ℕ) → 𝑛 / 𝑘𝐴 ∈ ℂ)
156155adantlr 715 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ ℕ) → 𝑛 / 𝑘𝐴 ∈ ℂ)
157122, 156syldan 591 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 𝑛 / 𝑘𝐴 ∈ ℂ)
158157abscld 15475 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → (abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
15971adantr 480 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 𝑚 ∈ ℝ)
160157absge0d 15483 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 0 ≤ (abs‘𝑛 / 𝑘𝐴))
161154, 158, 159, 160, 146letrd 11418 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 0 ≤ 𝑚)
162161ralrimiva 3146 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ∀𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))0 ≤ 𝑚)
163120nnzd 12640 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((⌊‘𝑐) + 1) ∈ ℤ)
164 uzid 12893 . . . . . . . . . . . . . 14 (((⌊‘𝑐) + 1) ∈ ℤ → ((⌊‘𝑐) + 1) ∈ (ℤ‘((⌊‘𝑐) + 1)))
165163, 164syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((⌊‘𝑐) + 1) ∈ (ℤ‘((⌊‘𝑐) + 1)))
166153, 162, 165rspcdva 3623 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 0 ≤ 𝑚)
167 reflcl 13836 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (⌊‘𝑥) ∈ ℝ)
16869, 167syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (⌊‘𝑥) ∈ ℝ)
169 ssdomg 9040 . . . . . . . . . . . . . . . 16 ((1...(⌊‘𝑥)) ∈ Fin → ((((⌊‘𝑐) + 1)...(⌊‘𝑥)) ⊆ (1...(⌊‘𝑥)) → (((⌊‘𝑐) + 1)...(⌊‘𝑥)) ≼ (1...(⌊‘𝑥))))
17064, 93, 169sylc 65 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (((⌊‘𝑐) + 1)...(⌊‘𝑥)) ≼ (1...(⌊‘𝑥)))
171 hashdomi 14419 . . . . . . . . . . . . . . 15 ((((⌊‘𝑐) + 1)...(⌊‘𝑥)) ≼ (1...(⌊‘𝑥)) → (♯‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) ≤ (♯‘(1...(⌊‘𝑥))))
172170, 171syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (♯‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) ≤ (♯‘(1...(⌊‘𝑥))))
173 flge0nn0 13860 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ0)
174 hashfz1 14385 . . . . . . . . . . . . . . 15 ((⌊‘𝑥) ∈ ℕ0 → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
17557, 173, 1743syl 18 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
176172, 175breqtrd 5169 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (♯‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) ≤ (⌊‘𝑥))
177 flle 13839 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
17869, 177syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (⌊‘𝑥) ≤ 𝑥)
179116, 168, 69, 176, 178letrd 11418 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (♯‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) ≤ 𝑥)
180116, 69, 71, 166, 179lemul1ad 12207 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((♯‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) · 𝑚) ≤ (𝑥 · 𝑚))
18198, 117, 100, 152, 180letrd 11418 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴) ≤ (𝑥 · 𝑚))
18270, 98, 99, 100, 113, 181le2addd 11882 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴)) ≤ ((𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)) + (𝑥 · 𝑚)))
183 ltp1 12107 . . . . . . . . . . 11 ((⌊‘𝑐) ∈ ℝ → (⌊‘𝑐) < ((⌊‘𝑐) + 1))
184 fzdisj 13591 . . . . . . . . . . 11 ((⌊‘𝑐) < ((⌊‘𝑐) + 1) → ((1...(⌊‘𝑐)) ∩ (((⌊‘𝑐) + 1)...(⌊‘𝑥))) = ∅)
18582, 183, 1843syl 18 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((1...(⌊‘𝑐)) ∩ (((⌊‘𝑐) + 1)...(⌊‘𝑥))) = ∅)
18696recnd 11289 . . . . . . . . . 10 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝑛 / 𝑘𝐴) ∈ ℂ)
187185, 92, 64, 186fsumsplit 15777 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴) = (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴)))
18836adantrr 717 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 𝑥 ∈ ℂ)
189188, 101, 149adddid 11285 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (𝑥 · (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚)) = ((𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)) + (𝑥 · 𝑚)))
190182, 187, 1893brtr4d 5175 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴) ≤ (𝑥 · (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚)))
19163, 68, 73, 76, 190letrd 11418 . . . . . . 7 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) ≤ (𝑥 · (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚)))
192 rpregt0 13049 . . . . . . . . 9 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
193192ad2antrl 728 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
194 ledivmul 12144 . . . . . . . 8 (((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) ∈ ℝ ∧ (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚) ∈ ℝ ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → (((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) / 𝑥) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚) ↔ (abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) ≤ (𝑥 · (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚))))
19563, 72, 193, 194syl3anc 1373 . . . . . . 7 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) / 𝑥) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚) ↔ (abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) ≤ (𝑥 · (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚))))
196191, 195mpbird 257 . . . . . 6 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) / 𝑥) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚))
19761, 196eqbrtrd 5165 . . . . 5 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚))
19810, 39, 45, 53, 197elo1d 15572 . . . 4 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → (𝑥 ∈ ℝ+ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) ∈ 𝑂(1))
199198ex 412 . . 3 ((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) → (∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚) → (𝑥 ∈ ℝ+ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) ∈ 𝑂(1)))
200199rexlimdvva 3213 . 2 (𝜑 → (∃𝑐 ∈ (1[,)+∞)∃𝑚 ∈ ℝ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚) → (𝑥 ∈ ℝ+ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) ∈ 𝑂(1)))
2018, 200mpd 15 1 (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) ∈ 𝑂(1))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  wne 2940  wral 3061  wrex 3070  csb 3899  cun 3949  cin 3950  wss 3951  c0 4333   class class class wbr 5143  cmpt 5225  dom cdm 5685  wf 6557  cfv 6561  (class class class)co 7431  cdom 8983  Fincfn 8985  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  +∞cpnf 11292   < clt 11295  cle 11296   / cdiv 11920  cn 12266  0cn0 12526  cz 12613  cuz 12878  +crp 13034  [,)cico 13389  ...cfz 13547  cfl 13830  chash 14369  abscabs 15273  𝑂(1)co1 15522  Σcsu 15722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-oadd 8510  df-er 8745  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-xnn0 12600  df-z 12614  df-uz 12879  df-rp 13035  df-ico 13393  df-fz 13548  df-fzo 13695  df-fl 13832  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-o1 15526  df-lo1 15527  df-sum 15723
This theorem is referenced by:  selberg2lem  27594
  Copyright terms: Public domain W3C validator