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

Theorem o1fsum 15763
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 12220 . . . . 5 β„• βŠ† ℝ
32a1i 11 . . . 4 (πœ‘ β†’ β„• βŠ† ℝ)
4 o1fsum.1 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐴 ∈ 𝑉)
54, 1o1mptrcl 15571 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐴 ∈ β„‚)
6 1red 11219 . . . 4 (πœ‘ β†’ 1 ∈ ℝ)
73, 5, 6elo1mpt2 15483 . . 3 (πœ‘ β†’ ((π‘˜ ∈ β„• ↦ 𝐴) ∈ 𝑂(1) ↔ βˆƒπ‘ ∈ (1[,)+∞)βˆƒπ‘š ∈ ℝ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)))
81, 7mpbid 231 . 2 (πœ‘ β†’ βˆƒπ‘ ∈ (1[,)+∞)βˆƒπ‘š ∈ ℝ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š))
9 rpssre 12985 . . . . . 6 ℝ+ βŠ† ℝ
109a1i 11 . . . . 5 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ ℝ+ βŠ† ℝ)
11 nfcv 2901 . . . . . . . 8 Ⅎ𝑛𝐴
12 nfcsb1v 3917 . . . . . . . 8 β„²π‘˜β¦‹π‘› / π‘˜β¦Œπ΄
13 csbeq1a 3906 . . . . . . . 8 (π‘˜ = 𝑛 β†’ 𝐴 = ⦋𝑛 / π‘˜β¦Œπ΄)
1411, 12, 13cbvsumi 15647 . . . . . . 7 Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))⦋𝑛 / π‘˜β¦Œπ΄
15 fzfid 13942 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ (1...(βŒŠβ€˜π‘₯)) ∈ Fin)
16 o1f 15477 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„• ↦ 𝐴) ∈ 𝑂(1) β†’ (π‘˜ ∈ β„• ↦ 𝐴):dom (π‘˜ ∈ β„• ↦ 𝐴)βŸΆβ„‚)
171, 16syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘˜ ∈ β„• ↦ 𝐴):dom (π‘˜ ∈ β„• ↦ 𝐴)βŸΆβ„‚)
184ralrimiva 3144 . . . . . . . . . . . . . 14 (πœ‘ β†’ βˆ€π‘˜ ∈ β„• 𝐴 ∈ 𝑉)
19 dmmptg 6240 . . . . . . . . . . . . . 14 (βˆ€π‘˜ ∈ β„• 𝐴 ∈ 𝑉 β†’ dom (π‘˜ ∈ β„• ↦ 𝐴) = β„•)
2018, 19syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ dom (π‘˜ ∈ β„• ↦ 𝐴) = β„•)
2120feq2d 6702 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘˜ ∈ β„• ↦ 𝐴):dom (π‘˜ ∈ β„• ↦ 𝐴)βŸΆβ„‚ ↔ (π‘˜ ∈ β„• ↦ 𝐴):β„•βŸΆβ„‚))
2217, 21mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ (π‘˜ ∈ β„• ↦ 𝐴):β„•βŸΆβ„‚)
23 eqid 2730 . . . . . . . . . . . 12 (π‘˜ ∈ β„• ↦ 𝐴) = (π‘˜ ∈ β„• ↦ 𝐴)
2423fmpt 7110 . . . . . . . . . . 11 (βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚ ↔ (π‘˜ ∈ β„• ↦ 𝐴):β„•βŸΆβ„‚)
2522, 24sylibr 233 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚)
2625ad3antrrr 726 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚)
27 elfznn 13534 . . . . . . . . 9 (𝑛 ∈ (1...(βŒŠβ€˜π‘₯)) β†’ 𝑛 ∈ β„•)
2812nfel1 2917 . . . . . . . . . . 11 β„²π‘˜β¦‹π‘› / π‘˜β¦Œπ΄ ∈ β„‚
2913eleq1d 2816 . . . . . . . . . . 11 (π‘˜ = 𝑛 β†’ (𝐴 ∈ β„‚ ↔ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚))
3028, 29rspc 3599 . . . . . . . . . 10 (𝑛 ∈ β„• β†’ (βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚ β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚))
3130impcom 406 . . . . . . . . 9 ((βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚ ∧ 𝑛 ∈ β„•) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
3226, 27, 31syl2an 594 . . . . . . . 8 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
3315, 32fsumcl 15683 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
3414, 33eqeltrid 2835 . . . . . 6 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 ∈ β„‚)
35 rpcn 12988 . . . . . . 7 (π‘₯ ∈ ℝ+ β†’ π‘₯ ∈ β„‚)
3635adantl 480 . . . . . 6 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ π‘₯ ∈ β„‚)
37 rpne0 12994 . . . . . . 7 (π‘₯ ∈ ℝ+ β†’ π‘₯ β‰  0)
3837adantl 480 . . . . . 6 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ π‘₯ β‰  0)
3934, 36, 38divcld 11994 . . . . 5 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯) ∈ β„‚)
40 simplrl 773 . . . . . . 7 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ 𝑐 ∈ (1[,)+∞))
41 1re 11218 . . . . . . . 8 1 ∈ ℝ
42 elicopnf 13426 . . . . . . . 8 (1 ∈ ℝ β†’ (𝑐 ∈ (1[,)+∞) ↔ (𝑐 ∈ ℝ ∧ 1 ≀ 𝑐)))
4341, 42ax-mp 5 . . . . . . 7 (𝑐 ∈ (1[,)+∞) ↔ (𝑐 ∈ ℝ ∧ 1 ≀ 𝑐))
4440, 43sylib 217 . . . . . 6 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (𝑐 ∈ ℝ ∧ 1 ≀ 𝑐))
4544simpld 493 . . . . 5 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ 𝑐 ∈ ℝ)
46 fzfid 13942 . . . . . . 7 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (1...(βŒŠβ€˜π‘)) ∈ Fin)
4725ad2antrr 722 . . . . . . . . 9 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚)
48 elfznn 13534 . . . . . . . . 9 (𝑛 ∈ (1...(βŒŠβ€˜π‘)) β†’ 𝑛 ∈ β„•)
4947, 48, 31syl2an 594 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘))) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
5049abscld 15387 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
5146, 50fsumrecl 15684 . . . . . 6 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
52 simplrr 774 . . . . . 6 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ π‘š ∈ ℝ)
5351, 52readdcld 11247 . . . . 5 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š) ∈ ℝ)
5434, 36, 38absdivd 15406 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) = ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / (absβ€˜π‘₯)))
5554adantrr 713 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) = ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / (absβ€˜π‘₯)))
56 rprege0 12993 . . . . . . . . . 10 (π‘₯ ∈ ℝ+ β†’ (π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯))
5756ad2antrl 724 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯))
58 absid 15247 . . . . . . . . 9 ((π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯) β†’ (absβ€˜π‘₯) = π‘₯)
5957, 58syl 17 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜π‘₯) = π‘₯)
6059oveq2d 7427 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / (absβ€˜π‘₯)) = ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / π‘₯))
6155, 60eqtrd 2770 . . . . . 6 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) = ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / π‘₯))
6234adantrr 713 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 ∈ β„‚)
6362abscld 15387 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ∈ ℝ)
64 fzfid 13942 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (1...(βŒŠβ€˜π‘₯)) ∈ Fin)
6547, 27, 31syl2an 594 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
6665adantlr 711 . . . . . . . . . 10 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
6766abscld 15387 . . . . . . . . 9 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
6864, 67fsumrecl 15684 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
6957simpld 493 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ π‘₯ ∈ ℝ)
7051adantr 479 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
7152adantr 479 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ π‘š ∈ ℝ)
7270, 71readdcld 11247 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š) ∈ ℝ)
7369, 72remulcld 11248 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š)) ∈ ℝ)
7414fveq2i 6893 . . . . . . . . 9 (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) = (absβ€˜Ξ£π‘› ∈ (1...(βŒŠβ€˜π‘₯))⦋𝑛 / π‘˜β¦Œπ΄)
7564, 66fsumabs 15751 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜Ξ£π‘› ∈ (1...(βŒŠβ€˜π‘₯))⦋𝑛 / π‘˜β¦Œπ΄) ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
7674, 75eqbrtrid 5182 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
77 fzfid 13942 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) ∈ Fin)
78 ssun2 4172 . . . . . . . . . . . . . 14 (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) βŠ† ((1...(βŒŠβ€˜π‘)) βˆͺ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)))
79 flge1nn 13790 . . . . . . . . . . . . . . . . . 18 ((𝑐 ∈ ℝ ∧ 1 ≀ 𝑐) β†’ (βŒŠβ€˜π‘) ∈ β„•)
8044, 79syl 17 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (βŒŠβ€˜π‘) ∈ β„•)
8180adantr 479 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘) ∈ β„•)
8281nnred 12231 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘) ∈ ℝ)
8345adantr 479 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 𝑐 ∈ ℝ)
84 flle 13768 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ ℝ β†’ (βŒŠβ€˜π‘) ≀ 𝑐)
8583, 84syl 17 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘) ≀ 𝑐)
86 simprr 769 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 𝑐 ≀ π‘₯)
8782, 83, 69, 85, 86letrd 11375 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘) ≀ π‘₯)
88 fznnfl 13831 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ ℝ β†’ ((βŒŠβ€˜π‘) ∈ (1...(βŒŠβ€˜π‘₯)) ↔ ((βŒŠβ€˜π‘) ∈ β„• ∧ (βŒŠβ€˜π‘) ≀ π‘₯)))
8969, 88syl 17 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((βŒŠβ€˜π‘) ∈ (1...(βŒŠβ€˜π‘₯)) ↔ ((βŒŠβ€˜π‘) ∈ β„• ∧ (βŒŠβ€˜π‘) ≀ π‘₯)))
9081, 87, 89mpbir2and 709 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘) ∈ (1...(βŒŠβ€˜π‘₯)))
91 fzsplit 13531 . . . . . . . . . . . . . . 15 ((βŒŠβ€˜π‘) ∈ (1...(βŒŠβ€˜π‘₯)) β†’ (1...(βŒŠβ€˜π‘₯)) = ((1...(βŒŠβ€˜π‘)) βˆͺ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))))
9290, 91syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (1...(βŒŠβ€˜π‘₯)) = ((1...(βŒŠβ€˜π‘)) βˆͺ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))))
9378, 92sseqtrrid 4034 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) βŠ† (1...(βŒŠβ€˜π‘₯)))
9493sselda 3981 . . . . . . . . . . . 12 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯)))
9565abscld 15387 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
9695adantlr 711 . . . . . . . . . . . 12 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
9794, 96syldan 589 . . . . . . . . . . 11 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
9877, 97fsumrecl 15684 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
9969, 70remulcld 11248 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) ∈ ℝ)
10069, 71remulcld 11248 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ Β· π‘š) ∈ ℝ)
10170recnd 11246 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ β„‚)
102101mullidd 11236 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (1 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
103 1red 11219 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 1 ∈ ℝ)
10449absge0d 15395 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘))) β†’ 0 ≀ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
10546, 50, 104fsumge0 15745 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ 0 ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
10651, 105jca 510 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ ∧ 0 ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
107106adantr 479 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ ∧ 0 ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
10844simprd 494 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ 1 ≀ 𝑐)
109108adantr 479 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 1 ≀ 𝑐)
110103, 83, 69, 109, 86letrd 11375 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 1 ≀ π‘₯)
111 lemul1a 12072 . . . . . . . . . . . 12 (((1 ∈ ℝ ∧ π‘₯ ∈ ℝ ∧ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ ∧ 0 ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))) ∧ 1 ≀ π‘₯) β†’ (1 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) ≀ (π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
112103, 69, 107, 110, 111syl31anc 1371 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (1 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) ≀ (π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
113102, 112eqbrtrrd 5171 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ (π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
114 hashcl 14320 . . . . . . . . . . . . 13 ((((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) ∈ Fin β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ∈ β„•0)
115 nn0re 12485 . . . . . . . . . . . . 13 ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ∈ β„•0 β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ∈ ℝ)
11677, 114, 1153syl 18 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ∈ ℝ)
117116, 71remulcld 11248 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) Β· π‘š) ∈ ℝ)
11871adantr 479 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) β†’ π‘š ∈ ℝ)
119 elfzuz 13501 . . . . . . . . . . . . . 14 (𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) β†’ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1)))
12081peano2nnd 12233 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((βŒŠβ€˜π‘) + 1) ∈ β„•)
121 eluznn 12906 . . . . . . . . . . . . . . . 16 ((((βŒŠβ€˜π‘) + 1) ∈ β„• ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑛 ∈ β„•)
122120, 121sylan 578 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑛 ∈ β„•)
123 simpllr 772 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š))
12483adantr 479 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑐 ∈ ℝ)
125 reflcl 13765 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ℝ β†’ (βŒŠβ€˜π‘) ∈ ℝ)
126 peano2re 11391 . . . . . . . . . . . . . . . . 17 ((βŒŠβ€˜π‘) ∈ ℝ β†’ ((βŒŠβ€˜π‘) + 1) ∈ ℝ)
127124, 125, 1263syl 18 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ ((βŒŠβ€˜π‘) + 1) ∈ ℝ)
128122nnred 12231 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑛 ∈ ℝ)
129 fllep1 13770 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ℝ β†’ 𝑐 ≀ ((βŒŠβ€˜π‘) + 1))
130124, 129syl 17 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑐 ≀ ((βŒŠβ€˜π‘) + 1))
131 eluzle 12839 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1)) β†’ ((βŒŠβ€˜π‘) + 1) ≀ 𝑛)
132131adantl 480 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ ((βŒŠβ€˜π‘) + 1) ≀ 𝑛)
133124, 127, 128, 130, 132letrd 11375 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑐 ≀ 𝑛)
134 nfv 1915 . . . . . . . . . . . . . . . . 17 β„²π‘˜ 𝑐 ≀ 𝑛
135 nfcv 2901 . . . . . . . . . . . . . . . . . . 19 β„²π‘˜abs
136135, 12nffv 6900 . . . . . . . . . . . . . . . . . 18 β„²π‘˜(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)
137 nfcv 2901 . . . . . . . . . . . . . . . . . 18 β„²π‘˜ ≀
138 nfcv 2901 . . . . . . . . . . . . . . . . . 18 β„²π‘˜π‘š
139136, 137, 138nfbr 5194 . . . . . . . . . . . . . . . . 17 β„²π‘˜(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š
140134, 139nfim 1897 . . . . . . . . . . . . . . . 16 β„²π‘˜(𝑐 ≀ 𝑛 β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š)
141 breq2 5151 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑛 β†’ (𝑐 ≀ π‘˜ ↔ 𝑐 ≀ 𝑛))
14213fveq2d 6894 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑛 β†’ (absβ€˜π΄) = (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
143142breq1d 5157 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑛 β†’ ((absβ€˜π΄) ≀ π‘š ↔ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š))
144141, 143imbi12d 343 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑛 β†’ ((𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š) ↔ (𝑐 ≀ 𝑛 β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š)))
145140, 144rspc 3599 . . . . . . . . . . . . . . 15 (𝑛 ∈ β„• β†’ (βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š) β†’ (𝑐 ≀ 𝑛 β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š)))
146122, 123, 133, 145syl3c 66 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š)
147119, 146sylan2 591 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š)
14877, 97, 118, 147fsumle 15749 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))π‘š)
14971recnd 11246 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ π‘š ∈ β„‚)
150 fsumconst 15740 . . . . . . . . . . . . 13 (((((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) ∈ Fin ∧ π‘š ∈ β„‚) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))π‘š = ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) Β· π‘š))
15177, 149, 150syl2anc 582 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))π‘š = ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) Β· π‘š))
152148, 151breqtrd 5173 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) Β· π‘š))
153 biidd 261 . . . . . . . . . . . . 13 (𝑛 = ((βŒŠβ€˜π‘) + 1) β†’ (0 ≀ π‘š ↔ 0 ≀ π‘š))
154 0red 11221 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 0 ∈ ℝ)
15547, 30mpan9 505 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ β„•) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
156155adantlr 711 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ β„•) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
157122, 156syldan 589 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
158157abscld 15387 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
15971adantr 479 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ π‘š ∈ ℝ)
160157absge0d 15395 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 0 ≀ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
161154, 158, 159, 160, 146letrd 11375 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 0 ≀ π‘š)
162161ralrimiva 3144 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ βˆ€π‘› ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))0 ≀ π‘š)
163120nnzd 12589 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((βŒŠβ€˜π‘) + 1) ∈ β„€)
164 uzid 12841 . . . . . . . . . . . . . 14 (((βŒŠβ€˜π‘) + 1) ∈ β„€ β†’ ((βŒŠβ€˜π‘) + 1) ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1)))
165163, 164syl 17 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((βŒŠβ€˜π‘) + 1) ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1)))
166153, 162, 165rspcdva 3612 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 0 ≀ π‘š)
167 reflcl 13765 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ (βŒŠβ€˜π‘₯) ∈ ℝ)
16869, 167syl 17 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘₯) ∈ ℝ)
169 ssdomg 8998 . . . . . . . . . . . . . . . 16 ((1...(βŒŠβ€˜π‘₯)) ∈ Fin β†’ ((((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) βŠ† (1...(βŒŠβ€˜π‘₯)) β†’ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) β‰Ό (1...(βŒŠβ€˜π‘₯))))
17064, 93, 169sylc 65 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) β‰Ό (1...(βŒŠβ€˜π‘₯)))
171 hashdomi 14344 . . . . . . . . . . . . . . 15 ((((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) β‰Ό (1...(βŒŠβ€˜π‘₯)) β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ≀ (β™―β€˜(1...(βŒŠβ€˜π‘₯))))
172170, 171syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ≀ (β™―β€˜(1...(βŒŠβ€˜π‘₯))))
173 flge0nn0 13789 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯) β†’ (βŒŠβ€˜π‘₯) ∈ β„•0)
174 hashfz1 14310 . . . . . . . . . . . . . . 15 ((βŒŠβ€˜π‘₯) ∈ β„•0 β†’ (β™―β€˜(1...(βŒŠβ€˜π‘₯))) = (βŒŠβ€˜π‘₯))
17557, 173, 1743syl 18 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (β™―β€˜(1...(βŒŠβ€˜π‘₯))) = (βŒŠβ€˜π‘₯))
176172, 175breqtrd 5173 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ≀ (βŒŠβ€˜π‘₯))
177 flle 13768 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ (βŒŠβ€˜π‘₯) ≀ π‘₯)
17869, 177syl 17 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘₯) ≀ π‘₯)
179116, 168, 69, 176, 178letrd 11375 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ≀ π‘₯)
180116, 69, 71, 166, 179lemul1ad 12157 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) Β· π‘š) ≀ (π‘₯ Β· π‘š))
18198, 117, 100, 152, 180letrd 11375 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ (π‘₯ Β· π‘š))
18270, 98, 99, 100, 113, 181le2addd 11837 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) ≀ ((π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) + (π‘₯ Β· π‘š)))
183 ltp1 12058 . . . . . . . . . . 11 ((βŒŠβ€˜π‘) ∈ ℝ β†’ (βŒŠβ€˜π‘) < ((βŒŠβ€˜π‘) + 1))
184 fzdisj 13532 . . . . . . . . . . 11 ((βŒŠβ€˜π‘) < ((βŒŠβ€˜π‘) + 1) β†’ ((1...(βŒŠβ€˜π‘)) ∩ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) = βˆ…)
18582, 183, 1843syl 18 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((1...(βŒŠβ€˜π‘)) ∩ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) = βˆ…)
18696recnd 11246 . . . . . . . . . 10 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ β„‚)
187185, 92, 64, 186fsumsplit 15691 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) = (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
18836adantrr 713 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ π‘₯ ∈ β„‚)
189188, 101, 149adddid 11242 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š)) = ((π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) + (π‘₯ Β· π‘š)))
190182, 187, 1893brtr4d 5179 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š)))
19163, 68, 73, 76, 190letrd 11375 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ≀ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š)))
192 rpregt0 12992 . . . . . . . . 9 (π‘₯ ∈ ℝ+ β†’ (π‘₯ ∈ ℝ ∧ 0 < π‘₯))
193192ad2antrl 724 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ ∈ ℝ ∧ 0 < π‘₯))
194 ledivmul 12094 . . . . . . . 8 (((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ∈ ℝ ∧ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š) ∈ ℝ ∧ (π‘₯ ∈ ℝ ∧ 0 < π‘₯)) β†’ (((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / π‘₯) ≀ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š) ↔ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ≀ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š))))
19563, 72, 193, 194syl3anc 1369 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / π‘₯) ≀ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š) ↔ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ≀ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š))))
196191, 195mpbird 256 . . . . . 6 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / π‘₯) ≀ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š))
19761, 196eqbrtrd 5169 . . . . 5 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) ≀ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š))
19810, 39, 45, 53, 197elo1d 15484 . . . 4 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) ∈ 𝑂(1))
199198ex 411 . . 3 ((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) β†’ (βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š) β†’ (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) ∈ 𝑂(1)))
200199rexlimdvva 3209 . 2 (πœ‘ β†’ (βˆƒπ‘ ∈ (1[,)+∞)βˆƒπ‘š ∈ ℝ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š) β†’ (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) ∈ 𝑂(1)))
2018, 200mpd 15 1 (πœ‘ β†’ (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) ∈ 𝑂(1))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  βˆƒwrex 3068  β¦‹csb 3892   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321   class class class wbr 5147   ↦ cmpt 5230  dom cdm 5675  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411   β‰Ό cdom 8939  Fincfn 8941  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117  +∞cpnf 11249   < clt 11252   ≀ cle 11253   / cdiv 11875  β„•cn 12216  β„•0cn0 12476  β„€cz 12562  β„€β‰₯cuz 12826  β„+crp 12978  [,)cico 13330  ...cfz 13488  βŒŠcfl 13759  β™―chash 14294  abscabs 15185  π‘‚(1)co1 15434  Ξ£csu 15636
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-er 8705  df-pm 8825  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-oi 9507  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-xnn0 12549  df-z 12563  df-uz 12827  df-rp 12979  df-ico 13334  df-fz 13489  df-fzo 13632  df-fl 13761  df-seq 13971  df-exp 14032  df-hash 14295  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-clim 15436  df-o1 15438  df-lo1 15439  df-sum 15637
This theorem is referenced by:  selberg2lem  27289
  Copyright terms: Public domain W3C validator