Theorem divsqrsumf

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	⊢ 𝐹 : ℝ+ ⟶ ℝ