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

Theorem o1fsum 15758
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 12215 . . . . 5 β„• βŠ† ℝ
32a1i 11 . . . 4 (πœ‘ β†’ β„• βŠ† ℝ)
4 o1fsum.1 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐴 ∈ 𝑉)
54, 1o1mptrcl 15566 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐴 ∈ β„‚)
6 1red 11214 . . . 4 (πœ‘ β†’ 1 ∈ ℝ)
73, 5, 6elo1mpt2 15478 . . 3 (πœ‘ β†’ ((π‘˜ ∈ β„• ↦ 𝐴) ∈ 𝑂(1) ↔ βˆƒπ‘ ∈ (1[,)+∞)βˆƒπ‘š ∈ ℝ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)))
81, 7mpbid 231 . 2 (πœ‘ β†’ βˆƒπ‘ ∈ (1[,)+∞)βˆƒπ‘š ∈ ℝ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š))
9 rpssre 12980 . . . . . 6 ℝ+ βŠ† ℝ
109a1i 11 . . . . 5 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ ℝ+ βŠ† ℝ)
11 nfcv 2903 . . . . . . . 8 Ⅎ𝑛𝐴
12 nfcsb1v 3918 . . . . . . . 8 β„²π‘˜β¦‹π‘› / π‘˜β¦Œπ΄
13 csbeq1a 3907 . . . . . . . 8 (π‘˜ = 𝑛 β†’ 𝐴 = ⦋𝑛 / π‘˜β¦Œπ΄)
1411, 12, 13cbvsumi 15642 . . . . . . 7 Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))⦋𝑛 / π‘˜β¦Œπ΄
15 fzfid 13937 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ (1...(βŒŠβ€˜π‘₯)) ∈ Fin)
16 o1f 15472 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„• ↦ 𝐴) ∈ 𝑂(1) β†’ (π‘˜ ∈ β„• ↦ 𝐴):dom (π‘˜ ∈ β„• ↦ 𝐴)βŸΆβ„‚)
171, 16syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘˜ ∈ β„• ↦ 𝐴):dom (π‘˜ ∈ β„• ↦ 𝐴)βŸΆβ„‚)
184ralrimiva 3146 . . . . . . . . . . . . . 14 (πœ‘ β†’ βˆ€π‘˜ ∈ β„• 𝐴 ∈ 𝑉)
19 dmmptg 6241 . . . . . . . . . . . . . 14 (βˆ€π‘˜ ∈ β„• 𝐴 ∈ 𝑉 β†’ dom (π‘˜ ∈ β„• ↦ 𝐴) = β„•)
2018, 19syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ dom (π‘˜ ∈ β„• ↦ 𝐴) = β„•)
2120feq2d 6703 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘˜ ∈ β„• ↦ 𝐴):dom (π‘˜ ∈ β„• ↦ 𝐴)βŸΆβ„‚ ↔ (π‘˜ ∈ β„• ↦ 𝐴):β„•βŸΆβ„‚))
2217, 21mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ (π‘˜ ∈ β„• ↦ 𝐴):β„•βŸΆβ„‚)
23 eqid 2732 . . . . . . . . . . . 12 (π‘˜ ∈ β„• ↦ 𝐴) = (π‘˜ ∈ β„• ↦ 𝐴)
2423fmpt 7109 . . . . . . . . . . 11 (βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚ ↔ (π‘˜ ∈ β„• ↦ 𝐴):β„•βŸΆβ„‚)
2522, 24sylibr 233 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚)
2625ad3antrrr 728 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚)
27 elfznn 13529 . . . . . . . . 9 (𝑛 ∈ (1...(βŒŠβ€˜π‘₯)) β†’ 𝑛 ∈ β„•)
2812nfel1 2919 . . . . . . . . . . 11 β„²π‘˜β¦‹π‘› / π‘˜β¦Œπ΄ ∈ β„‚
2913eleq1d 2818 . . . . . . . . . . 11 (π‘˜ = 𝑛 β†’ (𝐴 ∈ β„‚ ↔ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚))
3028, 29rspc 3600 . . . . . . . . . 10 (𝑛 ∈ β„• β†’ (βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚ β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚))
3130impcom 408 . . . . . . . . 9 ((βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚ ∧ 𝑛 ∈ β„•) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
3226, 27, 31syl2an 596 . . . . . . . 8 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
3315, 32fsumcl 15678 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
3414, 33eqeltrid 2837 . . . . . 6 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 ∈ β„‚)
35 rpcn 12983 . . . . . . 7 (π‘₯ ∈ ℝ+ β†’ π‘₯ ∈ β„‚)
3635adantl 482 . . . . . 6 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ π‘₯ ∈ β„‚)
37 rpne0 12989 . . . . . . 7 (π‘₯ ∈ ℝ+ β†’ π‘₯ β‰  0)
3837adantl 482 . . . . . 6 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ π‘₯ β‰  0)
3934, 36, 38divcld 11989 . . . . 5 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯) ∈ β„‚)
40 simplrl 775 . . . . . . 7 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ 𝑐 ∈ (1[,)+∞))
41 1re 11213 . . . . . . . 8 1 ∈ ℝ
42 elicopnf 13421 . . . . . . . 8 (1 ∈ ℝ β†’ (𝑐 ∈ (1[,)+∞) ↔ (𝑐 ∈ ℝ ∧ 1 ≀ 𝑐)))
4341, 42ax-mp 5 . . . . . . 7 (𝑐 ∈ (1[,)+∞) ↔ (𝑐 ∈ ℝ ∧ 1 ≀ 𝑐))
4440, 43sylib 217 . . . . . 6 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (𝑐 ∈ ℝ ∧ 1 ≀ 𝑐))
4544simpld 495 . . . . 5 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ 𝑐 ∈ ℝ)
46 fzfid 13937 . . . . . . 7 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (1...(βŒŠβ€˜π‘)) ∈ Fin)
4725ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ βˆ€π‘˜ ∈ β„• 𝐴 ∈ β„‚)
48 elfznn 13529 . . . . . . . . 9 (𝑛 ∈ (1...(βŒŠβ€˜π‘)) β†’ 𝑛 ∈ β„•)
4947, 48, 31syl2an 596 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘))) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
5049abscld 15382 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
5146, 50fsumrecl 15679 . . . . . 6 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
52 simplrr 776 . . . . . 6 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ π‘š ∈ ℝ)
5351, 52readdcld 11242 . . . . 5 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š) ∈ ℝ)
5434, 36, 38absdivd 15401 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ π‘₯ ∈ ℝ+) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) = ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / (absβ€˜π‘₯)))
5554adantrr 715 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) = ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / (absβ€˜π‘₯)))
56 rprege0 12988 . . . . . . . . . 10 (π‘₯ ∈ ℝ+ β†’ (π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯))
5756ad2antrl 726 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯))
58 absid 15242 . . . . . . . . 9 ((π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯) β†’ (absβ€˜π‘₯) = π‘₯)
5957, 58syl 17 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜π‘₯) = π‘₯)
6059oveq2d 7424 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / (absβ€˜π‘₯)) = ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / π‘₯))
6155, 60eqtrd 2772 . . . . . 6 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) = ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / π‘₯))
6234adantrr 715 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 ∈ β„‚)
6362abscld 15382 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ∈ ℝ)
64 fzfid 13937 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (1...(βŒŠβ€˜π‘₯)) ∈ Fin)
6547, 27, 31syl2an 596 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
6665adantlr 713 . . . . . . . . . 10 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
6766abscld 15382 . . . . . . . . 9 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
6864, 67fsumrecl 15679 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
6957simpld 495 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ π‘₯ ∈ ℝ)
7051adantr 481 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
7152adantr 481 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ π‘š ∈ ℝ)
7270, 71readdcld 11242 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š) ∈ ℝ)
7369, 72remulcld 11243 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š)) ∈ ℝ)
7414fveq2i 6894 . . . . . . . . 9 (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) = (absβ€˜Ξ£π‘› ∈ (1...(βŒŠβ€˜π‘₯))⦋𝑛 / π‘˜β¦Œπ΄)
7564, 66fsumabs 15746 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜Ξ£π‘› ∈ (1...(βŒŠβ€˜π‘₯))⦋𝑛 / π‘˜β¦Œπ΄) ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
7674, 75eqbrtrid 5183 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
77 fzfid 13937 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) ∈ Fin)
78 ssun2 4173 . . . . . . . . . . . . . 14 (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) βŠ† ((1...(βŒŠβ€˜π‘)) βˆͺ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)))
79 flge1nn 13785 . . . . . . . . . . . . . . . . . 18 ((𝑐 ∈ ℝ ∧ 1 ≀ 𝑐) β†’ (βŒŠβ€˜π‘) ∈ β„•)
8044, 79syl 17 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (βŒŠβ€˜π‘) ∈ β„•)
8180adantr 481 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘) ∈ β„•)
8281nnred 12226 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘) ∈ ℝ)
8345adantr 481 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 𝑐 ∈ ℝ)
84 flle 13763 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ ℝ β†’ (βŒŠβ€˜π‘) ≀ 𝑐)
8583, 84syl 17 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘) ≀ 𝑐)
86 simprr 771 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 𝑐 ≀ π‘₯)
8782, 83, 69, 85, 86letrd 11370 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘) ≀ π‘₯)
88 fznnfl 13826 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ ℝ β†’ ((βŒŠβ€˜π‘) ∈ (1...(βŒŠβ€˜π‘₯)) ↔ ((βŒŠβ€˜π‘) ∈ β„• ∧ (βŒŠβ€˜π‘) ≀ π‘₯)))
8969, 88syl 17 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((βŒŠβ€˜π‘) ∈ (1...(βŒŠβ€˜π‘₯)) ↔ ((βŒŠβ€˜π‘) ∈ β„• ∧ (βŒŠβ€˜π‘) ≀ π‘₯)))
9081, 87, 89mpbir2and 711 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘) ∈ (1...(βŒŠβ€˜π‘₯)))
91 fzsplit 13526 . . . . . . . . . . . . . . 15 ((βŒŠβ€˜π‘) ∈ (1...(βŒŠβ€˜π‘₯)) β†’ (1...(βŒŠβ€˜π‘₯)) = ((1...(βŒŠβ€˜π‘)) βˆͺ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))))
9290, 91syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (1...(βŒŠβ€˜π‘₯)) = ((1...(βŒŠβ€˜π‘)) βˆͺ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))))
9378, 92sseqtrrid 4035 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) βŠ† (1...(βŒŠβ€˜π‘₯)))
9493sselda 3982 . . . . . . . . . . . 12 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯)))
9565abscld 15382 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
9695adantlr 713 . . . . . . . . . . . 12 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
9794, 96syldan 591 . . . . . . . . . . 11 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
9877, 97fsumrecl 15679 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
9969, 70remulcld 11243 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) ∈ ℝ)
10069, 71remulcld 11243 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ Β· π‘š) ∈ ℝ)
10170recnd 11241 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ β„‚)
102101mullidd 11231 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (1 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
103 1red 11214 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 1 ∈ ℝ)
10449absge0d 15390 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘))) β†’ 0 ≀ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
10546, 50, 104fsumge0 15740 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ 0 ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
10651, 105jca 512 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ ∧ 0 ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
107106adantr 481 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ ∧ 0 ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
10844simprd 496 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ 1 ≀ 𝑐)
109108adantr 481 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 1 ≀ 𝑐)
110103, 83, 69, 109, 86letrd 11370 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 1 ≀ π‘₯)
111 lemul1a 12067 . . . . . . . . . . . 12 (((1 ∈ ℝ ∧ π‘₯ ∈ ℝ ∧ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ ∧ 0 ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))) ∧ 1 ≀ π‘₯) β†’ (1 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) ≀ (π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
112103, 69, 107, 110, 111syl31anc 1373 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (1 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) ≀ (π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
113102, 112eqbrtrrd 5172 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ (π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
114 hashcl 14315 . . . . . . . . . . . . 13 ((((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) ∈ Fin β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ∈ β„•0)
115 nn0re 12480 . . . . . . . . . . . . 13 ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ∈ β„•0 β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ∈ ℝ)
11677, 114, 1153syl 18 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ∈ ℝ)
117116, 71remulcld 11243 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) Β· π‘š) ∈ ℝ)
11871adantr 481 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) β†’ π‘š ∈ ℝ)
119 elfzuz 13496 . . . . . . . . . . . . . 14 (𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) β†’ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1)))
12081peano2nnd 12228 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((βŒŠβ€˜π‘) + 1) ∈ β„•)
121 eluznn 12901 . . . . . . . . . . . . . . . 16 ((((βŒŠβ€˜π‘) + 1) ∈ β„• ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑛 ∈ β„•)
122120, 121sylan 580 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑛 ∈ β„•)
123 simpllr 774 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š))
12483adantr 481 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑐 ∈ ℝ)
125 reflcl 13760 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ℝ β†’ (βŒŠβ€˜π‘) ∈ ℝ)
126 peano2re 11386 . . . . . . . . . . . . . . . . 17 ((βŒŠβ€˜π‘) ∈ ℝ β†’ ((βŒŠβ€˜π‘) + 1) ∈ ℝ)
127124, 125, 1263syl 18 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ ((βŒŠβ€˜π‘) + 1) ∈ ℝ)
128122nnred 12226 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑛 ∈ ℝ)
129 fllep1 13765 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ℝ β†’ 𝑐 ≀ ((βŒŠβ€˜π‘) + 1))
130124, 129syl 17 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑐 ≀ ((βŒŠβ€˜π‘) + 1))
131 eluzle 12834 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1)) β†’ ((βŒŠβ€˜π‘) + 1) ≀ 𝑛)
132131adantl 482 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ ((βŒŠβ€˜π‘) + 1) ≀ 𝑛)
133124, 127, 128, 130, 132letrd 11370 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 𝑐 ≀ 𝑛)
134 nfv 1917 . . . . . . . . . . . . . . . . 17 β„²π‘˜ 𝑐 ≀ 𝑛
135 nfcv 2903 . . . . . . . . . . . . . . . . . . 19 β„²π‘˜abs
136135, 12nffv 6901 . . . . . . . . . . . . . . . . . 18 β„²π‘˜(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)
137 nfcv 2903 . . . . . . . . . . . . . . . . . 18 β„²π‘˜ ≀
138 nfcv 2903 . . . . . . . . . . . . . . . . . 18 β„²π‘˜π‘š
139136, 137, 138nfbr 5195 . . . . . . . . . . . . . . . . 17 β„²π‘˜(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š
140134, 139nfim 1899 . . . . . . . . . . . . . . . 16 β„²π‘˜(𝑐 ≀ 𝑛 β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š)
141 breq2 5152 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑛 β†’ (𝑐 ≀ π‘˜ ↔ 𝑐 ≀ 𝑛))
14213fveq2d 6895 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑛 β†’ (absβ€˜π΄) = (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
143142breq1d 5158 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑛 β†’ ((absβ€˜π΄) ≀ π‘š ↔ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š))
144141, 143imbi12d 344 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑛 β†’ ((𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š) ↔ (𝑐 ≀ 𝑛 β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š)))
145140, 144rspc 3600 . . . . . . . . . . . . . . 15 (𝑛 ∈ β„• β†’ (βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š) β†’ (𝑐 ≀ 𝑛 β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š)))
146122, 123, 133, 145syl3c 66 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š)
147119, 146sylan2 593 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ π‘š)
14877, 97, 118, 147fsumle 15744 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))π‘š)
14971recnd 11241 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ π‘š ∈ β„‚)
150 fsumconst 15735 . . . . . . . . . . . . 13 (((((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) ∈ Fin ∧ π‘š ∈ β„‚) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))π‘š = ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) Β· π‘š))
15177, 149, 150syl2anc 584 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))π‘š = ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) Β· π‘š))
152148, 151breqtrd 5174 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) Β· π‘š))
153 biidd 261 . . . . . . . . . . . . 13 (𝑛 = ((βŒŠβ€˜π‘) + 1) β†’ (0 ≀ π‘š ↔ 0 ≀ π‘š))
154 0red 11216 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 0 ∈ ℝ)
15547, 30mpan9 507 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ 𝑛 ∈ β„•) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
156155adantlr 713 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ β„•) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
157122, 156syldan 591 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ ⦋𝑛 / π‘˜β¦Œπ΄ ∈ β„‚)
158157abscld 15382 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ ℝ)
15971adantr 481 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ π‘š ∈ ℝ)
160157absge0d 15390 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 0 ≀ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄))
161154, 158, 159, 160, 146letrd 11370 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))) β†’ 0 ≀ π‘š)
162161ralrimiva 3146 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ βˆ€π‘› ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1))0 ≀ π‘š)
163120nnzd 12584 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((βŒŠβ€˜π‘) + 1) ∈ β„€)
164 uzid 12836 . . . . . . . . . . . . . 14 (((βŒŠβ€˜π‘) + 1) ∈ β„€ β†’ ((βŒŠβ€˜π‘) + 1) ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1)))
165163, 164syl 17 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((βŒŠβ€˜π‘) + 1) ∈ (β„€β‰₯β€˜((βŒŠβ€˜π‘) + 1)))
166153, 162, 165rspcdva 3613 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ 0 ≀ π‘š)
167 reflcl 13760 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ (βŒŠβ€˜π‘₯) ∈ ℝ)
16869, 167syl 17 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘₯) ∈ ℝ)
169 ssdomg 8995 . . . . . . . . . . . . . . . 16 ((1...(βŒŠβ€˜π‘₯)) ∈ Fin β†’ ((((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) βŠ† (1...(βŒŠβ€˜π‘₯)) β†’ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) β‰Ό (1...(βŒŠβ€˜π‘₯))))
17064, 93, 169sylc 65 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) β‰Ό (1...(βŒŠβ€˜π‘₯)))
171 hashdomi 14339 . . . . . . . . . . . . . . 15 ((((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯)) β‰Ό (1...(βŒŠβ€˜π‘₯)) β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ≀ (β™―β€˜(1...(βŒŠβ€˜π‘₯))))
172170, 171syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ≀ (β™―β€˜(1...(βŒŠβ€˜π‘₯))))
173 flge0nn0 13784 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯) β†’ (βŒŠβ€˜π‘₯) ∈ β„•0)
174 hashfz1 14305 . . . . . . . . . . . . . . 15 ((βŒŠβ€˜π‘₯) ∈ β„•0 β†’ (β™―β€˜(1...(βŒŠβ€˜π‘₯))) = (βŒŠβ€˜π‘₯))
17557, 173, 1743syl 18 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (β™―β€˜(1...(βŒŠβ€˜π‘₯))) = (βŒŠβ€˜π‘₯))
176172, 175breqtrd 5174 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ≀ (βŒŠβ€˜π‘₯))
177 flle 13763 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ (βŒŠβ€˜π‘₯) ≀ π‘₯)
17869, 177syl 17 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (βŒŠβ€˜π‘₯) ≀ π‘₯)
179116, 168, 69, 176, 178letrd 11370 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) ≀ π‘₯)
180116, 69, 71, 166, 179lemul1ad 12152 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((β™―β€˜(((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) Β· π‘š) ≀ (π‘₯ Β· π‘š))
18198, 117, 100, 152, 180letrd 11370 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ (π‘₯ Β· π‘š))
18270, 98, 99, 100, 113, 181le2addd 11832 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) ≀ ((π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) + (π‘₯ Β· π‘š)))
183 ltp1 12053 . . . . . . . . . . 11 ((βŒŠβ€˜π‘) ∈ ℝ β†’ (βŒŠβ€˜π‘) < ((βŒŠβ€˜π‘) + 1))
184 fzdisj 13527 . . . . . . . . . . 11 ((βŒŠβ€˜π‘) < ((βŒŠβ€˜π‘) + 1) β†’ ((1...(βŒŠβ€˜π‘)) ∩ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) = βˆ…)
18582, 183, 1843syl 18 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((1...(βŒŠβ€˜π‘)) ∩ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))) = βˆ…)
18696recnd 11241 . . . . . . . . . 10 (((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ∈ β„‚)
187185, 92, 64, 186fsumsplit 15686 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) = (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + Σ𝑛 ∈ (((βŒŠβ€˜π‘) + 1)...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)))
18836adantrr 715 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ π‘₯ ∈ β„‚)
189188, 101, 149adddid 11237 . . . . . . . . 9 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š)) = ((π‘₯ Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄)) + (π‘₯ Β· π‘š)))
190182, 187, 1893brtr4d 5180 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) ≀ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š)))
19163, 68, 73, 76, 190letrd 11370 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ≀ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š)))
192 rpregt0 12987 . . . . . . . . 9 (π‘₯ ∈ ℝ+ β†’ (π‘₯ ∈ ℝ ∧ 0 < π‘₯))
193192ad2antrl 726 . . . . . . . 8 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (π‘₯ ∈ ℝ ∧ 0 < π‘₯))
194 ledivmul 12089 . . . . . . . 8 (((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ∈ ℝ ∧ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š) ∈ ℝ ∧ (π‘₯ ∈ ℝ ∧ 0 < π‘₯)) β†’ (((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / π‘₯) ≀ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š) ↔ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ≀ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š))))
19563, 72, 193, 194syl3anc 1371 . . . . . . 7 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / π‘₯) ≀ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š) ↔ (absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) ≀ (π‘₯ Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š))))
196191, 195mpbird 256 . . . . . 6 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ ((absβ€˜Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴) / π‘₯) ≀ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š))
19761, 196eqbrtrd 5170 . . . . 5 ((((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) ∧ (π‘₯ ∈ ℝ+ ∧ 𝑐 ≀ π‘₯)) β†’ (absβ€˜(Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) ≀ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘))(absβ€˜β¦‹π‘› / π‘˜β¦Œπ΄) + π‘š))
19810, 39, 45, 53, 197elo1d 15479 . . . 4 (((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) ∧ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š)) β†’ (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) ∈ 𝑂(1))
199198ex 413 . . 3 ((πœ‘ ∧ (𝑐 ∈ (1[,)+∞) ∧ π‘š ∈ ℝ)) β†’ (βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š) β†’ (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) ∈ 𝑂(1)))
200199rexlimdvva 3211 . 2 (πœ‘ β†’ (βˆƒπ‘ ∈ (1[,)+∞)βˆƒπ‘š ∈ ℝ βˆ€π‘˜ ∈ β„• (𝑐 ≀ π‘˜ β†’ (absβ€˜π΄) ≀ π‘š) β†’ (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) ∈ 𝑂(1)))
2018, 200mpd 15 1 (πœ‘ β†’ (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))𝐴 / π‘₯)) ∈ 𝑂(1))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  β¦‹csb 3893   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322   class class class wbr 5148   ↦ cmpt 5231  dom cdm 5676  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7408   β‰Ό cdom 8936  Fincfn 8938  β„‚cc 11107  β„cr 11108  0cc0 11109  1c1 11110   + caddc 11112   Β· cmul 11114  +∞cpnf 11244   < clt 11247   ≀ cle 11248   / cdiv 11870  β„•cn 12211  β„•0cn0 12471  β„€cz 12557  β„€β‰₯cuz 12821  β„+crp 12973  [,)cico 13325  ...cfz 13483  βŒŠcfl 13754  β™―chash 14289  abscabs 15180  π‘‚(1)co1 15429  Ξ£csu 15631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-inf2 9635  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186  ax-pre-sup 11187
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7855  df-1st 7974  df-2nd 7975  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-1o 8465  df-oadd 8469  df-er 8702  df-pm 8822  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-sup 9436  df-inf 9437  df-oi 9504  df-card 9933  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-div 11871  df-nn 12212  df-2 12274  df-3 12275  df-n0 12472  df-xnn0 12544  df-z 12558  df-uz 12822  df-rp 12974  df-ico 13329  df-fz 13484  df-fzo 13627  df-fl 13756  df-seq 13966  df-exp 14027  df-hash 14290  df-cj 15045  df-re 15046  df-im 15047  df-sqrt 15181  df-abs 15182  df-clim 15431  df-o1 15433  df-lo1 15434  df-sum 15632
This theorem is referenced by:  selberg2lem  27050
  Copyright terms: Public domain W3C validator