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

Theorem o1fsum 14589
 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 11062 . . . . 5 ℕ ⊆ ℝ
32a1i 11 . . . 4 (𝜑 → ℕ ⊆ ℝ)
4 o1fsum.1 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝐴𝑉)
54, 1o1mptrcl 14397 . . . 4 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ ℂ)
6 1red 10093 . . . 4 (𝜑 → 1 ∈ ℝ)
73, 5, 6elo1mpt2 14310 . . 3 (𝜑 → ((𝑘 ∈ ℕ ↦ 𝐴) ∈ 𝑂(1) ↔ ∃𝑐 ∈ (1[,)+∞)∃𝑚 ∈ ℝ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)))
81, 7mpbid 222 . 2 (𝜑 → ∃𝑐 ∈ (1[,)+∞)∃𝑚 ∈ ℝ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚))
9 rpssre 11881 . . . . . 6 + ⊆ ℝ
109a1i 11 . . . . 5 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → ℝ+ ⊆ ℝ)
11 nfcv 2793 . . . . . . . 8 𝑛𝐴
12 nfcsb1v 3582 . . . . . . . 8 𝑘𝑛 / 𝑘𝐴
13 csbeq1a 3575 . . . . . . . 8 (𝑘 = 𝑛𝐴 = 𝑛 / 𝑘𝐴)
1411, 12, 13cbvsumi 14471 . . . . . . 7 Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 = Σ𝑛 ∈ (1...(⌊‘𝑥))𝑛 / 𝑘𝐴
15 fzfid 12812 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
16 o1f 14304 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ↦ 𝐴) ∈ 𝑂(1) → (𝑘 ∈ ℕ ↦ 𝐴):dom (𝑘 ∈ ℕ ↦ 𝐴)⟶ℂ)
171, 16syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ ℕ ↦ 𝐴):dom (𝑘 ∈ ℕ ↦ 𝐴)⟶ℂ)
184ralrimiva 2995 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑘 ∈ ℕ 𝐴𝑉)
19 dmmptg 5670 . . . . . . . . . . . . . 14 (∀𝑘 ∈ ℕ 𝐴𝑉 → dom (𝑘 ∈ ℕ ↦ 𝐴) = ℕ)
2018, 19syl 17 . . . . . . . . . . . . 13 (𝜑 → dom (𝑘 ∈ ℕ ↦ 𝐴) = ℕ)
2120feq2d 6069 . . . . . . . . . . . 12 (𝜑 → ((𝑘 ∈ ℕ ↦ 𝐴):dom (𝑘 ∈ ℕ ↦ 𝐴)⟶ℂ ↔ (𝑘 ∈ ℕ ↦ 𝐴):ℕ⟶ℂ))
2217, 21mpbid 222 . . . . . . . . . . 11 (𝜑 → (𝑘 ∈ ℕ ↦ 𝐴):ℕ⟶ℂ)
23 eqid 2651 . . . . . . . . . . . 12 (𝑘 ∈ ℕ ↦ 𝐴) = (𝑘 ∈ ℕ ↦ 𝐴)
2423fmpt 6421 . . . . . . . . . . 11 (∀𝑘 ∈ ℕ 𝐴 ∈ ℂ ↔ (𝑘 ∈ ℕ ↦ 𝐴):ℕ⟶ℂ)
2522, 24sylibr 224 . . . . . . . . . 10 (𝜑 → ∀𝑘 ∈ ℕ 𝐴 ∈ ℂ)
2625ad3antrrr 766 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) → ∀𝑘 ∈ ℕ 𝐴 ∈ ℂ)
27 elfznn 12408 . . . . . . . . 9 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
2812nfel1 2808 . . . . . . . . . . 11 𝑘𝑛 / 𝑘𝐴 ∈ ℂ
2913eleq1d 2715 . . . . . . . . . . 11 (𝑘 = 𝑛 → (𝐴 ∈ ℂ ↔ 𝑛 / 𝑘𝐴 ∈ ℂ))
3028, 29rspc 3334 . . . . . . . . . 10 (𝑛 ∈ ℕ → (∀𝑘 ∈ ℕ 𝐴 ∈ ℂ → 𝑛 / 𝑘𝐴 ∈ ℂ))
3130impcom 445 . . . . . . . . 9 ((∀𝑘 ∈ ℕ 𝐴 ∈ ℂ ∧ 𝑛 ∈ ℕ) → 𝑛 / 𝑘𝐴 ∈ ℂ)
3226, 27, 31syl2an 493 . . . . . . . 8 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 / 𝑘𝐴 ∈ ℂ)
3315, 32fsumcl 14508 . . . . . . 7 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))𝑛 / 𝑘𝐴 ∈ ℂ)
3414, 33syl5eqel 2734 . . . . . 6 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 ∈ ℂ)
35 rpcn 11879 . . . . . . 7 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
3635adantl 481 . . . . . 6 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
37 rpne0 11886 . . . . . . 7 (𝑥 ∈ ℝ+𝑥 ≠ 0)
3837adantl 481 . . . . . 6 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
3934, 36, 38divcld 10839 . . . . 5 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) → (Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥) ∈ ℂ)
40 simplrl 817 . . . . . . 7 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → 𝑐 ∈ (1[,)+∞))
41 1re 10077 . . . . . . . 8 1 ∈ ℝ
42 elicopnf 12307 . . . . . . . 8 (1 ∈ ℝ → (𝑐 ∈ (1[,)+∞) ↔ (𝑐 ∈ ℝ ∧ 1 ≤ 𝑐)))
4341, 42ax-mp 5 . . . . . . 7 (𝑐 ∈ (1[,)+∞) ↔ (𝑐 ∈ ℝ ∧ 1 ≤ 𝑐))
4440, 43sylib 208 . . . . . 6 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → (𝑐 ∈ ℝ ∧ 1 ≤ 𝑐))
4544simpld 474 . . . . 5 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → 𝑐 ∈ ℝ)
46 fzfid 12812 . . . . . . 7 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → (1...(⌊‘𝑐)) ∈ Fin)
4725ad2antrr 762 . . . . . . . . 9 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → ∀𝑘 ∈ ℕ 𝐴 ∈ ℂ)
48 elfznn 12408 . . . . . . . . 9 (𝑛 ∈ (1...(⌊‘𝑐)) → 𝑛 ∈ ℕ)
4947, 48, 31syl2an 493 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑛 ∈ (1...(⌊‘𝑐))) → 𝑛 / 𝑘𝐴 ∈ ℂ)
5049abscld 14219 . . . . . . 7 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑛 ∈ (1...(⌊‘𝑐))) → (abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
5146, 50fsumrecl 14509 . . . . . 6 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
52 simplrr 818 . . . . . 6 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → 𝑚 ∈ ℝ)
5351, 52readdcld 10107 . . . . 5 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚) ∈ ℝ)
5434, 36, 38absdivd 14238 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑥 ∈ ℝ+) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) = ((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) / (abs‘𝑥)))
5554adantrr 753 . . . . . . 7 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) = ((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) / (abs‘𝑥)))
56 rprege0 11885 . . . . . . . . . 10 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
5756ad2antrl 764 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
58 absid 14080 . . . . . . . . 9 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
5957, 58syl 17 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (abs‘𝑥) = 𝑥)
6059oveq2d 6706 . . . . . . 7 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) / (abs‘𝑥)) = ((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) / 𝑥))
6155, 60eqtrd 2685 . . . . . 6 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) = ((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) / 𝑥))
6234adantrr 753 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 ∈ ℂ)
6362abscld 14219 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) ∈ ℝ)
64 fzfid 12812 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (1...(⌊‘𝑥)) ∈ Fin)
6547, 27, 31syl2an 493 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 / 𝑘𝐴 ∈ ℂ)
6665adantlr 751 . . . . . . . . . 10 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 / 𝑘𝐴 ∈ ℂ)
6766abscld 14219 . . . . . . . . 9 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
6864, 67fsumrecl 14509 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
6957simpld 474 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 𝑥 ∈ ℝ)
7051adantr 480 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
7152adantr 480 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 𝑚 ∈ ℝ)
7270, 71readdcld 10107 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚) ∈ ℝ)
7369, 72remulcld 10108 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (𝑥 · (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚)) ∈ ℝ)
7414fveq2i 6232 . . . . . . . . 9 (abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) = (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))𝑛 / 𝑘𝐴)
7564, 66fsumabs 14577 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))𝑛 / 𝑘𝐴) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴))
7674, 75syl5eqbr 4720 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴))
77 fzfid 12812 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (((⌊‘𝑐) + 1)...(⌊‘𝑥)) ∈ Fin)
78 ssun2 3810 . . . . . . . . . . . . . 14 (((⌊‘𝑐) + 1)...(⌊‘𝑥)) ⊆ ((1...(⌊‘𝑐)) ∪ (((⌊‘𝑐) + 1)...(⌊‘𝑥)))
79 flge1nn 12662 . . . . . . . . . . . . . . . . . 18 ((𝑐 ∈ ℝ ∧ 1 ≤ 𝑐) → (⌊‘𝑐) ∈ ℕ)
8044, 79syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → (⌊‘𝑐) ∈ ℕ)
8180adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (⌊‘𝑐) ∈ ℕ)
8281nnred 11073 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (⌊‘𝑐) ∈ ℝ)
8345adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 𝑐 ∈ ℝ)
84 flle 12640 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ ℝ → (⌊‘𝑐) ≤ 𝑐)
8583, 84syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (⌊‘𝑐) ≤ 𝑐)
86 simprr 811 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 𝑐𝑥)
8782, 83, 69, 85, 86letrd 10232 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (⌊‘𝑐) ≤ 𝑥)
88 fznnfl 12701 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → ((⌊‘𝑐) ∈ (1...(⌊‘𝑥)) ↔ ((⌊‘𝑐) ∈ ℕ ∧ (⌊‘𝑐) ≤ 𝑥)))
8969, 88syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((⌊‘𝑐) ∈ (1...(⌊‘𝑥)) ↔ ((⌊‘𝑐) ∈ ℕ ∧ (⌊‘𝑐) ≤ 𝑥)))
9081, 87, 89mpbir2and 977 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (⌊‘𝑐) ∈ (1...(⌊‘𝑥)))
91 fzsplit 12405 . . . . . . . . . . . . . . 15 ((⌊‘𝑐) ∈ (1...(⌊‘𝑥)) → (1...(⌊‘𝑥)) = ((1...(⌊‘𝑐)) ∪ (((⌊‘𝑐) + 1)...(⌊‘𝑥))))
9290, 91syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (1...(⌊‘𝑥)) = ((1...(⌊‘𝑐)) ∪ (((⌊‘𝑐) + 1)...(⌊‘𝑥))))
9378, 92syl5sseqr 3687 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (((⌊‘𝑐) + 1)...(⌊‘𝑥)) ⊆ (1...(⌊‘𝑥)))
9493sselda 3636 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))) → 𝑛 ∈ (1...(⌊‘𝑥)))
9565abscld 14219 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
9695adantlr 751 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
9794, 96syldan 486 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))) → (abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
9877, 97fsumrecl 14509 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
9969, 70remulcld 10108 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)) ∈ ℝ)
10069, 71remulcld 10108 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (𝑥 · 𝑚) ∈ ℝ)
10170recnd 10106 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) ∈ ℂ)
102101mulid2d 10096 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (1 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)) = Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴))
103 1red 10093 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 1 ∈ ℝ)
10449absge0d 14227 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑛 ∈ (1...(⌊‘𝑐))) → 0 ≤ (abs‘𝑛 / 𝑘𝐴))
10546, 50, 104fsumge0 14571 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴))
10651, 105jca 553 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) ∈ ℝ ∧ 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)))
107106adantr 480 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) ∈ ℝ ∧ 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)))
10844simprd 478 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → 1 ≤ 𝑐)
109108adantr 480 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 1 ≤ 𝑐)
110103, 83, 69, 109, 86letrd 10232 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 1 ≤ 𝑥)
111 lemul1a 10915 . . . . . . . . . . . 12 (((1 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) ∈ ℝ ∧ 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴))) ∧ 1 ≤ 𝑥) → (1 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)) ≤ (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)))
112103, 69, 107, 110, 111syl31anc 1369 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (1 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)) ≤ (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)))
113102, 112eqbrtrrd 4709 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) ≤ (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)))
114 hashcl 13185 . . . . . . . . . . . . 13 ((((⌊‘𝑐) + 1)...(⌊‘𝑥)) ∈ Fin → (#‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) ∈ ℕ0)
115 nn0re 11339 . . . . . . . . . . . . 13 ((#‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) ∈ ℕ0 → (#‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) ∈ ℝ)
11677, 114, 1153syl 18 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (#‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) ∈ ℝ)
117116, 71remulcld 10108 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((#‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) · 𝑚) ∈ ℝ)
11871adantr 480 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))) → 𝑚 ∈ ℝ)
119 elfzuz 12376 . . . . . . . . . . . . . 14 (𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥)) → 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1)))
12081peano2nnd 11075 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((⌊‘𝑐) + 1) ∈ ℕ)
121 eluznn 11796 . . . . . . . . . . . . . . . 16 ((((⌊‘𝑐) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 𝑛 ∈ ℕ)
122120, 121sylan 487 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 𝑛 ∈ ℕ)
123 simpllr 815 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚))
12483adantr 480 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 𝑐 ∈ ℝ)
125 reflcl 12637 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ℝ → (⌊‘𝑐) ∈ ℝ)
126 peano2re 10247 . . . . . . . . . . . . . . . . 17 ((⌊‘𝑐) ∈ ℝ → ((⌊‘𝑐) + 1) ∈ ℝ)
127124, 125, 1263syl 18 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → ((⌊‘𝑐) + 1) ∈ ℝ)
128122nnred 11073 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 𝑛 ∈ ℝ)
129 fllep1 12642 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ℝ → 𝑐 ≤ ((⌊‘𝑐) + 1))
130124, 129syl 17 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 𝑐 ≤ ((⌊‘𝑐) + 1))
131 eluzle 11738 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1)) → ((⌊‘𝑐) + 1) ≤ 𝑛)
132131adantl 481 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → ((⌊‘𝑐) + 1) ≤ 𝑛)
133124, 127, 128, 130, 132letrd 10232 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 𝑐𝑛)
134 nfv 1883 . . . . . . . . . . . . . . . . 17 𝑘 𝑐𝑛
135 nfcv 2793 . . . . . . . . . . . . . . . . . . 19 𝑘abs
136135, 12nffv 6236 . . . . . . . . . . . . . . . . . 18 𝑘(abs‘𝑛 / 𝑘𝐴)
137 nfcv 2793 . . . . . . . . . . . . . . . . . 18 𝑘
138 nfcv 2793 . . . . . . . . . . . . . . . . . 18 𝑘𝑚
139136, 137, 138nfbr 4732 . . . . . . . . . . . . . . . . 17 𝑘(abs‘𝑛 / 𝑘𝐴) ≤ 𝑚
140134, 139nfim 1865 . . . . . . . . . . . . . . . 16 𝑘(𝑐𝑛 → (abs‘𝑛 / 𝑘𝐴) ≤ 𝑚)
141 breq2 4689 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → (𝑐𝑘𝑐𝑛))
14213fveq2d 6233 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → (abs‘𝐴) = (abs‘𝑛 / 𝑘𝐴))
143142breq1d 4695 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → ((abs‘𝐴) ≤ 𝑚 ↔ (abs‘𝑛 / 𝑘𝐴) ≤ 𝑚))
144141, 143imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → ((𝑐𝑘 → (abs‘𝐴) ≤ 𝑚) ↔ (𝑐𝑛 → (abs‘𝑛 / 𝑘𝐴) ≤ 𝑚)))
145140, 144rspc 3334 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚) → (𝑐𝑛 → (abs‘𝑛 / 𝑘𝐴) ≤ 𝑚)))
146122, 123, 133, 145syl3c 66 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → (abs‘𝑛 / 𝑘𝐴) ≤ 𝑚)
147119, 146sylan2 490 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))) → (abs‘𝑛 / 𝑘𝐴) ≤ 𝑚)
14877, 97, 118, 147fsumle 14575 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴) ≤ Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))𝑚)
14971recnd 10106 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 𝑚 ∈ ℂ)
150 fsumconst 14566 . . . . . . . . . . . . 13 (((((⌊‘𝑐) + 1)...(⌊‘𝑥)) ∈ Fin ∧ 𝑚 ∈ ℂ) → Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))𝑚 = ((#‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) · 𝑚))
15177, 149, 150syl2anc 694 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))𝑚 = ((#‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) · 𝑚))
152148, 151breqtrd 4711 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴) ≤ ((#‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) · 𝑚))
153120nnzd 11519 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((⌊‘𝑐) + 1) ∈ ℤ)
154 uzid 11740 . . . . . . . . . . . . . 14 (((⌊‘𝑐) + 1) ∈ ℤ → ((⌊‘𝑐) + 1) ∈ (ℤ‘((⌊‘𝑐) + 1)))
155153, 154syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((⌊‘𝑐) + 1) ∈ (ℤ‘((⌊‘𝑐) + 1)))
156 0red 10079 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 0 ∈ ℝ)
15747, 30mpan9 485 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ 𝑛 ∈ ℕ) → 𝑛 / 𝑘𝐴 ∈ ℂ)
158157adantlr 751 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ ℕ) → 𝑛 / 𝑘𝐴 ∈ ℂ)
159122, 158syldan 486 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 𝑛 / 𝑘𝐴 ∈ ℂ)
160159abscld 14219 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → (abs‘𝑛 / 𝑘𝐴) ∈ ℝ)
16171adantr 480 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 𝑚 ∈ ℝ)
162159absge0d 14227 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 0 ≤ (abs‘𝑛 / 𝑘𝐴))
163156, 160, 161, 162, 146letrd 10232 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))) → 0 ≤ 𝑚)
164163ralrimiva 2995 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ∀𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))0 ≤ 𝑚)
165 biidd 252 . . . . . . . . . . . . . 14 (𝑛 = ((⌊‘𝑐) + 1) → (0 ≤ 𝑚 ↔ 0 ≤ 𝑚))
166165rspcv 3336 . . . . . . . . . . . . 13 (((⌊‘𝑐) + 1) ∈ (ℤ‘((⌊‘𝑐) + 1)) → (∀𝑛 ∈ (ℤ‘((⌊‘𝑐) + 1))0 ≤ 𝑚 → 0 ≤ 𝑚))
167155, 164, 166sylc 65 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 0 ≤ 𝑚)
168 reflcl 12637 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (⌊‘𝑥) ∈ ℝ)
16969, 168syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (⌊‘𝑥) ∈ ℝ)
170 ssdomg 8043 . . . . . . . . . . . . . . . 16 ((1...(⌊‘𝑥)) ∈ Fin → ((((⌊‘𝑐) + 1)...(⌊‘𝑥)) ⊆ (1...(⌊‘𝑥)) → (((⌊‘𝑐) + 1)...(⌊‘𝑥)) ≼ (1...(⌊‘𝑥))))
17164, 93, 170sylc 65 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (((⌊‘𝑐) + 1)...(⌊‘𝑥)) ≼ (1...(⌊‘𝑥)))
172 hashdomi 13207 . . . . . . . . . . . . . . 15 ((((⌊‘𝑐) + 1)...(⌊‘𝑥)) ≼ (1...(⌊‘𝑥)) → (#‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) ≤ (#‘(1...(⌊‘𝑥))))
173171, 172syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (#‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) ≤ (#‘(1...(⌊‘𝑥))))
174 flge0nn0 12661 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ0)
175 hashfz1 13174 . . . . . . . . . . . . . . 15 ((⌊‘𝑥) ∈ ℕ0 → (#‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
17657, 174, 1753syl 18 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (#‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
177173, 176breqtrd 4711 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (#‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) ≤ (⌊‘𝑥))
178 flle 12640 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
17969, 178syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (⌊‘𝑥) ≤ 𝑥)
180116, 169, 69, 177, 179letrd 10232 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (#‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) ≤ 𝑥)
181116, 69, 71, 167, 180lemul1ad 11001 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((#‘(((⌊‘𝑐) + 1)...(⌊‘𝑥))) · 𝑚) ≤ (𝑥 · 𝑚))
18298, 117, 100, 152, 181letrd 10232 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴) ≤ (𝑥 · 𝑚))
18370, 98, 99, 100, 113, 182le2addd 10684 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴)) ≤ ((𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)) + (𝑥 · 𝑚)))
184 ltp1 10899 . . . . . . . . . . 11 ((⌊‘𝑐) ∈ ℝ → (⌊‘𝑐) < ((⌊‘𝑐) + 1))
185 fzdisj 12406 . . . . . . . . . . 11 ((⌊‘𝑐) < ((⌊‘𝑐) + 1) → ((1...(⌊‘𝑐)) ∩ (((⌊‘𝑐) + 1)...(⌊‘𝑥))) = ∅)
18682, 184, 1853syl 18 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((1...(⌊‘𝑐)) ∩ (((⌊‘𝑐) + 1)...(⌊‘𝑥))) = ∅)
18796recnd 10106 . . . . . . . . . 10 (((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝑛 / 𝑘𝐴) ∈ ℂ)
188186, 92, 64, 187fsumsplit 14515 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴) = (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + Σ𝑛 ∈ (((⌊‘𝑐) + 1)...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴)))
18936adantrr 753 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → 𝑥 ∈ ℂ)
190189, 101, 149adddid 10102 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (𝑥 · (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚)) = ((𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴)) + (𝑥 · 𝑚)))
191183, 188, 1903brtr4d 4717 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘𝑛 / 𝑘𝐴) ≤ (𝑥 · (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚)))
19263, 68, 73, 76, 191letrd 10232 . . . . . . 7 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) ≤ (𝑥 · (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚)))
193 rpregt0 11884 . . . . . . . . 9 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
194193ad2antrl 764 . . . . . . . 8 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
195 ledivmul 10937 . . . . . . . 8 (((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) ∈ ℝ ∧ (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚) ∈ ℝ ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → (((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) / 𝑥) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚) ↔ (abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) ≤ (𝑥 · (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚))))
19663, 72, 194, 195syl3anc 1366 . . . . . . 7 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) / 𝑥) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚) ↔ (abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) ≤ (𝑥 · (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚))))
197192, 196mpbird 247 . . . . . 6 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → ((abs‘Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴) / 𝑥) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚))
19861, 197eqbrtrd 4707 . . . . 5 ((((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) ∧ (𝑥 ∈ ℝ+𝑐𝑥)) → (abs‘(Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑐))(abs‘𝑛 / 𝑘𝐴) + 𝑚))
19910, 39, 45, 53, 198elo1d 14311 . . . 4 (((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) ∧ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚)) → (𝑥 ∈ ℝ+ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) ∈ 𝑂(1))
200199ex 449 . . 3 ((𝜑 ∧ (𝑐 ∈ (1[,)+∞) ∧ 𝑚 ∈ ℝ)) → (∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚) → (𝑥 ∈ ℝ+ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) ∈ 𝑂(1)))
201200rexlimdvva 3067 . 2 (𝜑 → (∃𝑐 ∈ (1[,)+∞)∃𝑚 ∈ ℝ ∀𝑘 ∈ ℕ (𝑐𝑘 → (abs‘𝐴) ≤ 𝑚) → (𝑥 ∈ ℝ+ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) ∈ 𝑂(1)))
2028, 201mpd 15 1 (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))𝐴 / 𝑥)) ∈ 𝑂(1))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  ⦋csb 3566   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948   class class class wbr 4685   ↦ cmpt 4762  dom cdm 5143  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690   ≼ cdom 7995  Fincfn 7997  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  +∞cpnf 10109   < clt 10112   ≤ cle 10113   / cdiv 10722  ℕcn 11058  ℕ0cn0 11330  ℤcz 11415  ℤ≥cuz 11725  ℝ+crp 11870  [,)cico 12215  ...cfz 12364  ⌊cfl 12631  #chash 13157  abscabs 14018  𝑂(1)co1 14261  Σcsu 14460 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-xnn0 11402  df-z 11416  df-uz 11726  df-rp 11871  df-ico 12219  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-o1 14265  df-lo1 14266  df-sum 14461 This theorem is referenced by:  selberg2lem  25284
 Copyright terms: Public domain W3C validator