Metamath Proof Explorer

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	\|- F = ( x e. RR+ \|-> ( sum_ n e. ( 1 ... ( \|_ ` x ) ) ( 1 / ( sqrt ` n ) ) - ( 2 x. ( sqrt ` x ) ) ) )
	Assertion	divsqrsumf	\|- F : RR+ --> RR

Step	Hyp	Ref	Expression
1		divsqrtsum.2	\|- F = ( x e. RR+ \|-> ( sum_ n e. ( 1 ... ( \|_ ` x ) ) ( 1 / ( sqrt ` n ) ) - ( 2 x. ( sqrt ` x ) ) ) )
2	1	divsqrtsumlem	\|- ( F : RR+ --> RR /\ F e. dom ~~>r /\ ( ( F ~~>r 1 /\ 1 e. RR+ ) -> ( abs ` ( ( F ` 1 ) - 1 ) ) <_ ( 1 / ( sqrt ` 1 ) ) ) )
3	2	simp1i	\|- F : RR+ --> RR

Step

Hyp

Ref

Expression

divsqrtsum.2

 |-  F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` n ) ) - ( 2 x. ( sqrt ` x ) ) ) )

 |-  ( F : RR+ --> RR /\ F e. dom ~~>r /\ ( ( F ~~>r 1 /\ 1 e. RR+ ) -> ( abs ` ( ( F ` 1 ) - 1 ) ) <_ ( 1 / ( sqrt ` 1 ) ) ) )

 |-  F : RR+ --> RR