Theorem rpsqrtcn

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

	Ref	Expression
Assertion	rpsqrtcn	⊢ ( √ ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		rpssre	⊢ ℝ+ ⊆ ℝ
2		ax-resscn	⊢ ℝ ⊆ ℂ
3	1 2	sstri	⊢ ℝ+ ⊆ ℂ
4		sqrtf	⊢ √ : ℂ ⟶ ℂ
5		fdm	⊢ ( √ : ℂ ⟶ ℂ → dom √ = ℂ )
6	4 5	ax-mp	⊢ dom √ = ℂ
7	3 6	sseqtrri	⊢ ℝ+ ⊆ dom √
8	7	sseli	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ dom √ )
9		rpsqrtcl	⊢ ( 𝑥 ∈ ℝ+ → ( √ ‘ 𝑥 ) ∈ ℝ+ )
10	8 9	jca	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ dom √ ∧ ( √ ‘ 𝑥 ) ∈ ℝ+ ) )
11	10	rgen	⊢ ∀ 𝑥 ∈ ℝ+ ( 𝑥 ∈ dom √ ∧ ( √ ‘ 𝑥 ) ∈ ℝ+ )
12		ffun	⊢ ( √ : ℂ ⟶ ℂ → Fun √ )
13	4 12	ax-mp	⊢ Fun √
14		ffvresb	⊢ ( Fun √ → ( ( √ ↾ ℝ+ ) : ℝ+ ⟶ ℝ+ ↔ ∀ 𝑥 ∈ ℝ+ ( 𝑥 ∈ dom √ ∧ ( √ ‘ 𝑥 ) ∈ ℝ+ ) ) )
15	13 14	ax-mp	⊢ ( ( √ ↾ ℝ+ ) : ℝ+ ⟶ ℝ+ ↔ ∀ 𝑥 ∈ ℝ+ ( 𝑥 ∈ dom √ ∧ ( √ ‘ 𝑥 ) ∈ ℝ+ ) )
16	11 15	mpbir	⊢ ( √ ↾ ℝ+ ) : ℝ+ ⟶ ℝ+
17		ioorp	⊢ ( 0 (,) +∞ ) = ℝ+
18		ioossico	⊢ ( 0 (,) +∞ ) ⊆ ( 0 [,) +∞ )
19	17 18	eqsstrri	⊢ ℝ+ ⊆ ( 0 [,) +∞ )
20		resabs1	⊢ ( ℝ+ ⊆ ( 0 [,) +∞ ) → ( ( √ ↾ ( 0 [,) +∞ ) ) ↾ ℝ+ ) = ( √ ↾ ℝ+ ) )
21	19 20	ax-mp	⊢ ( ( √ ↾ ( 0 [,) +∞ ) ) ↾ ℝ+ ) = ( √ ↾ ℝ+ )
22		resqrtcn	⊢ ( √ ↾ ( 0 [,) +∞ ) ) ∈ ( ( 0 [,) +∞ ) –cn→ ℝ )
23		rescncf	⊢ ( ℝ+ ⊆ ( 0 [,) +∞ ) → ( ( √ ↾ ( 0 [,) +∞ ) ) ∈ ( ( 0 [,) +∞ ) –cn→ ℝ ) → ( ( √ ↾ ( 0 [,) +∞ ) ) ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℝ ) ) )
24	19 22 23	mp2	⊢ ( ( √ ↾ ( 0 [,) +∞ ) ) ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℝ )
25	21 24	eqeltrri	⊢ ( √ ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℝ )
26		cncfcdm	⊢ ( ( ℝ+ ⊆ ℂ ∧ ( √ ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℝ ) ) → ( ( √ ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℝ+ ) ↔ ( √ ↾ ℝ+ ) : ℝ+ ⟶ ℝ+ ) )
27	3 25 26	mp2an	⊢ ( ( √ ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℝ+ ) ↔ ( √ ↾ ℝ+ ) : ℝ+ ⟶ ℝ+ )
28	16 27	mpbir	⊢ ( √ ↾ ℝ+ ) ∈ ( ℝ+ –cn→ ℝ+ )