Step |
Hyp |
Ref |
Expression |
1 |
|
o1fsum.1 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ 𝑉 ) |
2 |
|
o1fsum.2 |
⊢ ( 𝜑 → ( 𝑘 ∈ ℕ ↦ 𝐴 ) ∈ 𝑂(1) ) |
3 |
|
nnssre |
⊢ ℕ ⊆ ℝ |
4 |
3
|
a1i |
⊢ ( 𝜑 → ℕ ⊆ ℝ ) |
5 |
1 2
|
o1mptrcl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℂ ) |
6 |
|
1red |
⊢ ( 𝜑 → 1 ∈ ℝ ) |
7 |
4 5 6
|
elo1mpt2 |
⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ ↦ 𝐴 ) ∈ 𝑂(1) ↔ ∃ 𝑐 ∈ ( 1 [,) +∞ ) ∃ 𝑚 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ) |
8 |
2 7
|
mpbid |
⊢ ( 𝜑 → ∃ 𝑐 ∈ ( 1 [,) +∞ ) ∃ 𝑚 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) |
9 |
|
rpssre |
⊢ ℝ+ ⊆ ℝ |
10 |
9
|
a1i |
⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) → ℝ+ ⊆ ℝ ) |
11 |
|
nfcv |
⊢ Ⅎ 𝑛 𝐴 |
12 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ 𝐴 |
13 |
|
csbeq1a |
⊢ ( 𝑘 = 𝑛 → 𝐴 = ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) |
14 |
11 12 13
|
cbvsumi |
⊢ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⦋ 𝑛 / 𝑘 ⦌ 𝐴 |
15 |
|
fzfid |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ) |
16 |
|
o1f |
⊢ ( ( 𝑘 ∈ ℕ ↦ 𝐴 ) ∈ 𝑂(1) → ( 𝑘 ∈ ℕ ↦ 𝐴 ) : dom ( 𝑘 ∈ ℕ ↦ 𝐴 ) ⟶ ℂ ) |
17 |
2 16
|
syl |
⊢ ( 𝜑 → ( 𝑘 ∈ ℕ ↦ 𝐴 ) : dom ( 𝑘 ∈ ℕ ↦ 𝐴 ) ⟶ ℂ ) |
18 |
1
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑉 ) |
19 |
|
dmmptg |
⊢ ( ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑉 → dom ( 𝑘 ∈ ℕ ↦ 𝐴 ) = ℕ ) |
20 |
18 19
|
syl |
⊢ ( 𝜑 → dom ( 𝑘 ∈ ℕ ↦ 𝐴 ) = ℕ ) |
21 |
20
|
feq2d |
⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ ↦ 𝐴 ) : dom ( 𝑘 ∈ ℕ ↦ 𝐴 ) ⟶ ℂ ↔ ( 𝑘 ∈ ℕ ↦ 𝐴 ) : ℕ ⟶ ℂ ) ) |
22 |
17 21
|
mpbid |
⊢ ( 𝜑 → ( 𝑘 ∈ ℕ ↦ 𝐴 ) : ℕ ⟶ ℂ ) |
23 |
|
eqid |
⊢ ( 𝑘 ∈ ℕ ↦ 𝐴 ) = ( 𝑘 ∈ ℕ ↦ 𝐴 ) |
24 |
23
|
fmpt |
⊢ ( ∀ 𝑘 ∈ ℕ 𝐴 ∈ ℂ ↔ ( 𝑘 ∈ ℕ ↦ 𝐴 ) : ℕ ⟶ ℂ ) |
25 |
22 24
|
sylibr |
⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ 𝐴 ∈ ℂ ) |
26 |
25
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ 𝑥 ∈ ℝ+ ) → ∀ 𝑘 ∈ ℕ 𝐴 ∈ ℂ ) |
27 |
|
elfznn |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ ) |
28 |
12
|
nfel1 |
⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ∈ ℂ |
29 |
13
|
eleq1d |
⊢ ( 𝑘 = 𝑛 → ( 𝐴 ∈ ℂ ↔ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ∈ ℂ ) ) |
30 |
28 29
|
rspc |
⊢ ( 𝑛 ∈ ℕ → ( ∀ 𝑘 ∈ ℕ 𝐴 ∈ ℂ → ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ∈ ℂ ) ) |
31 |
30
|
impcom |
⊢ ( ( ∀ 𝑘 ∈ ℕ 𝐴 ∈ ℂ ∧ 𝑛 ∈ ℕ ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ∈ ℂ ) |
32 |
26 27 31
|
syl2an |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ∈ ℂ ) |
33 |
15 32
|
fsumcl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ∈ ℂ ) |
34 |
14 33
|
eqeltrid |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 ∈ ℂ ) |
35 |
|
rpcn |
⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ ) |
36 |
35
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ ) |
37 |
|
rpne0 |
⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 ) |
38 |
37
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ≠ 0 ) |
39 |
34 36 38
|
divcld |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 / 𝑥 ) ∈ ℂ ) |
40 |
|
simplrl |
⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) → 𝑐 ∈ ( 1 [,) +∞ ) ) |
41 |
|
1re |
⊢ 1 ∈ ℝ |
42 |
|
elicopnf |
⊢ ( 1 ∈ ℝ → ( 𝑐 ∈ ( 1 [,) +∞ ) ↔ ( 𝑐 ∈ ℝ ∧ 1 ≤ 𝑐 ) ) ) |
43 |
41 42
|
ax-mp |
⊢ ( 𝑐 ∈ ( 1 [,) +∞ ) ↔ ( 𝑐 ∈ ℝ ∧ 1 ≤ 𝑐 ) ) |
44 |
40 43
|
sylib |
⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) → ( 𝑐 ∈ ℝ ∧ 1 ≤ 𝑐 ) ) |
45 |
44
|
simpld |
⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) → 𝑐 ∈ ℝ ) |
46 |
|
fzfid |
⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) → ( 1 ... ( ⌊ ‘ 𝑐 ) ) ∈ Fin ) |
47 |
25
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) → ∀ 𝑘 ∈ ℕ 𝐴 ∈ ℂ ) |
48 |
|
elfznn |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) → 𝑛 ∈ ℕ ) |
49 |
47 48 31
|
syl2an |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ∈ ℂ ) |
50 |
49
|
abscld |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ) → ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ∈ ℝ ) |
51 |
46 50
|
fsumrecl |
⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ∈ ℝ ) |
52 |
|
simplrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) → 𝑚 ∈ ℝ ) |
53 |
51 52
|
readdcld |
⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) + 𝑚 ) ∈ ℝ ) |
54 |
34 36 38
|
absdivd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 / 𝑥 ) ) = ( ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 ) / ( abs ‘ 𝑥 ) ) ) |
55 |
54
|
adantrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( abs ‘ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 / 𝑥 ) ) = ( ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 ) / ( abs ‘ 𝑥 ) ) ) |
56 |
|
rprege0 |
⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) |
57 |
56
|
ad2antrl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) |
58 |
|
absid |
⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( abs ‘ 𝑥 ) = 𝑥 ) |
59 |
57 58
|
syl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( abs ‘ 𝑥 ) = 𝑥 ) |
60 |
59
|
oveq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 ) / ( abs ‘ 𝑥 ) ) = ( ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 ) / 𝑥 ) ) |
61 |
55 60
|
eqtrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( abs ‘ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 / 𝑥 ) ) = ( ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 ) / 𝑥 ) ) |
62 |
34
|
adantrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 ∈ ℂ ) |
63 |
62
|
abscld |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 ) ∈ ℝ ) |
64 |
|
fzfid |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ) |
65 |
47 27 31
|
syl2an |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ∈ ℂ ) |
66 |
65
|
adantlr |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ∈ ℂ ) |
67 |
66
|
abscld |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ∈ ℝ ) |
68 |
64 67
|
fsumrecl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ∈ ℝ ) |
69 |
57
|
simpld |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ ) |
70 |
51
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ∈ ℝ ) |
71 |
52
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → 𝑚 ∈ ℝ ) |
72 |
70 71
|
readdcld |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) + 𝑚 ) ∈ ℝ ) |
73 |
69 72
|
remulcld |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( 𝑥 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) + 𝑚 ) ) ∈ ℝ ) |
74 |
14
|
fveq2i |
⊢ ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 ) = ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) |
75 |
64 66
|
fsumabs |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) |
76 |
74 75
|
eqbrtrid |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) |
77 |
|
fzfid |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ) |
78 |
|
ssun2 |
⊢ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ⊆ ( ( 1 ... ( ⌊ ‘ 𝑐 ) ) ∪ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) |
79 |
|
flge1nn |
⊢ ( ( 𝑐 ∈ ℝ ∧ 1 ≤ 𝑐 ) → ( ⌊ ‘ 𝑐 ) ∈ ℕ ) |
80 |
44 79
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) → ( ⌊ ‘ 𝑐 ) ∈ ℕ ) |
81 |
80
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑐 ) ∈ ℕ ) |
82 |
81
|
nnred |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑐 ) ∈ ℝ ) |
83 |
45
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → 𝑐 ∈ ℝ ) |
84 |
|
flle |
⊢ ( 𝑐 ∈ ℝ → ( ⌊ ‘ 𝑐 ) ≤ 𝑐 ) |
85 |
83 84
|
syl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑐 ) ≤ 𝑐 ) |
86 |
|
simprr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → 𝑐 ≤ 𝑥 ) |
87 |
82 83 69 85 86
|
letrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑐 ) ≤ 𝑥 ) |
88 |
|
fznnfl |
⊢ ( 𝑥 ∈ ℝ → ( ( ⌊ ‘ 𝑐 ) ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( ( ⌊ ‘ 𝑐 ) ∈ ℕ ∧ ( ⌊ ‘ 𝑐 ) ≤ 𝑥 ) ) ) |
89 |
69 88
|
syl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ( ⌊ ‘ 𝑐 ) ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( ( ⌊ ‘ 𝑐 ) ∈ ℕ ∧ ( ⌊ ‘ 𝑐 ) ≤ 𝑥 ) ) ) |
90 |
81 87 89
|
mpbir2and |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑐 ) ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) |
91 |
|
fzsplit |
⊢ ( ( ⌊ ‘ 𝑐 ) ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) = ( ( 1 ... ( ⌊ ‘ 𝑐 ) ) ∪ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) ) |
92 |
90 91
|
syl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) = ( ( 1 ... ( ⌊ ‘ 𝑐 ) ) ∪ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) ) |
93 |
78 92
|
sseqtrrid |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) |
94 |
93
|
sselda |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) |
95 |
65
|
abscld |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ∈ ℝ ) |
96 |
95
|
adantlr |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ∈ ℝ ) |
97 |
94 96
|
syldan |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ∈ ℝ ) |
98 |
77 97
|
fsumrecl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ∈ ℝ ) |
99 |
69 70
|
remulcld |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( 𝑥 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) ∈ ℝ ) |
100 |
69 71
|
remulcld |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( 𝑥 · 𝑚 ) ∈ ℝ ) |
101 |
70
|
recnd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ∈ ℂ ) |
102 |
101
|
mulid2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( 1 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) |
103 |
|
1red |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → 1 ∈ ℝ ) |
104 |
49
|
absge0d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ) → 0 ≤ ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) |
105 |
46 50 104
|
fsumge0 |
⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) → 0 ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) |
106 |
51 105
|
jca |
⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ∈ ℝ ∧ 0 ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) ) |
107 |
106
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ∈ ℝ ∧ 0 ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) ) |
108 |
44
|
simprd |
⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) → 1 ≤ 𝑐 ) |
109 |
108
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → 1 ≤ 𝑐 ) |
110 |
103 83 69 109 86
|
letrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → 1 ≤ 𝑥 ) |
111 |
|
lemul1a |
⊢ ( ( ( 1 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ∈ ℝ ∧ 0 ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) ) ∧ 1 ≤ 𝑥 ) → ( 1 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) ≤ ( 𝑥 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) ) |
112 |
103 69 107 110 111
|
syl31anc |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( 1 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) ≤ ( 𝑥 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) ) |
113 |
102 112
|
eqbrtrrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ≤ ( 𝑥 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) ) |
114 |
|
hashcl |
⊢ ( ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin → ( ♯ ‘ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) ∈ ℕ0 ) |
115 |
|
nn0re |
⊢ ( ( ♯ ‘ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) ∈ ℕ0 → ( ♯ ‘ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) ∈ ℝ ) |
116 |
77 114 115
|
3syl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ♯ ‘ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) ∈ ℝ ) |
117 |
116 71
|
remulcld |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ( ♯ ‘ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) · 𝑚 ) ∈ ℝ ) |
118 |
71
|
adantr |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℝ ) |
119 |
|
elfzuz |
⊢ ( 𝑛 ∈ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) |
120 |
81
|
peano2nnd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ( ⌊ ‘ 𝑐 ) + 1 ) ∈ ℕ ) |
121 |
|
eluznn |
⊢ ( ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ∈ ℕ ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) → 𝑛 ∈ ℕ ) |
122 |
120 121
|
sylan |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) → 𝑛 ∈ ℕ ) |
123 |
|
simpllr |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) → ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) |
124 |
83
|
adantr |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) → 𝑐 ∈ ℝ ) |
125 |
|
reflcl |
⊢ ( 𝑐 ∈ ℝ → ( ⌊ ‘ 𝑐 ) ∈ ℝ ) |
126 |
|
peano2re |
⊢ ( ( ⌊ ‘ 𝑐 ) ∈ ℝ → ( ( ⌊ ‘ 𝑐 ) + 1 ) ∈ ℝ ) |
127 |
124 125 126
|
3syl |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) → ( ( ⌊ ‘ 𝑐 ) + 1 ) ∈ ℝ ) |
128 |
122
|
nnred |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) → 𝑛 ∈ ℝ ) |
129 |
|
fllep1 |
⊢ ( 𝑐 ∈ ℝ → 𝑐 ≤ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) |
130 |
124 129
|
syl |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) → 𝑐 ≤ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) |
131 |
|
eluzle |
⊢ ( 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) → ( ( ⌊ ‘ 𝑐 ) + 1 ) ≤ 𝑛 ) |
132 |
131
|
adantl |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) → ( ( ⌊ ‘ 𝑐 ) + 1 ) ≤ 𝑛 ) |
133 |
124 127 128 130 132
|
letrd |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) → 𝑐 ≤ 𝑛 ) |
134 |
|
nfv |
⊢ Ⅎ 𝑘 𝑐 ≤ 𝑛 |
135 |
|
nfcv |
⊢ Ⅎ 𝑘 abs |
136 |
135 12
|
nffv |
⊢ Ⅎ 𝑘 ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) |
137 |
|
nfcv |
⊢ Ⅎ 𝑘 ≤ |
138 |
|
nfcv |
⊢ Ⅎ 𝑘 𝑚 |
139 |
136 137 138
|
nfbr |
⊢ Ⅎ 𝑘 ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ≤ 𝑚 |
140 |
134 139
|
nfim |
⊢ Ⅎ 𝑘 ( 𝑐 ≤ 𝑛 → ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ≤ 𝑚 ) |
141 |
|
breq2 |
⊢ ( 𝑘 = 𝑛 → ( 𝑐 ≤ 𝑘 ↔ 𝑐 ≤ 𝑛 ) ) |
142 |
13
|
fveq2d |
⊢ ( 𝑘 = 𝑛 → ( abs ‘ 𝐴 ) = ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) |
143 |
142
|
breq1d |
⊢ ( 𝑘 = 𝑛 → ( ( abs ‘ 𝐴 ) ≤ 𝑚 ↔ ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ≤ 𝑚 ) ) |
144 |
141 143
|
imbi12d |
⊢ ( 𝑘 = 𝑛 → ( ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ↔ ( 𝑐 ≤ 𝑛 → ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ≤ 𝑚 ) ) ) |
145 |
140 144
|
rspc |
⊢ ( 𝑛 ∈ ℕ → ( ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) → ( 𝑐 ≤ 𝑛 → ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ≤ 𝑚 ) ) ) |
146 |
122 123 133 145
|
syl3c |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) → ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ≤ 𝑚 ) |
147 |
119 146
|
sylan2 |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ≤ 𝑚 ) |
148 |
77 97 118 147
|
fsumle |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) 𝑚 ) |
149 |
71
|
recnd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → 𝑚 ∈ ℂ ) |
150 |
|
fsumconst |
⊢ ( ( ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ∧ 𝑚 ∈ ℂ ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) 𝑚 = ( ( ♯ ‘ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) · 𝑚 ) ) |
151 |
77 149 150
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) 𝑚 = ( ( ♯ ‘ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) · 𝑚 ) ) |
152 |
148 151
|
breqtrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ≤ ( ( ♯ ‘ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) · 𝑚 ) ) |
153 |
|
biidd |
⊢ ( 𝑛 = ( ( ⌊ ‘ 𝑐 ) + 1 ) → ( 0 ≤ 𝑚 ↔ 0 ≤ 𝑚 ) ) |
154 |
|
0red |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) → 0 ∈ ℝ ) |
155 |
47 30
|
mpan9 |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ 𝑛 ∈ ℕ ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ∈ ℂ ) |
156 |
155
|
adantlr |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ℕ ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ∈ ℂ ) |
157 |
122 156
|
syldan |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ∈ ℂ ) |
158 |
157
|
abscld |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) → ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ∈ ℝ ) |
159 |
71
|
adantr |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) → 𝑚 ∈ ℝ ) |
160 |
157
|
absge0d |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) → 0 ≤ ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) |
161 |
154 158 159 160 146
|
letrd |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) → 0 ≤ 𝑚 ) |
162 |
161
|
ralrimiva |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) 0 ≤ 𝑚 ) |
163 |
120
|
nnzd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ( ⌊ ‘ 𝑐 ) + 1 ) ∈ ℤ ) |
164 |
|
uzid |
⊢ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ∈ ℤ → ( ( ⌊ ‘ 𝑐 ) + 1 ) ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) |
165 |
163 164
|
syl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ( ⌊ ‘ 𝑐 ) + 1 ) ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑐 ) + 1 ) ) ) |
166 |
153 162 165
|
rspcdva |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → 0 ≤ 𝑚 ) |
167 |
|
reflcl |
⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ∈ ℝ ) |
168 |
69 167
|
syl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℝ ) |
169 |
|
ssdomg |
⊢ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin → ( ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ≼ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ) |
170 |
64 93 169
|
sylc |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ≼ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) |
171 |
|
hashdomi |
⊢ ( ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ≼ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → ( ♯ ‘ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) ≤ ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ) |
172 |
170 171
|
syl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ♯ ‘ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) ≤ ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ) |
173 |
|
flge0nn0 |
⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 ) |
174 |
|
hashfz1 |
⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) = ( ⌊ ‘ 𝑥 ) ) |
175 |
57 173 174
|
3syl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) = ( ⌊ ‘ 𝑥 ) ) |
176 |
172 175
|
breqtrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ♯ ‘ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) ≤ ( ⌊ ‘ 𝑥 ) ) |
177 |
|
flle |
⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ≤ 𝑥 ) |
178 |
69 177
|
syl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑥 ) ≤ 𝑥 ) |
179 |
116 168 69 176 178
|
letrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ♯ ‘ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) ≤ 𝑥 ) |
180 |
116 69 71 166 179
|
lemul1ad |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ( ♯ ‘ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) · 𝑚 ) ≤ ( 𝑥 · 𝑚 ) ) |
181 |
98 117 100 152 180
|
letrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ≤ ( 𝑥 · 𝑚 ) ) |
182 |
70 98 99 100 113 181
|
le2addd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) ≤ ( ( 𝑥 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) + ( 𝑥 · 𝑚 ) ) ) |
183 |
|
ltp1 |
⊢ ( ( ⌊ ‘ 𝑐 ) ∈ ℝ → ( ⌊ ‘ 𝑐 ) < ( ( ⌊ ‘ 𝑐 ) + 1 ) ) |
184 |
|
fzdisj |
⊢ ( ( ⌊ ‘ 𝑐 ) < ( ( ⌊ ‘ 𝑐 ) + 1 ) → ( ( 1 ... ( ⌊ ‘ 𝑐 ) ) ∩ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) = ∅ ) |
185 |
82 183 184
|
3syl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ( 1 ... ( ⌊ ‘ 𝑐 ) ) ∩ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) = ∅ ) |
186 |
96
|
recnd |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ∈ ℂ ) |
187 |
185 92 64 186
|
fsumsplit |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ 𝑐 ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) ) |
188 |
36
|
adantrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → 𝑥 ∈ ℂ ) |
189 |
188 101 149
|
adddid |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( 𝑥 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) + 𝑚 ) ) = ( ( 𝑥 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ) + ( 𝑥 · 𝑚 ) ) ) |
190 |
182 187 189
|
3brtr4d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) ≤ ( 𝑥 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) + 𝑚 ) ) ) |
191 |
63 68 73 76 190
|
letrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 ) ≤ ( 𝑥 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) + 𝑚 ) ) ) |
192 |
|
rpregt0 |
⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) |
193 |
192
|
ad2antrl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) |
194 |
|
ledivmul |
⊢ ( ( ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 ) ∈ ℝ ∧ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) + 𝑚 ) ∈ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) → ( ( ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 ) / 𝑥 ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) + 𝑚 ) ↔ ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 ) ≤ ( 𝑥 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) + 𝑚 ) ) ) ) |
195 |
63 72 193 194
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ( ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 ) / 𝑥 ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) + 𝑚 ) ↔ ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 ) ≤ ( 𝑥 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) + 𝑚 ) ) ) ) |
196 |
191 195
|
mpbird |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( ( abs ‘ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 ) / 𝑥 ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) + 𝑚 ) ) |
197 |
61 196
|
eqbrtrd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑐 ≤ 𝑥 ) ) → ( abs ‘ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 / 𝑥 ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑐 ) ) ( abs ‘ ⦋ 𝑛 / 𝑘 ⦌ 𝐴 ) + 𝑚 ) ) |
198 |
10 39 45 53 197
|
elo1d |
⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 / 𝑥 ) ) ∈ 𝑂(1) ) |
199 |
198
|
ex |
⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ℝ ) ) → ( ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 / 𝑥 ) ) ∈ 𝑂(1) ) ) |
200 |
199
|
rexlimdvva |
⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( 1 [,) +∞ ) ∃ 𝑚 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝑐 ≤ 𝑘 → ( abs ‘ 𝐴 ) ≤ 𝑚 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 / 𝑥 ) ) ∈ 𝑂(1) ) ) |
201 |
8 200
|
mpd |
⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 𝐴 / 𝑥 ) ) ∈ 𝑂(1) ) |