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

Theorem o1fsum 15705
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 12164 . . . . 5 β„• βŠ† ℝ
32a1i 11 . . . 4 (πœ‘ β†’ β„• βŠ† ℝ)
4 o1fsum.1 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐴 ∈ 𝑉)
54, 1o1mptrcl 15512 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐴 ∈ β„‚)
6 1red 11163 . . . 4 (πœ‘ β†’ 1 ∈ ℝ)
73, 5, 6elo1mpt2 15424 . . 3 (πœ‘ β†’ ((π‘˜ ∈ β„• ↦ 𝐴) ∈ 𝑂(1) ↔ βˆƒπ‘ ∈ (1[,)+∞)βˆƒπ‘š ∈ ℝ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)))
81, 7mpbid 231 . 2 (πœ‘ β†’ βˆƒπ‘ ∈ (1[,)+∞)βˆƒπ‘š ∈ ℝ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š))
9 rpssre 12929 . . . . . 6 ℝ+ βŠ† ℝ
109a1i 11 . . . . 5 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ ℝ+ βŠ† ℝ)
11 nfcv 2908 . . . . . . . 8 Ⅎ𝑛𝐴
12 nfcsb1v 3885 . . . . . . . 8 β„²π‘˜β¦‹π‘› / π‘˜β¦Œπ΄
13 csbeq1a 3874 . . . . . . . 8 (π‘˜ = 𝑛 β†’ 𝐴 = ⦋𝑛 / π‘˜β¦Œπ΄)
1411, 12, 13cbvsumi 15589 . . . . . . 7 Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))⦋𝑛 / π‘˜β¦Œπ΄
15 fzfid 13885 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ (1...(βŒŠβ€˜π‘₯)) ∈ Fin)
16 o1f 15418 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„• ↦ 𝐴) ∈ 𝑂(1) β†’ (π‘˜ ∈ β„• ↦ 𝐴):dom (π‘˜ ∈ β„• ↦ 𝐴)βŸΆβ„‚)
171, 16syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘˜ ∈ β„• ↦ 𝐴):dom (π‘˜ ∈ β„• ↦ 𝐴)βŸΆβ„‚)
184ralrimiva 3144 . . . . . . . . . . . . . 14 (πœ‘ β†’ βˆ€π‘˜ ∈ β„• 𝐴 ∈ 𝑉)
19 dmmptg 6199 . . . . . . . . . . . . . 14 (βˆ€π‘˜ ∈ β„• 𝐴 ∈ 𝑉 β†’ dom (π‘˜ ∈ β„• ↦ 𝐴) = β„•)
2018, 19syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ dom (π‘˜ ∈ β„• ↦ 𝐴) = β„•)
2120feq2d 6659 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘˜ ∈ β„• ↦ 𝐴):dom (π‘˜ ∈ β„• ↦ 𝐴)βŸΆβ„‚ ↔ (π‘˜ ∈ β„• ↦ 𝐴):β„•βŸΆβ„‚))
2217, 21mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ (π‘˜ ∈ β„• ↦ 𝐴):β„•βŸΆβ„‚)
23 eqid 2737 . . . . . . . . . . . 12 (π‘˜ ∈ β„• ↦ 𝐴) = (π‘˜ ∈ β„• ↦ 𝐴)
2423fmpt 7063 . . . . . . . . . . 11 (βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚ ↔ (π‘˜ ∈ β„• ↦ 𝐴):β„•βŸΆβ„‚)
2522, 24sylibr 233 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚)
2625ad3antrrr 729 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚)
27 elfznn 13477 . . . . . . . . 9 (𝑛 ∈ (1...(βŒŠβ€˜π‘₯)) β†’ 𝑛 ∈ β„•)
2812nfel1 2924 . . . . . . . . . . 11 β„²π‘˜β¦‹π‘› / π‘˜β¦Œπ΄ ∈ β„‚
2913eleq1d 2823 . . . . . . . . . . 11 (π‘˜ = 𝑛 β†’ (𝐴 ∈ β„‚ ↔ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚))
3028, 29rspc 3572 . . . . . . . . . 10 (𝑛 ∈ β„• β†’ (βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚ β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚))
3130impcom 409 . . . . . . . . 9 ((βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚ ∧ 𝑛 ∈ β„•) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
3226, 27, 31syl2an 597 . . . . . . . 8 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
3315, 32fsumcl 15625 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
3414, 33eqeltrid 2842 . . . . . 6 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 ∈ β„‚)
35 rpcn 12932 . . . . . . 7 (π‘₯ ∈ ℝ+ β†’ π‘₯ ∈ β„‚)
3635adantl 483 . . . . . 6 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ π‘₯ ∈ β„‚)
37 rpne0 12938 . . . . . . 7 (π‘₯ ∈ ℝ+ β†’ π‘₯ β‰  0)
3837adantl 483 . . . . . 6 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ π‘₯ β‰  0)
3934, 36, 38divcld 11938 . . . . 5 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯) ∈ β„‚)
40 simplrl 776 . . . . . . 7 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ 𝑐 ∈ (1[,)+∞))
41 1re 11162 . . . . . . . 8 1 ∈ ℝ
42 elicopnf 13369 . . . . . . . 8 (1 ∈ ℝ β†’ (𝑐 ∈ (1[,)+∞) ↔ (𝑐 ∈ ℝ ∧ 1 ≀ 𝑐)))
4341, 42ax-mp 5 . . . . . . 7 (𝑐 ∈ (1[,)+∞) ↔ (𝑐 ∈ ℝ ∧ 1 ≀ 𝑐))
4440, 43sylib 217 . . . . . 6 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (𝑐 ∈ ℝ ∧ 1 ≀ 𝑐))
4544simpld 496 . . . . 5 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ 𝑐 ∈ ℝ)
46 fzfid 13885 . . . . . . 7 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (1...(βŒŠβ€˜π‘)) ∈ Fin)
4725ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚)
48 elfznn 13477 . . . . . . . . 9 (𝑛 ∈ (1...(βŒŠβ€˜π‘)) β†’ 𝑛 ∈ β„•)
4947, 48, 31syl2an 597 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘))) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
5049abscld 15328 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
5146, 50fsumrecl 15626 . . . . . 6 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
52 simplrr 777 . . . . . 6 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ π‘š ∈ ℝ)
5351, 52readdcld 11191 . . . . 5 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š) ∈ ℝ)
5434, 36, 38absdivd 15347 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) = ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / (absβ€˜π‘₯)))
5554adantrr 716 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) = ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / (absβ€˜π‘₯)))
56 rprege0 12937 . . . . . . . . . 10 (π‘₯ ∈ ℝ+ β†’ (π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯))
5756ad2antrl 727 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯))
58 absid 15188 . . . . . . . . 9 ((π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯) β†’ (absβ€˜π‘₯) = π‘₯)
5957, 58syl 17 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜π‘₯) = π‘₯)
6059oveq2d 7378 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / (absβ€˜π‘₯)) = ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / π‘₯))
6155, 60eqtrd 2777 . . . . . 6 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) = ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / π‘₯))
6234adantrr 716 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 ∈ β„‚)
6362abscld 15328 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ∈ ℝ)
64 fzfid 13885 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (1...(βŒŠβ€˜π‘₯)) ∈ Fin)
6547, 27, 31syl2an 597 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
6665adantlr 714 . . . . . . . . . 10 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
6766abscld 15328 . . . . . . . . 9 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
6864, 67fsumrecl 15626 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
6957simpld 496 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ π‘₯ ∈ ℝ)
7051adantr 482 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
7152adantr 482 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ π‘š ∈ ℝ)
7270, 71readdcld 11191 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š) ∈ ℝ)
7369, 72remulcld 11192 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š)) ∈ ℝ)
7414fveq2i 6850 . . . . . . . . 9 (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) = (absβ€˜Ξ£π‘› ∈ (1...(βŒŠβ€˜π‘₯))⦋𝑛 / π‘˜β¦Œπ΄)
7564, 66fsumabs 15693 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜Ξ£π‘› ∈ (1...(βŒŠβ€˜π‘₯))⦋𝑛 / π‘˜β¦Œπ΄) ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
7674, 75eqbrtrid 5145 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
77 fzfid 13885 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) ∈ Fin)
78 ssun2 4138 . . . . . . . . . . . . . 14 (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) βŠ† ((1...(βŒŠβ€˜π‘)) βˆͺ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)))
79 flge1nn 13733 . . . . . . . . . . . . . . . . . 18 ((𝑐 ∈ ℝ ∧ 1 ≀ 𝑐) β†’ (βŒŠβ€˜π‘) ∈ β„•)
8044, 79syl 17 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (βŒŠβ€˜π‘) ∈ β„•)
8180adantr 482 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘) ∈ β„•)
8281nnred 12175 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘) ∈ ℝ)
8345adantr 482 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 𝑐 ∈ ℝ)
84 flle 13711 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ ℝ β†’ (βŒŠβ€˜π‘) ≀ 𝑐)
8583, 84syl 17 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘) ≀ 𝑐)
86 simprr 772 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 𝑐 ≀ π‘₯)
8782, 83, 69, 85, 86letrd 11319 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘) ≀ π‘₯)
88 fznnfl 13774 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ ℝ β†’ ((βŒŠβ€˜π‘) ∈ (1...(βŒŠβ€˜π‘₯)) ↔ ((βŒŠβ€˜π‘) ∈ β„• ∧ (βŒŠβ€˜π‘) ≀ π‘₯)))
8969, 88syl 17 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((βŒŠβ€˜π‘) ∈ (1...(βŒŠβ€˜π‘₯)) ↔ ((βŒŠβ€˜π‘) ∈ β„• ∧ (βŒŠβ€˜π‘) ≀ π‘₯)))
9081, 87, 89mpbir2and 712 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘) ∈ (1...(βŒŠβ€˜π‘₯)))
91 fzsplit 13474 . . . . . . . . . . . . . . 15 ((βŒŠβ€˜π‘) ∈ (1...(βŒŠβ€˜π‘₯)) β†’ (1...(βŒŠβ€˜π‘₯)) = ((1...(βŒŠβ€˜π‘)) βˆͺ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))))
9290, 91syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (1...(βŒŠβ€˜π‘₯)) = ((1...(βŒŠβ€˜π‘)) βˆͺ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))))
9378, 92sseqtrrid 4002 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) βŠ† (1...(βŒŠβ€˜π‘₯)))
9493sselda 3949 . . . . . . . . . . . 12 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯)))
9565abscld 15328 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
9695adantlr 714 . . . . . . . . . . . 12 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
9794, 96syldan 592 . . . . . . . . . . 11 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
9877, 97fsumrecl 15626 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
9969, 70remulcld 11192 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) ∈ ℝ)
10069, 71remulcld 11192 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ Β· π‘š) ∈ ℝ)
10170recnd 11190 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ β„‚)
102101mulid2d 11180 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (1 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
103 1red 11163 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 1 ∈ ℝ)
10449absge0d 15336 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘))) β†’ 0 ≀ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
10546, 50, 104fsumge0 15687 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ 0 ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
10651, 105jca 513 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ ∧ 0 ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
107106adantr 482 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ ∧ 0 ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
10844simprd 497 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ 1 ≀ 𝑐)
109108adantr 482 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 1 ≀ 𝑐)
110103, 83, 69, 109, 86letrd 11319 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 1 ≀ π‘₯)
111 lemul1a 12016 . . . . . . . . . . . 12 (((1 ∈ ℝ ∧ π‘₯ ∈ ℝ ∧ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ ∧ 0 ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))) ∧ 1 ≀ π‘₯) β†’ (1 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) ≀ (π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
112103, 69, 107, 110, 111syl31anc 1374 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (1 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) ≀ (π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
113102, 112eqbrtrrd 5134 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ (π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
114 hashcl 14263 . . . . . . . . . . . . 13 ((((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) ∈ Fin β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ∈ β„•0)
115 nn0re 12429 . . . . . . . . . . . . 13 ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ∈ β„•0 β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ∈ ℝ)
11677, 114, 1153syl 18 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ∈ ℝ)
117116, 71remulcld 11192 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) Β· π‘š) ∈ ℝ)
11871adantr 482 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) β†’ π‘š ∈ ℝ)
119 elfzuz 13444 . . . . . . . . . . . . . 14 (𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) β†’ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1)))
12081peano2nnd 12177 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((βŒŠβ€˜π‘) + 1) ∈ β„•)
121 eluznn 12850 . . . . . . . . . . . . . . . 16 ((((βŒŠβ€˜π‘) + 1) ∈ β„• ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑛 ∈ β„•)
122120, 121sylan 581 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑛 ∈ β„•)
123 simpllr 775 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š))
12483adantr 482 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑐 ∈ ℝ)
125 reflcl 13708 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ℝ β†’ (βŒŠβ€˜π‘) ∈ ℝ)
126 peano2re 11335 . . . . . . . . . . . . . . . . 17 ((βŒŠβ€˜π‘) ∈ ℝ β†’ ((βŒŠβ€˜π‘) + 1) ∈ ℝ)
127124, 125, 1263syl 18 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ ((βŒŠβ€˜π‘) + 1) ∈ ℝ)
128122nnred 12175 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑛 ∈ ℝ)
129 fllep1 13713 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ℝ β†’ 𝑐 ≀ ((βŒŠβ€˜π‘) + 1))
130124, 129syl 17 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑐 ≀ ((βŒŠβ€˜π‘) + 1))
131 eluzle 12783 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1)) β†’ ((βŒŠβ€˜π‘) + 1) ≀ 𝑛)
132131adantl 483 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ ((βŒŠβ€˜π‘) + 1) ≀ 𝑛)
133124, 127, 128, 130, 132letrd 11319 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑐 ≀ 𝑛)
134 nfv 1918 . . . . . . . . . . . . . . . . 17 β„²π‘˜ 𝑐 ≀ 𝑛
135 nfcv 2908 . . . . . . . . . . . . . . . . . . 19 β„²π‘˜abs
136135, 12nffv 6857 . . . . . . . . . . . . . . . . . 18 β„²π‘˜(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)
137 nfcv 2908 . . . . . . . . . . . . . . . . . 18 β„²π‘˜ ≀
138 nfcv 2908 . . . . . . . . . . . . . . . . . 18 β„²π‘˜π‘š
139136, 137, 138nfbr 5157 . . . . . . . . . . . . . . . . 17 β„²π‘˜(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š
140134, 139nfim 1900 . . . . . . . . . . . . . . . 16 β„²π‘˜(𝑐 ≀ 𝑛 β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š)
141 breq2 5114 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑛 β†’ (𝑐 ≀ π‘˜ ↔ 𝑐 ≀ 𝑛))
14213fveq2d 6851 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑛 β†’ (absβ€˜π΄) = (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
143142breq1d 5120 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑛 β†’ ((absβ€˜π΄) ≀ π‘š ↔ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š))
144141, 143imbi12d 345 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑛 β†’ ((𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š) ↔ (𝑐 ≀ 𝑛 β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š)))
145140, 144rspc 3572 . . . . . . . . . . . . . . 15 (𝑛 ∈ β„• β†’ (βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š) β†’ (𝑐 ≀ 𝑛 β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š)))
146122, 123, 133, 145syl3c 66 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š)
147119, 146sylan2 594 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š)
14877, 97, 118, 147fsumle 15691 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))π‘š)
14971recnd 11190 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ π‘š ∈ β„‚)
150 fsumconst 15682 . . . . . . . . . . . . 13 (((((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) ∈ Fin ∧ π‘š ∈ β„‚) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))π‘š = ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) Β· π‘š))
15177, 149, 150syl2anc 585 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))π‘š = ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) Β· π‘š))
152148, 151breqtrd 5136 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) Β· π‘š))
153 biidd 262 . . . . . . . . . . . . 13 (𝑛 = ((βŒŠβ€˜π‘) + 1) β†’ (0 ≀ π‘š ↔ 0 ≀ π‘š))
154 0red 11165 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 0 ∈ ℝ)
15547, 30mpan9 508 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ β„•) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
156155adantlr 714 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ β„•) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
157122, 156syldan 592 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
158157abscld 15328 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
15971adantr 482 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ π‘š ∈ ℝ)
160157absge0d 15336 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 0 ≀ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
161154, 158, 159, 160, 146letrd 11319 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 0 ≀ π‘š)
162161ralrimiva 3144 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ βˆ€π‘› ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))0 ≀ π‘š)
163120nnzd 12533 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((βŒŠβ€˜π‘) + 1) ∈ β„€)
164 uzid 12785 . . . . . . . . . . . . . 14 (((βŒŠβ€˜π‘) + 1) ∈ β„€ β†’ ((βŒŠβ€˜π‘) + 1) ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1)))
165163, 164syl 17 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((βŒŠβ€˜π‘) + 1) ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1)))
166153, 162, 165rspcdva 3585 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 0 ≀ π‘š)
167 reflcl 13708 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ (βŒŠβ€˜π‘₯) ∈ ℝ)
16869, 167syl 17 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘₯) ∈ ℝ)
169 ssdomg 8947 . . . . . . . . . . . . . . . 16 ((1...(βŒŠβ€˜π‘₯)) ∈ Fin β†’ ((((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) βŠ† (1...(βŒŠβ€˜π‘₯)) β†’ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) β‰Ό (1...(βŒŠβ€˜π‘₯))))
17064, 93, 169sylc 65 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) β‰Ό (1...(βŒŠβ€˜π‘₯)))
171 hashdomi 14287 . . . . . . . . . . . . . . 15 ((((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) β‰Ό (1...(βŒŠβ€˜π‘₯)) β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ≀ (β™―β€˜(1...(βŒŠβ€˜π‘₯))))
172170, 171syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ≀ (β™―β€˜(1...(βŒŠβ€˜π‘₯))))
173 flge0nn0 13732 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯) β†’ (βŒŠβ€˜π‘₯) ∈ β„•0)
174 hashfz1 14253 . . . . . . . . . . . . . . 15 ((βŒŠβ€˜π‘₯) ∈ β„•0 β†’ (β™―β€˜(1...(βŒŠβ€˜π‘₯))) = (βŒŠβ€˜π‘₯))
17557, 173, 1743syl 18 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (β™―β€˜(1...(βŒŠβ€˜π‘₯))) = (βŒŠβ€˜π‘₯))
176172, 175breqtrd 5136 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ≀ (βŒŠβ€˜π‘₯))
177 flle 13711 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ (βŒŠβ€˜π‘₯) ≀ π‘₯)
17869, 177syl 17 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘₯) ≀ π‘₯)
179116, 168, 69, 176, 178letrd 11319 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ≀ π‘₯)
180116, 69, 71, 166, 179lemul1ad 12101 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) Β· π‘š) ≀ (π‘₯ Β· π‘š))
18198, 117, 100, 152, 180letrd 11319 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ (π‘₯ Β· π‘š))
18270, 98, 99, 100, 113, 181le2addd 11781 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) ≀ ((π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) + (π‘₯ Β· π‘š)))
183 ltp1 12002 . . . . . . . . . . 11 ((βŒŠβ€˜π‘) ∈ ℝ β†’ (βŒŠβ€˜π‘) < ((βŒŠβ€˜π‘) + 1))
184 fzdisj 13475 . . . . . . . . . . 11 ((βŒŠβ€˜π‘) < ((βŒŠβ€˜π‘) + 1) β†’ ((1...(βŒŠβ€˜π‘)) ∩ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) = βˆ…)
18582, 183, 1843syl 18 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((1...(βŒŠβ€˜π‘)) ∩ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) = βˆ…)
18696recnd 11190 . . . . . . . . . 10 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ β„‚)
187185, 92, 64, 186fsumsplit 15633 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) = (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
18836adantrr 716 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ π‘₯ ∈ β„‚)
189188, 101, 149adddid 11186 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š)) = ((π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) + (π‘₯ Β· π‘š)))
190182, 187, 1893brtr4d 5142 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š)))
19163, 68, 73, 76, 190letrd 11319 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ≀ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š)))
192 rpregt0 12936 . . . . . . . . 9 (π‘₯ ∈ ℝ+ β†’ (π‘₯ ∈ ℝ ∧ 0 < π‘₯))
193192ad2antrl 727 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ ∈ ℝ ∧ 0 < π‘₯))
194 ledivmul 12038 . . . . . . . 8 (((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ∈ ℝ ∧ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š) ∈ ℝ ∧ (π‘₯ ∈ ℝ ∧ 0 < π‘₯)) β†’ (((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / π‘₯) ≀ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š) ↔ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ≀ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š))))
19563, 72, 193, 194syl3anc 1372 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / π‘₯) ≀ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š) ↔ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ≀ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š))))
196191, 195mpbird 257 . . . . . 6 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / π‘₯) ≀ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š))
19761, 196eqbrtrd 5132 . . . . 5 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) ≀ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š))
19810, 39, 45, 53, 197elo1d 15425 . . . 4 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) ∈ 𝑂(1))
199198ex 414 . . 3 ((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) β†’ (βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š) β†’ (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) ∈ 𝑂(1)))
200199rexlimdvva 3206 . 2 (πœ‘ β†’ (βˆƒπ‘ ∈ (1[,)+∞)βˆƒπ‘š ∈ ℝ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š) β†’ (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) ∈ 𝑂(1)))
2018, 200mpd 15 1 (πœ‘ β†’ (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) ∈ 𝑂(1))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  β¦‹csb 3860   βˆͺ cun 3913   ∩ cin 3914   βŠ† wss 3915  βˆ…c0 4287   class class class wbr 5110   ↦ cmpt 5193  dom cdm 5638  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362   β‰Ό cdom 8888  Fincfn 8890  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063  +∞cpnf 11193   < clt 11196   ≀ cle 11197   / cdiv 11819  β„•cn 12160  β„•0cn0 12420  β„€cz 12506  β„€β‰₯cuz 12770  β„+crp 12922  [,)cico 13273  ...cfz 13431  βŒŠcfl 13702  β™―chash 14237  abscabs 15126  π‘‚(1)co1 15375  Ξ£csu 15577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-oadd 8421  df-er 8655  df-pm 8775  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-inf 9386  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-xnn0 12493  df-z 12507  df-uz 12771  df-rp 12923  df-ico 13277  df-fz 13432  df-fzo 13575  df-fl 13704  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-clim 15377  df-o1 15379  df-lo1 15380  df-sum 15578
This theorem is referenced by:  selberg2lem  26914
  Copyright terms: Public domain W3C validator