Theorem rpsqrtcn

Description: Continuity of the real positive square root function. (Contributed by Thierry Arnoux, 20-Dec-2021)

	Ref	Expression
Assertion	rpsqrtcn	|- ( sqrt |` RR+ ) e. ( RR+ -cn-> RR+ )

Proof

Step	Hyp	Ref	Expression
1		rpssre	|- RR+ C_ RR
2		ax-resscn	|- RR C_ CC
3	1 2	sstri	|- RR+ C_ CC
4		sqrtf	|- sqrt : CC --> CC
5		fdm	|- ( sqrt : CC --> CC -> dom sqrt = CC )
6	4 5	ax-mp	|- dom sqrt = CC
7	3 6	sseqtrri	|- RR+ C_ dom sqrt
8	7	sseli	|- ( x e. RR+ -> x e. dom sqrt )
9		rpsqrtcl	|- ( x e. RR+ -> ( sqrt ` x ) e. RR+ )
10	8 9	jca	|- ( x e. RR+ -> ( x e. dom sqrt /\ ( sqrt ` x ) e. RR+ ) )
11	10	rgen	|- A. x e. RR+ ( x e. dom sqrt /\ ( sqrt ` x ) e. RR+ )
12		ffun	|- ( sqrt : CC --> CC -> Fun sqrt )
13	4 12	ax-mp	|- Fun sqrt
14		ffvresb	|- ( Fun sqrt -> ( ( sqrt |` RR+ ) : RR+ --> RR+ <-> A. x e. RR+ ( x e. dom sqrt /\ ( sqrt ` x ) e. RR+ ) ) )
15	13 14	ax-mp	|- ( ( sqrt |` RR+ ) : RR+ --> RR+ <-> A. x e. RR+ ( x e. dom sqrt /\ ( sqrt ` x ) e. RR+ ) )
16	11 15	mpbir	|- ( sqrt |` RR+ ) : RR+ --> RR+
17		ioorp	|- ( 0 (,) +oo ) = RR+
18		ioossico	|- ( 0 (,) +oo ) C_ ( 0 [,) +oo )
19	17 18	eqsstrri	|- RR+ C_ ( 0 [,) +oo )
20		resabs1	|- ( RR+ C_ ( 0 [,) +oo ) -> ( ( sqrt |` ( 0 [,) +oo ) ) |` RR+ ) = ( sqrt |` RR+ ) )
21	19 20	ax-mp	|- ( ( sqrt |` ( 0 [,) +oo ) ) |` RR+ ) = ( sqrt |` RR+ )
22		resqrtcn	|- ( sqrt |` ( 0 [,) +oo ) ) e. ( ( 0 [,) +oo ) -cn-> RR )
23		rescncf	|- ( RR+ C_ ( 0 [,) +oo ) -> ( ( sqrt |` ( 0 [,) +oo ) ) e. ( ( 0 [,) +oo ) -cn-> RR ) -> ( ( sqrt |` ( 0 [,) +oo ) ) |` RR+ ) e. ( RR+ -cn-> RR ) ) )
24	19 22 23	mp2	|- ( ( sqrt |` ( 0 [,) +oo ) ) |` RR+ ) e. ( RR+ -cn-> RR )
25	21 24	eqeltrri	|- ( sqrt |` RR+ ) e. ( RR+ -cn-> RR )
26		cncffvrn	|- ( ( RR+ C_ CC /\ ( sqrt |` RR+ ) e. ( RR+ -cn-> RR ) ) -> ( ( sqrt |` RR+ ) e. ( RR+ -cn-> RR+ ) <-> ( sqrt |` RR+ ) : RR+ --> RR+ ) )
27	3 25 26	mp2an	|- ( ( sqrt |` RR+ ) e. ( RR+ -cn-> RR+ ) <-> ( sqrt |` RR+ ) : RR+ --> RR+ )
28	16 27	mpbir	|- ( sqrt |` RR+ ) e. ( RR+ -cn-> RR+ )