This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: The function F used in divsqrsum is a real function. (Contributed by Mario Carneiro, 12-May-2016)
|
|
Ref |
Expression |
|
Hypothesis |
divsqrtsum.2 |
⊢ 𝐹 = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑛 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) ) |
|
Assertion |
divsqrsumf |
⊢ 𝐹 : ℝ+ ⟶ ℝ |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
divsqrtsum.2 |
⊢ 𝐹 = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑛 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) ) |
| 2 |
1
|
divsqrtsumlem |
⊢ ( 𝐹 : ℝ+ ⟶ ℝ ∧ 𝐹 ∈ dom ⇝𝑟 ∧ ( ( 𝐹 ⇝𝑟 1 ∧ 1 ∈ ℝ+ ) → ( abs ‘ ( ( 𝐹 ‘ 1 ) − 1 ) ) ≤ ( 1 / ( √ ‘ 1 ) ) ) ) |
| 3 |
2
|
simp1i |
⊢ 𝐹 : ℝ+ ⟶ ℝ |