Theorem resqrtcl

Description: Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013)

	Ref	Expression
Assertion	resqrtcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		resqrex	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ∃ 𝑦 ∈ ℝ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) )
2		simp1l	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → 𝐴 ∈ ℝ )
3		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
4		sqrtval	⊢ ( 𝐴 ∈ ℂ → ( √ ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
5	2 3 4	3syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( √ ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
6		simp3r	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( 𝑦 ↑ 2 ) = 𝐴 )
7		simp3l	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → 0 ≤ 𝑦 )
8		rere	⊢ ( 𝑦 ∈ ℝ → ( ℜ ‘ 𝑦 ) = 𝑦 )
9	8	3ad2ant2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( ℜ ‘ 𝑦 ) = 𝑦 )
10	7 9	breqtrrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → 0 ≤ ( ℜ ‘ 𝑦 ) )
11		rennim	⊢ ( 𝑦 ∈ ℝ → ( i · 𝑦 ) ∉ ℝ+ )
12	11	3ad2ant2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( i · 𝑦 ) ∉ ℝ+ )
13	6 10 12	3jca	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) )
14		recn	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
15	14	3ad2ant2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → 𝑦 ∈ ℂ )
16		resqreu	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
17	16	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
18		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ 2 ) = ( 𝑦 ↑ 2 ) )
19	18	eqeq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ 2 ) = 𝐴 ↔ ( 𝑦 ↑ 2 ) = 𝐴 ) )
20		fveq2	⊢ ( 𝑥 = 𝑦 → ( ℜ ‘ 𝑥 ) = ( ℜ ‘ 𝑦 ) )
21	20	breq2d	⊢ ( 𝑥 = 𝑦 → ( 0 ≤ ( ℜ ‘ 𝑥 ) ↔ 0 ≤ ( ℜ ‘ 𝑦 ) ) )
22		oveq2	⊢ ( 𝑥 = 𝑦 → ( i · 𝑥 ) = ( i · 𝑦 ) )
23		neleq1	⊢ ( ( i · 𝑥 ) = ( i · 𝑦 ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · 𝑦 ) ∉ ℝ+ ) )
24	22 23	syl	⊢ ( 𝑥 = 𝑦 → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · 𝑦 ) ∉ ℝ+ ) )
25	19 21 24	3anbi123d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) )
26	25	riota2	⊢ ( ( 𝑦 ∈ ℂ ∧ ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) → ( ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ↔ ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) = 𝑦 ) )
27	15 17 26	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ↔ ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) = 𝑦 ) )
28	13 27	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) = 𝑦 )
29	5 28	eqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( √ ‘ 𝐴 ) = 𝑦 )
30		simp2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → 𝑦 ∈ ℝ )
31	29 30	eqeltrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( √ ‘ 𝐴 ) ∈ ℝ )
32	31	rexlimdv3a	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ∃ 𝑦 ∈ ℝ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℝ ) )
33	1 32	mpd	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℝ )